Pith. sign in

REVIEW 4 major objections 5 minor 2 cited by

Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Step-by-step Lean 4 proof checks, summarized by a tiny LSTM and fused with a process reward model, consistently improve best-of-n answer selection across LLMs and math datasets.

desk verdict A genuinely novel step-level Lean verification pipeline and a useful benchmark, but the paper's own audit data leave the central causal claim that formal proofs drive the BoN gains unproven. read the letter →

arxiv 2506.04592 v1 pith:3Y5PBBCJ submitted 2025-06-05 cs.CL cs.AIcs.LG

Chengwu Liu , Ye Yuan , Yichun Yin , Yan Xu , Xin Xu , Zaoyu Chen , Yasheng Wang , Lifeng Shang
show 2 more authors
Qun Liu Ming Zhang
This is my paper
classification cs.CLcs.AIcs.LG
keywords formalverificationLean4auto-formalizationprocessrewardmodelchain-of-thoughtreasoningbest-of-ntheoremprovingLSTM
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that formal verification of individual reasoning steps can serve as a reliable retrospective signal for detecting hallucinations in LLM chain-of-thought. Concretely, it proposes Safe: decompose a solution into steps, auto-formalize each step into a Lean 4 theorem using GPT-4o, attempt a proof with an automated theorem prover, and map each step to one of four states. A small LSTM reads the state sequence and produces a retrospective score, which is combined multiplicatively with a process reward model's prospective score to select the best of five sampled solutions. On MATH-500, GSM8K, and CollegeMath, across four LLMs, Safe beats standalone ORMs, PRMs, and majority voting, and the proof outcomes themselves furnish interpretable evidence. The paper also releases FormalStep, 30,809 auto-formalized step-level statements, as a benchmark for step-correctness theorem proving.

What carries the argument

The carrying object is the step verifier: a two-stage pipeline in which GPT-4o auto-formalizes each natural-language reasoning step into a Lean 4 theorem statement (using the step's own premises as hypotheses and its conclusion as the goal), and DeepSeek-Prover-V1.5 (or COPRA) attempts a proof within a small sample budget. The verifier's output is a four-state token per step; a two-layer 64-hidden-unit LSTM over these tokens produces the retrospective score, and the final selection score is $\mathrm{score}_{\mathrm{retro}}^\alpha \cdot \mathrm{score}_{\mathrm{pro}}^{1-\alpha}$ fused with a process reward model. The proof artifacts are the checkable evidence: a successful Lean proof of a faithful formalization is what the framework relies on to mark a step sound.

What would settle it

Construct trajectories in which every step is a provable Lean 4 theorem but the final answer is wrong (e.g., by formalizing an identity that is true but irrelevant, or by omitting a condition in the formalization), and check whether Safe's score ranks such a trajectory above a correct one. If a large fraction of wrong-but-formally-provable trajectories are preferred, the retrospective signal is not tracking step correctness.

Watch

Extended reading notes

Core claim

The central claim is that the output of Lean 4's proof checker on auto-formalized single reasoning steps, aggregated over the whole trajectory, is a usable and complementary verification signal for LLM mathematical reasoning. The paper's position is that a step is 'correct' in the relevant sense when its formalization is a provable Lean 4 theorem; four discrete states (no verification needed, formalization failed, proof succeeded, proof failed) condense each step into two bits of evidence. An LSTM trained on state sequences learns to convert that evidence into a retrospective score, and the weighted product of this score with an off-the-shelf PRM's prospective Q-value outperforms each component alone. This is the first claimed use of Lean 4 to verify natural-language reasoning trajectories generated by LLMs.

Load-bearing premise

A Lean proof of the machine-translated statement is taken as evidence that the original natural-language step is correct; if GPT-4o's formalization is unfaithful to the step, a valid proof can still accompany a false step, and the paper's own evaluation finds 18.6% of formalized statements poorly aligned while only 72.2% of steps formalize at all.

Editorial extensions

If this is right

  • Best-of-N selection improves: Safe beats the best ORM/PRM baselines on 11 of 12 model-dataset pairs, with the largest gains on MATH-500 and CollegeMath.
  • The four-state encoding makes verification cost and failure modes explicit: unformalizable steps (geometry/combinatorics), failed formalization, and proof failures are distinguishable, so the method can report where evidence is missing.
  • Data efficiency: about 2,000 trajectories from 500 questions suffice to train the LSTM aggregator, orders of magnitude less than PRM800K or Math-Shepherd training data.
  • Synergy: retrospective (formal, step-local) and prospective (PRM Q-value) scores are complementary; the weighted product outperforms ensembles of ORMs and PRMs.
  • FormalStep (30,809 statements, 81.2% provable by DeepSeek-Prover-V1.5 with 16 samples) provides a low-compute benchmark for step-level auto-formalization and theorem proving.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the formalization step were made provably faithful (e.g., by checking semantic equivalence or training a dedicated formalizer with alignment feedback), the retrospective signal should become stronger; the current 18.6% poor-alignment rate caps the verifier's precision.
  • The same four-state, LSTM-aggregation recipe could transfer to code reasoning steps (assertions about program states) or to deductive tasks in first-order logic, where formalization is more tractable than in geometry or combinatorics.
  • Because the LSTM is tiny and each state carries two bits, the aggregator's decisions can be systematically audited; the paper's limitation section already points toward using the LSTM's parameters to identify critical proof steps, which could turn the verifier into a step-level reward for reinforcement learning.
  • A testable extension: replacing the flat four-state encoding with a state distribution (e.g., proof success rate over multiple ATP tries) might reduce the noise the paper acknowledges from auto-formalization and theorem-prover failures.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper proposes Safe, a neuro-symbolic framework for best-of-n answer selection in LLM mathematical reasoning. Each chain-of-thought step is auto-formalized into a Lean 4 statement and passed to an automated theorem prover; the resulting sequence of four discrete verification states (no verification required, failed formalization, proof success, proof failure) is aggregated by a small LSTM to produce a retrospective score. This score is combined multiplicatively with a process reward model (PRM) score, and the trajectory with the highest combined score is selected. The paper also introduces FormalStep, a dataset of 30,809 auto-formalized step-level Lean 4 statements. Experiments on GSM8K, MATH-500, and CollegeMath across four LLMs report consistent improvements over PRM and ORM baselines, plus ablations of ensemble strategies and theorem-proving budgets.

Significance. If the empirical findings are robust, the paper makes a useful contribution by connecting formal verification to LLM reasoning evaluation in an interpretable, step-aware way. The proposed state representation is simple and the LSTM aggregator is parameter-efficient, trained on far fewer trajectories than existing PRM training sets. The FormalStep dataset addresses a genuinely underexplored task, step-level auto-formalization, and the reported proof rates under limited compute are informative. The paper also includes several honest analyses, including a scaling comparison and a limitation statement. However, the central claim that formal verification is the driver of the improvements is not yet established, because the empirical evaluation lacks statistical rigor and the reported pipeline contains substantial noise that is not controlled for.

major comments (4)
  1. [Section 4.2, Table 1] The headline claim that Safe 'consistently outperforms almost every other baseline' rests on single point estimates with no reported variance. Several margins are very small (e.g., Llama-3.1 GSM8K: Safe 90.8 vs. Shepherd 90.2; GPT-4o MATH-500: Safe 80.4 vs. Shepherd 79.8). Without standard errors, confidence intervals, or multiple random seeds, the reader cannot determine whether these differences are meaningful. Please report variance estimates and, ideally, paired significance tests across the evaluation problems.
  2. [Section 3.3, Eq. (3)] The ensemble score is defined as score_retro^alpha * score_pro^(1-alpha), with alpha as a hyper-parameter, but the paper never reports the alpha values used in Table 1 or the procedure for selecting them. If alpha is tuned on the test sets, or chosen separately for each model/dataset, the comparison against fixed baselines is not fair. Please report the alpha values, the search range, and a sensitivity analysis showing how results vary with alpha.
  3. [Sections 4.1 and 5.2, Table 5, Figure 5] The paper does not establish that the Lean 4 formal proofs, rather than generic sequential ensembling or the LSTM's outcome supervision, are responsible for the reported improvements. The LSTM is trained on final-answer correctness labels (Section 4.1), and the state sequence is noisy: only 72.2% of steps are formalizable, 18.6% of formalized statements are rated 'poor' in semantic alignment, and 43.3% of Proof-Successful states occur in trajectories with a wrong final answer. The Limitations section itself concedes that the correlation between the Lean 4 REPL output and final evaluation scores is 'relatively indirect.' To support the mechanism claim, add controlled ablations such as training the LSTM on random or permuted state tokens, or comparing against an ORM+PRM ensemble that does not use the formal verifier at all; these controls would show whether the formal proof signal contributes beyond a generic supervised ensemble.
  4. [Appendix G, Table 5] The quality audit of FormalStep relies entirely on GPT-4o-mini as an LLM-as-a-judge, but the judge's reliability is not assessed. Since the 80.9% 'good' alignment figure is used to argue that auto-formalization is of acceptable quality, please provide agreement statistics against a human-annotated sample, or at least a qualitative error analysis. This is needed to interpret the formalization noise that the method is designed to handle.
minor comments (5)
  1. [Section 5.1 and Figure 6] The text states that a sample budget of 16 is used as the default theorem-proving strategy, but Figure 6 plots success rates for max attempts from 20 to 25. Please clarify this discrepancy or relabel the figure.
  2. [Equation (2)] The notation W·LSTM(...) + b is underspecified; please state the dimensions of W and the final hidden state, and clarify whether the sigmoid is applied elementwise.
  3. [Section 5.4] The claim that single-step validation requires 'approximately 4–8x greater' LLM queries than PRMs is not derived in the text; please show the calculation or soften the claim to match the reported average attempt counts.
  4. [Appendix C] The fallback from LLM-based decomposition to heuristic rules is mentioned, but the frequency and quality of this fallback are not reported; please state how often the JSON parsing fails and whether decomposition mode affects downstream results.
  5. [Table 3] The abbreviations ORM1, ORM2, PRM1, PRM2 are introduced in the table but not defined in the caption; please spell them out or refer to the baseline names from Section 4.1.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Safe's BoN gains are evaluated on held-out datasets against external baselines, the LSTM aggregator is standard supervised verification, and the paper's self-citations are not load-bearing.

full rationale

Safe's central claim is an empirical Best-of-N@5 improvement on held-out MATH-500, GSM8K, and CollegeMath evaluations against external ORM and PRM baselines (Section 4.2, Table 1), so the headline result is not defined in terms of the fitted components. The LSTM state aggregator is trained on state sequences labeled by ground-truth final-answer correctness from a training subset (Section 4.1); using such a trained verifier to select test-time responses is standard supervised verification, not a prediction that reduces to its input. The Lean 4 evidence itself is produced by off-the-shelf provers (DeepSeek-Prover-V1.5, COPRA) and checked by the Lean REPL, giving it independent machine-checked content conditional on semantic alignment of the auto-formalized statements. Self-citations such as FIMO, Process-driven Autoformalization, and DT-solver appear in related-work or benchmark context and are not load-bearing for the main result; no uniqueness theorem from the authors' prior work is invoked to forbid alternatives. The paper's own audit data weaken the mechanistic interpretation but do not show circularity: Table 5 reports 18.6% of FormalStep statements have 'poor' semantic alignment, Figure 5 shows only 56.7% of Proof-Successful states come from correct trajectories, and the Limitations section concedes that 'The correlation between the output of the Lean 4 REPL and the final evaluation scores appears to be relatively indirect.' These are correctness-risk concerns about the quality of the formal-state evidence, not instances where a stated prediction is equivalent to its input by construction. No circular step can be exhibited from the paper's equations or citations.

Assumptions & free parameters 5 free parameters · 6 assumptions · 0 invented entities

The central claim rests on the faithfulness of the auto-formalization step, the compositionality of step-wise correctness, and the sufficiency of the four-state representation. All of these are domain assumptions adopted by the paper; none are machine-checked or externally grounded beyond the paper's own LLM-judge evaluation.

free parameters (5)
  • Ensemble weight alpha = not reported
    Section 3.3 defines score = retro^alpha * pro^(1-alpha) and calls alpha a hyper-parameter; its value and tuning protocol are not reported. Appendix D selects the weighted-multiplication strategy using one model and one dataset, so alpha may have been chosen after observing results.
  • LSTM parameters = 2 layers, hidden size 64
    Section 4.1 trains the state aggregator to predict final-answer correctness from state sequences; the weights are fitted on reasoning trajectories generated by each target LLM.
  • Max auto-formalization attempts = 3
    Section 5.4 states each step allows a maximum of 3 auto-formalization attempts; chosen to balance cost and reliability.
  • Max theorem-proving attempts = 16 default, 8 in reduced-cost analysis
    Section 5.1 adopts DeepSeek-Prover-V1.5 with a sample budget of 16 (no MCTS); Section 5.4 says reducing to 8 still exceeds 80% proof success.
  • LSTM training data size = 500 MATH, 1,000 GSM8K, full CollegeMath training
    Section 4.1 reports the aggregator training set is randomly selected to be approximately the same size as the test dataset for each benchmark.
assumptions (6)
  • standard math Lean 4 and mathlib are sound: a statement checked by the Lean 4 REPL is true.
    The framework relies on the Lean kernel to certify formal statements (Section 3.2.2); this is standard trust in an interactive theorem prover.
  • domain assumption Auto-formalization is semantically faithful: a provable formal statement validates the corresponding natural-language step.
    Appendix A instructs the model that 'if the Lean 4 theorem can be proven, then the step is correct'; Table 5 shows 18.6% of statements scored 'poor' alignment by the paper's own judge, so this assumption is partially violated.
  • domain assumption Step decomposition preserves the correctness of the full trajectory.
    Appendix C splits solutions into independent steps; the verifier scores each step and aggregates, implicitly assuming each step's validity composes to overall correctness.
  • domain assumption The four-state sequence is a sufficient signal with which to rank trajectories.
    Section 3.3 trains an LSTM to map the state sequence to a scalar score; this assumes the two bits per step carry enough information about final correctness.
  • domain assumption Prospective PRM scores and retrospective formal-verification scores are complementary and can be combined by a weighted product.
    Section 3.3 defines score = retro^alpha * pro^(1-alpha); Section 5.5 argues synergy from the complementary nature of the two signals, but this is tested only through ablations.
  • ad hoc to paper LLM-as-a-judge labels are a valid measure of semantic alignment and theorem category.
    Appendix B uses GPT-4o-mini to label 'good', 'fair', 'poor' and to classify theorems; no human validation of these labels is reported in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification." pith.science (2026). https://pith.science/paper/3Y5PBBCJ

@misc{pith2026250604592,
  author       = {Pith},
  title        = {Pith review of: Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3Y5PBBCJ}},
  note         = {Machine review of arXiv:2506.04592}
}
abstract

Chain-of-Thought (CoT) prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs). However, to mitigate hallucinations in CoT that are notoriously difficult to detect, current methods such as process reward models (PRMs) or self-consistency operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness. To address this issue, we draw inspiration from the idea that "the gold standard for supporting a mathematical claim is to provide a proof". We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations. We evaluate our framework $Safe$ across multiple language models and various mathematical datasets, demonstrating a significant performance improvement while offering interpretable and verifiable evidence. We also propose $FormalStep$ as a benchmark for step correctness theorem proving with $30,809$ formal statements. To the best of our knowledge, our work represents the first endeavor to utilize formal mathematical language Lean 4 for verifying natural language content generated by LLMs, aligning with the reason why formal mathematical languages were created in the first place: to provide a robust foundation for hallucination-prone human-written proofs.

Figures

Figures reproduced from arXiv: 2506.04592 by the authors.

Figure 1
Figure 1. The distinction between prospective verifica [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. The primary pipeline flowchart. Solutions for each mathematical problem, generated using the zero-shot [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. The pipeline of the step verifier. We construct a prompt that incorporates the relevant question and [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Scaling Best-of-N with Math-Shephed PRM and ArmoRM ORM. The red dashed line indicates the [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: The distribution of steps by state and their [PITH_FULL_IMAGE:figures/full_fig_p015_5.png]
Figure 6
Figure 6. Figure 6: The proof rates of two SOTA theorem provers [PITH_FULL_IMAGE:figures/full_fig_p016_6.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

    cs.CL 2025-07 conditional novelty 6.0 of 10

    A minimal-prior pipeline with automated data curation and verifier-driven RL lets small LLMs generate verifiable Dafny specifications and beat larger proprietary models on a synthetic compositional benchmark.

  2. LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

    cs.AI 2025-06 conditional novelty 5.0 of 10

    LeanConjecturer automatically generates thousands of Lean 4 theorem statements from Mathlib files and uses them for reinforcement learning, with modest measured gains on held-out problems.

Reference graph

Works this paper leans on

69 extracted references · 32 canonical work pages · cited by 2 Pith papers

  1. [1]

    Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. 2024. https://arxiv.org/abs/2402.00157 Large language models for mathematical reasoning: Progresses and challenges . ArXiv preprint, abs/2402.00157

    arXiv 2024

  2. [2]

    Jeremy Avigad, Leonardo De Moura, and Soonho Kong. 2021. Theorem proving in lean

    work page 2021

  3. [3]

    Tarek R Besold, Artur d’Avila Garcez, Sebastian Bader, Howard Bowman, Pedro Domingos, Pascal Hitzler, Kai-Uwe K \"u hnberger, Luis C Lamb, Priscila Machado Vieira Lima, Leo de Penning, et al. 2021. Neural-symbolic learning and reasoning: A survey and interpretation 1. In Neuro-Symbolic Artificial Intelligence: The State of the Art, pages 1--51. IOS press

    work page 2021

  4. [4]

    Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. Advances in neural information processing systems, 33:1877--1901

    2020

  5. [5]

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. 2021. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168

    arXiv 2021

  6. [6]

    Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. 2024. The llama 3 herd of models. arXiv preprint arXiv:2407.21783

    arXiv 2024

  7. [7]

    Bin Feng, Zequn Liu, Nanlan Huang, Zhiping Xiao, Haomiao Zhang, Srbuhi Mirzoyan, Hanwen Xu, Jiaran Hao, Yinghui Xu, Ming Zhang, et al. 2024. A bioactivity foundation model using pairwise meta-learning. Nature Machine Intelligence, 6(8):962--974

    work page 2024

  8. [8]

    Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. 2022. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations

    work page 2022

Show all 69 references
  1. [9]

    Shibo Hao, Yi Gu, Haodi Ma, Joshua Hong, Zhen Wang, Daisy Wang, and Zhiting Hu. 2023. Reasoning with language model is planning with world model. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 8154--8173

    2023

  2. [10]

    Alexander Havrilla, Sharath Chandra Raparthy, Christoforos Nalmpantis, Jane Dwivedi-Yu, Maksym Zhuravinskyi, Eric Hambro, and Roberta Raileanu. 2024. Glore: When, where, and how to improve llm reasoning via global and local refinements. In Forty-first International Conference ...

    2024

  3. [11]

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the math dataset. NeurIPS

    2021

  4. [12]

    S Hochreiter. 1997. Long short-term memory. Neural Computation MIT-Press

    1997

  5. [13]

    Jie Huang and Kevin Chen-Chuan Chang. 2023. Towards reasoning in large language models: A survey. In Findings of the Association for Computational Linguistics: ACL 2023, pages 1049--1065

    2023

  6. [14]

    Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. 2024. Mustard: Mastering uniform synthesis of theorem and proof data. In The Twelfth International Conference on Learning Representations

    2024

  7. [15]

    Aaron Hurst, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, et al. 2024. Gpt-4o system card. arXiv preprint arXiv:2410.21276

    2024 arXiv

  8. [16]

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2022. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learnin...

    2022

  9. [17]

    Dongwei Jiang, Marcio Fonseca, and Shay B Cohen. 2024. Leanreasoner: Boosting complex logical reasoning with lean. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long ...

    2024

  10. [18]

    John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ronneberger, Kathryn Tunyasuvunakool, Russ Bates, Augustin Z \' dek, Anna Potapenko, et al. 2021. Highly accurate protein structure prediction with alphafold. nature, 596(7873):583--589

    2021

  11. [19]

    John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Kathryn Tunyasuvunakool, Olaf Ronneberger, Russ Bates, Augustin Z \' dek, Alex Bridgland, et al. 2020. Alphafold 2. Fourteenth Critical Assessment of Techniques for Protein Structure Prediction

    2020

  12. [20]

    Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. https://proceedings.neurips.cc/paper_files/paper/2022/file/8bb0d291acd4acf06ef112099c16f326-Paper-Conference.pdf Large language models are zero-shot reasoners . In Advances in Neural Inf...

    2022

  13. [21]

    Xin Lai, Zhuotao Tian, Yukang Chen, Senqiao Yang, Xiangru Peng, and Jiaya Jia. 2024. Step-dpo: Step-wise preference optimization for long-chain reasoning of llms. CoRR

    2024

  14. [22]

    Smith, and Hannaneh Hajishirzi

    Nathan Lambert, Valentina Pyatkin, Jacob Morrison, LJ Miranda, Bill Yuchen Lin, Khyathi Chandu, Nouha Dziri, Sachin Kumar, Tom Zick, Yejin Choi, Noah A. Smith, and Hannaneh Hajishirzi. 2024. https://arxiv.org/abs/2403.13787 Rewardbench: Evaluating reward models for language mo...

    2024 arXiv

  15. [23]

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337--26349

    2022

  16. [24]

    Jia Li, Ge Li, Xuanming Zhang, Yihong Dong, and Zhi Jin. 2024. Evocodebench: An evolving code generation benchmark aligned with real-world code repositories. arXiv preprint arXiv:2404.00599

    2024 arXiv

  17. [25]

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. 2024. https://openreview.net/forum?id=v8L0pN6EOi Let's verify step by step . In The Twelfth International Conference on Learning Re...

    2024

  18. [26]

    Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. 2023. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295

    2023 arXiv

  19. [27]

    Chris Yuhao Liu, Liang Zeng, Jiacai Liu, Rui Yan, Jujie He, Chaojie Wang, Shuicheng Yan, Yang Liu, and Yahui Zhou. 2024. Skywork-reward: Bag of tricks for reward modeling in llms. arXiv preprint arXiv:2410.18451

    2024 arXiv

  20. [28]

    Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. 2024. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.01940

    2024 arXiv

  21. [29]

    Ali Madani, Ben Krause, Eric R Greene, Subu Subramanian, Benjamin P Mohr, James M Holton, Jose Luis Olmos, Caiming Xiong, Zachary Z Sun, Richard Socher, et al. 2023. Large language models generate functional protein sequences across diverse families. Nature Biotechnology, 41(8...

    2023

  22. [30]

    The mathlib Community. 2019. https://arxiv.org/abs/1910.09336 The lean mathematical library . CoRR, abs/1910.09336

    2019 arXiv

  23. [31]

    Leonardo de Moura and Sebastian Ullrich. 2021. https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37 The lean 4 theorem prover and programming language . In Automated Deduction--CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12--15,...

    2021 doi

  24. [32]

    Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. Linc: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference on Empirical...

    2023

  25. [33]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806--3824

    2023

  26. [34]

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations

    2022

  27. [35]

    Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393

    2020 arXiv

  28. [36]

    David Rein, Betty Li Hou, Asa Cooper Stickland, Jackson Petty, Richard Yuanzhe Pang, Julien Dirani, Julian Michael, and Samuel R Bowman. 2023. Gpqa: A graduate-level google-proof q&a benchmark. arXiv preprint arXiv:2311.12022

    2023 arXiv

  29. [37]

    Md Kamruzzaman Sarker, Lu Zhou, Aaron Eberhart, and Pascal Hitzler. 2022. Neuro-symbolic artificial intelligence: Current trends. Ai Communications, 34(3):197--209

    2022

  30. [38]

    Amrith Setlur, Chirag Nagpal, Adam Fisch, Xinyang Geng, Jacob Eisenstein, Rishabh Agarwal, Alekh Agarwal, Jonathan Berant, and Aviral Kumar. 2024. Rewarding progress: Scaling automated process verifiers for llm reasoning. In The Thirteenth International Conference on Learning ...

    2024

  31. [39]

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. 2024. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300

    2024 arXiv

  32. [40]

    Jianhao Shen, Yichun Yin, Lin Li, Lifeng Shang, Xin Jiang, Ming Zhang, and Qun Liu. 2021. https://doi.org/10.18653/v1/2021.findings-emnlp.195 Generate & Rank : A Multi-task Framework for Math Word Problems . In Findings of the Association for Computational Linguistics : EMNLP ...

    2021 doi

  33. [41]

    Zhengyang Tang, Xingxing Zhang, Benyou Wang, and Furu Wei. 2024. Mathscale: Scaling instruction tuning for mathematical reasoning. In Forty-first International Conference on Machine Learning

    2024

  34. [42]

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. 2024. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling

    2024

  35. [43]

    Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. 2023. A language-agent approach to formal theorem-proving. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23

    2023

  36. [44]

    Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2023 a . https://doi.org/10.18653/v1/2023.acl-long.706 DT -solver: Automated theorem proving with dynamic-tree sampling gui...

    2023 doi

  37. [45]

    Haoxiang Wang, Wei Xiong, Tengyang Xie, Han Zhao, and Tong Zhang. 2024 a . Interpretable preferences via multi-objective reward modeling and mixture-of-experts. In EMNLP

    2024

  38. [46]

    Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. 2024 b . https://doi.org/10.18653/v1/2024.acl-long.510 Math- Shepherd : Verify and Reinforce LLMs Step-by-step without Human Annotations . In Proceedings of the 62nd Annual Mee...

    2024 doi

  39. [47]

    Xiaoxuan Wang, Ziniu Hu, Pan Lu, Yanqiao Zhu, Jieyu Zhang, Satyen Subramaniam, Arjun R Loomba, Shichang Zhang, Yizhou Sun, and Wei Wang. 2023 b . Scibench: Evaluating college-level scientific problem-solving abilities of large language models. arXiv preprint arXiv:2307.10635

    2023 arXiv

  40. [48]

    Chi, Quoc V Le, and Denny Zhou

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. 2022. https://openreview.net/forum?id=_VjQlMeSB_J Chain of thought prompting elicits reasoning in large language models . In Advances in Neural Information Proc...

    2022

  41. [49]

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353--32368

    2022

  42. [50]

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024 a . Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333

    2024 arXiv

  43. [51]

    Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. 2024 b . Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. CoRR

    2024

  44. [52]

    Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, et al. 2023. Trigo: Benchmarking formal mathematical proof reduction for generative language models. In Proceedings of the 2023 Conference on Empirical ...

    2023

  45. [53]

    Wei Xiong, Hanning Zhang, Nan Jiang, and Tong Zhang. 2024. An implementation of generative prm. https://github.com/RLHFlow/RLHF-Reward-Modeling

    2024

  46. [54]

    Xin Xu, Shizhe Diao, Can Yang, and Yang Wang. 2024 a . Can we verify step by step for incorrect answer detection? arXiv preprint arXiv:2402.10528

    2024 arXiv

  47. [55]

    Xin Xu, Tong Xiao, Zitong Chao, Zhenya Huang, Can Yang, and Yang Wang. 2024 b . Can llms solve longer math word problems better? arXiv preprint arXiv:2405.14804

    2024 arXiv

  48. [56]

    Xin Xu, Jiaxin Zhang, Tianhao Chen, Zitong Chao, Jishan Hu, and Can Yang. 2025. Ugmathbench: A diverse and dynamic benchmark for undergraduate-level mathematical reasoning with large language models. arXiv preprint arXiv:2501.13766

    2025 arXiv

  49. [57]

    Yuchen Yan, Jin Jiang, Yang Liu, Yixin Cao, Xin Xu, Xunliang Cai, Jian Shao, et al. 2024. S ^ 3 c-math: Spontaneous step-level self-correction makes large language models better mathematical reasoners. arXiv preprint arXiv:2409.01524

    2024 arXiv

  50. [58]

    Junwei Yang, Hanwen Xu, Srbuhi Mirzoyan, Tong Chen, Zixuan Liu, Zequn Liu, Wei Ju, Luchen Liu, Zhiping Xiao, Ming Zhang, et al. 2024 a . Poisoning medical knowledge using large language models. Nature Machine Intelligence, 6(10):1156--1168

    2024

  51. [59]

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024 b . Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075

    2024 arXiv

  52. [60]

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36:21573--21612

    2023

  53. [61]

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024 a . Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847

    2024 arXiv

  54. [62]

    Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. 2024 b . Internlm-math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332

    2024 arXiv

  55. [63]

    Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. 2023. https://arxiv.org/abs/2309.12284 Metamath: Bootstrap your own mathematical questions for large language models . ArXiv preprint, abs/2309.12284

    2023 arXiv

  56. [64]

    Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. 2022. Star: Bootstrapping reasoning with reasoning. Advances in Neural Information Processing Systems, 35:15476--15488

    2022

  57. [65]

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations

    2021

  58. [66]

    Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. 2024. Don't trust: Verify-grounding llm quantitative reasoning with autoformalization. In ICLR

    2024

  59. [67]

    Terry Yue Zhuo, Minh Chien Vu, Jenny Chim, Han Hu, Wenhao Yu, Ratnadira Widyasari, Imam Nur Bani Yusuf, Haolan Zhan, Junda He, Indraneil Paul, et al. 2024. Bigcodebench: Benchmarking code generation with diverse function calls and complex instructions. arXiv preprint arXiv:2406.15877

    2024 arXiv

  60. [68]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...

  61. [69]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.