Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

The paper claims that HERMES, an agent that interleaves LLM reasoning with Lean4 verification of intermediate steps, improves mathematical accuracy and reduces token use relative to reward-model approaches.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

Interleaving LLM reasoning with Lean4 verification of individual steps improves math-problem accuracy and cuts token budgets versus reward-model methods.

T0 review reviewed 2026-08-03 challenge →

load-bearing objection HERMES is a genuine integration of existing Lean-verification pieces with a real gap in its core claim: the semantic bridge between informal steps and Lean statements is checked by an LLM, not the kernel, and the paper's own appendix shows that gap changing the answer. the 3 major comments →

arxiv 2511.18760 v2 pith:XSVCGREQ submitted 2025-11-24 cs.AI cs.FL

HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs

Azim Ospanov , Zijin Feng , Jiacheng Sun , Haoli Bai , Xin Shen , Farzan Farnia This is my paper
classification cs.AI cs.FL
keywords LLM reasoningLean4formal verificationautoformalizationchain-of-thoughtprocess rewardmathematical reasoningtool-augmented agent
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The reading

The paper tries to show that the flexible, exploratory reasoning of an LLM and the rigid, machine-checkable formality of a proof assistant like Lean4 can be fused into a single agent that is both more accurate and cheaper than existing methods. The agent, HERMES, verifies each critical chain-of-thought step: an informal step is translated into a Lean4 goal, a prover attempts to prove or disprove it, and the resulting signal tells the LLM whether to continue, revise, or pivot. Across four benchmarks and three LLM sizes, the paper reports accuracy gains over zero-shot CoT and reward-model baselines, with up to 67% improvement on AIME'25 and up to 80% fewer inference FLOPs. If correct, this makes step-level verification a practical, interpretable alternative to score-based reasoning guidance.

Core claim

On its own terms, the paper's central claim is that interleaving informal proof steps with formally verified Lean4 checks during inference improves LLM mathematical reasoning and reduces compute. The mechanism is a verification loop: for each critical step, a translator produces a Lean4 statement, a prover attempts to prove the statement and its negation, and only the compiler's verdict is fed back to the LLM. A memory module stores verified steps so later steps can reference them as hypotheses. The paper reports consistent accuracy improvements on four benchmarks across three base models, with the largest gains on the hardest datasets, and token budgets 4–6 times smaller than reward-model s

What carries the argument

The central object is the verification loop connecting the reasoning LLM to the Lean4 compiler. Each natural-language proof step is autoformalized into a Lean4 theorem statement, which must compile; the statement is then backtranslated to English and checked for semantic equivalence; finally a prover tries to prove the goal and its negation, producing one of three signals (CORRECT, INCORRECT, VERIFICATION FAILURE). A memory buffer of verified steps provides hypotheses for later steps, maintaining continuity. This loop gives the LLM machine-checkable, step-level feedback instead of a scalar reward score.

Load-bearing premise

The back-translation check — an LLM deciding that the Lean statement means the same as the informal step — must actually catch semantic drift; if it does not, a verified Lean proof validates a proposition the LLM never meant to assert.

What would settle it

Collect the informal steps that HERMES marks CORRECT, backtranslate each to English, and have independent annotators decide whether the backtranslated statement matches the original informal step. If a large fraction of CORRECT steps are judged semantically mismatched, the Lean verification is not checking the LLM's actual reasoning.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • HERMES improves accuracy over base CoT and reward-based baselines across all tested settings, with an average gain of 14%.
  • The largest gains occur on the hardest benchmarks (AIME'25, HARDMath2), where reasoning drift is most damaging.
  • Token and FLOP budgets are comparable to zero-shot CoT and 4–6 times lower than reward-model best-of-N, so step-level verification is a compute-efficient alternative to sampling many traces.
  • Test-time scaling (Hermes@5) boosts accuracy by a further 20%, suggesting the verification signal remains useful across multiple attempts.
  • Ablation shows that removing either the prover or the memory buffer degrades accuracy, especially on AIME'25, confirming both modules carry the benefit.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If verified steps are reliable, the same loop could extend to other tasks with a formal verifier, such as program synthesis or logical reasoning, not just mathematics.
  • The back-translation equivalence check is itself an LLM judgment; a stronger approach might train a dedicated semantic-equivalence discriminator on verified positive/negative pairs.
  • The reported efficiency depends on the translator's success rate; at low budgets more than half of steps fail to translate, so improving autoformalization may shift the bottleneck to the prover.
  • On geometry, gains are smaller because formal libraries lag; as formal libraries grow, the approach could close that gap and become more uniformly beneficial.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. HERMES is an agentic framework that interleaves LLM-generated informal reasoning with Lean4 formal verification of intermediate proof steps. The reasoning LLM invokes a translation module (autoformalizer plus back-translation equivalence check), a prover module that tries to prove or disprove the formalized step, and a memory block that stores verified steps for retrieval. The authors report accuracy improvements over zero-shot CoT, majority voting, ORM/PRM baselines, and the earlier Safe method on MATH500, AIME'25, CollegeMath, and HARDMath2, with substantially lower token and FLOP budgets than reward-model-based best-of-N selection. They also provide ablations of the memory and prover modules and a sensitivity analysis of the Kt/Kp sampling budgets.

Significance. If the semantic bridge between informal steps and Lean statements were fully trusted, HERMES would be a valuable contribution: it makes step-level feedback machine-checkable rather than reward-model-based, provides interpretable verification signals, and the reported efficiency gains are practically important. The paper has real strengths: the code is publicly released, the experimental protocol is clearly described, the ablation and sensitivity analyses are informative, and the appendix candidly includes a failure case. However, the central claim of 'verifiable reasoning' depends on the correctness and faithfulness of the autoformalization/back-translation pipeline, and the paper's own Appendix C gives a concrete example where a Lean-verified step led to a wrong mathematical conclusion. The efficiency claim also rests on a coarse FLOP model. These issues are fixable but require additional analysis, so the current manuscript needs substantial revision before the central claims can be accepted.

major comments (3)
  1. [§3.1, Appendix C (Fig. 8)] The semantic bridge between the informal step and the Lean statement is not machine-checked. §3.1's second verification step uses an LLM back-translator to judge equivalence, but this checker is itself a stochastic LLM and no false-positive rate is reported. Appendix C (MATH500 precalculus-768) provides a direct failure: the Lean-verified steps are used to conclude tan⁻¹(x)=cot⁻¹(1/x) for x≠0, which is false for x<0, and the model then returns only 3±2√2, dropping the negative solutions the unaided CoT had found. Thus a CORRECT signal did not validate the actual reasoning step. Since 'verifiable' is the paper's central value proposition, the claim needs either a trusted (kernel-checked or deterministic) semantic equivalence check, or a measured false-positive rate of the back-translation check, or claims should be restricted to formal-statement correctness. This is load-bearing.
  2. [§4.6, Table 1, Table 3] Hyperparameter selection and evaluation overlap. Table 3 reports accuracy on HM2 for Kt/Kp combinations, and §4.6 states Kt=4, Kp=4 are set as defaults based on these results; Table 1 then reports HM2 accuracy with exactly these selected values. For the HM2 row, the test set is used for model selection, so the reported 30.3% may be optimistically biased. Additionally, AIME'25 contains only 30 problems; e.g., Qwen3-8B 20.0→30.0 is 3 problems, and no error bars or significance tests are provided anywhere. The paper should either use a validation split for hyperparameter choice and report held-out HM2 numbers, or provide confidence intervals/significance tests. This affects the reliability of the headline accuracy gains.
  3. [§4.4, Fig. 5] The FLOP comparison is based on a formula that sets nctx to the maximum 8,192 for every model and dataset, and it is not explained how the external translator/prover module costs are attributed. This is likely to overstate the cost of reward-model baselines (which generate up to 60 traces, but only 5 in the main comparison) and to understate Hermes's multi-module calls. The abstract's claim of '80% fewer total inference FLOPs' is load-bearing for the efficiency contribution. Please provide a detailed per-module token/FLOP accounting (actual contexts, number of sampler calls at Kt=Kp=4, prover/translator model sizes) and a sensitivity analysis of the FLOP estimate. As written, the efficiency advantage may be partly an artifact of the estimation method.
minor comments (5)
  1. [Abstract / §1] The abstract says 'up to 67% accuracy improvement' but Table 1 shows DeepSeek-V3.1 on AIME'25 going from 46.7 to 66.7, which is 20 percentage points (≈43% relative). Please ensure percentage improvement is consistently defined as relative or absolute.
  2. [Figure 2] The illustrative Lean code contains '80*x100*y' with a missing operator; it should read something like '80*x + 100*y'.
  3. [Related Works, p.3] The statement that current autoformalization models are 'capable of translating informal statements to formal goals with syntactic and semantic correctness' is unsupported in this paper and contradicted by Figures 6 and 7, where translation failures exceed 60% at Kt=1.
  4. [Tables 4-9] The topic distribution tables have formatting issues with numbers running together (e.g., '3636', '3610'). Also, the appendix figure caption (Figure 8) describes the case as 'Hermes detects and corrects a hallucinated reasoning step,' but the displayed trace suggests the verification actually reinforced an incorrect inference; the caption should be reworded to match the content.
  5. [General] The paper claims to be 'the first tool-based Lean4 reasoning agent' but prior work such as DTV and Lean-STaR already combine LLMs with Lean verification. The novelty claims should be softened to focus on the specific interleaving with memory and back-translation equivalence checking.

Circularity Check

1 steps flagged

No construction-level circularity: the accuracy and efficiency claims are empirical, not derived from fitted equations. The only mild self-referential loop is the HM2-based choice of Kt/Kp that is then reported as the HM2 result; a separate but non-circular validity gap is the LLM-judged back-translation equivalence.

specific steps
  1. fitted input called prediction [Section 4.6 (Table 3); Section 4.1 and Table 1 (HM2 row for DeepSeek-V3.1)]
    "We vary the autoformalizer sampling budget (Kt) from 1 to 8 and prover sampling budget (Kp) from 1 to 16 ... We thus set Kt=4 and Kp=4 as the default values in our experiments."

    The default Kt=Kp=4 is selected from the HM2 accuracy grid in Table 3, where the DeepSeek-V3.1 cell is 30.3%. The same cell is then reused as the reported HM2 accuracy (30.3%) in Table 1. Thus the headline HM2 result is not an out-of-sample prediction but the tuned operating point, and comparisons to untuned baselines on HM2 are partially forced by this selection. This is a mild self-referential evaluation loop, not a definitional equation-level circularity.

full rationale

The central claims of HERMES are empirical: accuracy and token/FLOP efficiency are measured on external benchmarks with separate answer checking. The prover and autoformalizer are externally cited components (Goedel-Prover-V2/Goedel-Autoformalizer [20]), and no accuracy number reduces by construction to a training label or fitted target. The only step approaching circularity is Section 4.6: Kt and Kp are chosen from the HM2 grid and the same grid cell is reported as the HM2 result, partially in-breeding that benchmark. This is a test-set tuning concern rather than a derivation-level equivalence. A related but non-circular validity issue is Section 3.1's back-translation equivalence: the semantic bridge from informal step to Lean statement is judged by an LLM, not by the Lean kernel. Appendix C even exhibits a concrete case where Lean-verified steps only supported x>0 yet the model used the identity for x!=0, so the CORRECT signal did not validate the step actually used. This weakens the 'verifiable' framing but does not make the measured improvements a restatement of the inputs. Self-citations to prior author work (APOLLO [28], Lean IMO dataset [32]) appear only in related work or ablations and are not load-bearing. Therefore the circularity score is low: 2.0, reflecting the mild HM2 tuning loop rather than any definitional circularity.

Axiom & Free-Parameter Ledger

4 free parameters · 5 axioms · 0 invented entities

The central empirical claim relies less on mathematical axioms than on engineering assumptions: the autoformalizer/back-translator pair must preserve semantic equivalence, and the main sampling budgets are tuned on an evaluation benchmark. No novel mathematical entities are postulated.

free parameters (4)
  • Kt (autoformalizer sampling budget) = 4 (default; grid evaluated 1, 4, 8)
    Table 3 shows HM2 accuracy rises from 15.6% at Kt=1 to 23.7% at Kt=4; Kt=4 is then used for all reported experiments, including HM2 itself.
  • Kp (prover sampling budget) = 4 (default; grid evaluated 1, 4, 8, 16)
    Table 3 shows HM2 accuracy improves from 16.6% to 30.3% as Kp goes 1 to 4; Kp=4 is selected on HM2 and then reported in Table 1.
  • Memory top-k retrieval = 3
    The memory module selects the top three recorded steps as context; no sensitivity analysis is reported for this choice.
  • Lean4 verification timeout = 60 seconds
    Verification success depends on timeout; no sensitivity analysis is reported.
axioms (5)
  • standard math Lean4's kernel is sound: every accepted proof is a valid derivation.
    The framework treats Lean's True/False signal as ground truth for the formalized goal.
  • domain assumption Goedel-Autoformalizer-8B produces Lean statements whose semantics match the intended informal proof step.
    Section 3.1 relies on the autoformalizer being syntactically and semantically correct; the only semantic check is LLM back-translation.
  • ad hoc to paper The LLM back-translation equivalence check reliably detects semantic mismatch.
    Section 3.1 uses an LLM to compare the original and backtranslated steps, so the semantic guard is itself an LLM prone to the errors the framework targets.
  • domain assumption A proof or counter-proof of the formalized goal corresponds to correctness or incorrectness of the informal step.
    This is the bridge from Lean's verdict to the natural-language reasoning step; it is assumed throughout the feedback module.
  • domain assumption The LLM invokes the verifier on critical steps and treats CORRECT feedback as reliable.
    Appendix A instructs the model to verify every critical step, but steps can also be skipped with NO VERIFICATION, so coverage is incomplete.

reviewed 2026-08-03 · how reviews work

0 comments
Cite this review

Pith. "Pith review of HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs." pith.science (2026). https://pith.science/paper/XSVCGREQ

@misc{pith2026251118760,
  author       = {Pith},
  title        = {Pith review of: HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XSVCGREQ}},
  note         = {Machine review of arXiv:2511.18760}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Informal mathematics has been central to modern large language model (LLM) reasoning, offering flexibility and efficient construction of arguments. However, purely informal reasoning is prone to logical gaps and subtle errors that are difficult to detect and correct. In contrast, formal theorem proving provides rigorous, verifiable mathematical reasoning, where each inference step is checked by a trusted compiler, but lacks the exploratory freedom of informal problem-solving. This mismatch leaves current LLM-based math agents without a principled way to combine the strengths of both paradigms. In this work, we introduce Hermes, the first tool-assisted agent that explicitly interleaves informal reasoning with formally verified proofs in Lean. The framework performs intermediate formal checking to prevent reasoning drift and a memory module for proof continuity across multi-step reasoning chains, enabling both exploration and verification. We evaluate Hermes on four challenging mathematical reasoning benchmarks using LLMs of varying parameter scales, from small models to state-of-the-art systems. Across all settings, Hermes reliably improves the reasoning accuracy of base models while substantially reducing reasoning token usage and computational cost compared to reward-based approaches. On difficult datasets such as AIME and HARDMath2, Hermes@1 achieves up to a 40% accuracy improvement while using 80% fewer total inference FLOPs. When scaled at test time, Hermes@5 boosts accuracy further by 20%. The implementation and codebase are publicly available at https://github.com/aziksh-ospanov/HERMES.

Figures

Figures reproduced from arXiv: 2511.18760 by Azim Ospanov, Farzan Farnia, Haoli Bai, Jiacheng Sun, Xin Shen, Zijin Feng.

Figure 1
Figure 1. Figure 1: Overview of the Hermes framework. Hermes is a Lean4-driven, multi-modular reasoning agent integrating LLM reasoning with formal verification for reliable mathematical problem solving. It comprises four modules: an LLM that generates reasoning steps, a translator that formalizes these steps into Lean code, a prover that symbolically verifies their correctness, and a feedback module that returns verification… view at source ↗
Figure 2
Figure 2. Figure 2: Full Hermes framework with illustrative examples. 3 Our Approach In this section, we describe Hermes, our framework for a verifiable and interpretable tool-based agent for mathematical reasoning. Hermes is designed to be split into multiple swappable modules that analyze intermediate proof steps and produce proper verification for each mathematical step [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Average reasoning token usage per problem on MATH500, AIME’25, CollegeMath, and HardMath2 [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Scaling behavior of BoN across ORM, PRM, Safe and Majority vote. The green dashed line [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Average TeraFLOPs per problem on MATH500, AIME’25, CollegeMath, and HardMath2 under [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Distribution of Hermes failures with a fixed translation budget (Kt). @1 @4 @8 Translator sampling (@K) 0% 20% 40% 60% 80% 100% Lean4 Feedback (%) Prover sampling is fixed at @1 Autoformalizer failed to translate Prover failed to prove/disprove (a) Prover @1 @1 @4 @8 Translator sampling (@K) 0% 20% 40% 60% 80% 100% Lean4 Feedback (%) Prover sampling is fixed at @4 Autoformalizer failed to translate Prover … view at source ↗
Figure 7
Figure 7. Figure 7: Distribution of Hermes failures with a fixed prover budget (Kp). B Additional ablation on different combinations of autoformalizers and provers Following the ablation studies presented in [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Illustration of Hermes’s effect on chain-of-thought generation: the model attempts to solve the precalculus-768 problem from the MATH500 dataset, and Hermes detects and corrects a hallucinated reasoning step. C Examples of Hermes corrected problems [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

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

  1. Where to Spend Rollouts: Hit-Utility Optimal Rollout Allocation for Group-Based RLVR

    cs.LG 2026-05 unverdicted novelty 7.0

    HORA adaptively allocates rollouts using hit utility to improve Pass@K over compute-matched GRPO on math reasoning benchmarks while preserving Pass@1.

  2. Case study: proving sqrt(2) irrational with LPTP and an LLM

    cs.LO 2026-07 accept novelty 5.0

    A general-purpose LLM and the LPTP proof checker jointly produced a machine-checked proof that sqrt(2) is irrational, with the checker localizing every wrong step.

Reference graph

Works this paper leans on

57 extracted references · 10 linked inside Pith · cited by 2 Pith papers

  1. [1]

    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. Chain of thought prompting elicits reasoning in large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors,Advances in Neural Information Processing Systems, 2022

    2022

  2. [2]

    Large language models are zero-shot reasoners

    Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors,Advances in Neural Information Processing Systems, volume 35, pages 22199–22213. Curran Associates, Inc., 2022

    2022

  3. [3]

    Metamath: Bootstrap your own mathematical questions for large language models.ArXiv preprint, abs/2309.12284, 2023

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

    Pith/arXiv arXiv 2023

  4. [4]

    Can llms solve longer math word problems better?arXiv preprint arXiv:2405.14804, 2024

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

    Pith/arXiv arXiv 2024

  5. [5]

    Yichen Huang and Lin F. Yang. Winning gold at imo 2025 with a model-agnostic verification-and- refinement pipeline, 2025

    2025

  6. [6]

    A survey on hallucination in large language models: Principles, taxonomy, challenges, and open questions.ACM Trans

    Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, and Ting Liu. A survey on hallucination in large language models: Principles, taxonomy, challenges, and open questions.ACM Trans. Inf. Syst., 43(2), January 2025

    2025

  7. [7]

    Auditing meta-cognitive hallucinations in reasoning large language models

    Haolang Lu, Yilian Liu, Jingxin Xu, Guoshun Nan, Yuanlong Yu, Zhican Chen, and Kun Wang. Auditing meta-cognitive hallucinations in reasoning large language models. InThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025

    2025

  8. [8]

    HalluMeasure: Fine-grained hallucination measurement using chain-of-thought reasoning

    Shayan Ali Akbar, Md Mosharaf Hossain, Tess Wood, Si-Chi Chin, Erica M Salinas, Victor Alvarez, and Erwin Cornejo. HalluMeasure: Fine-grained hallucination measurement using chain-of-thought reasoning. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors,Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages...

    2024

  9. [9]

    Let’s verify step by step

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. InThe Twelfth International Conference on Learning Representations, 2024

    2024

  10. [10]

    Math-shepherd: Verify and reinforce llms step-by-step without human annotations

    Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce llms step-by-step without human annotations. InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2024, Bangkok, Thailand, August 11-16, 2024, pages 9426–...

    2024

  11. [11]

    R-PRM: reasoning- driven process reward modeling.CoRR, abs/2503.21295, 2025

    Shuaijie She, Junxiao Liu, Yifeng Liu, Jiajun Chen, Xin Huang, and Shujian Huang. R-PRM: reasoning- driven process reward modeling.CoRR, abs/2503.21295, 2025

    Pith/arXiv arXiv 2025

  12. [12]

    The lessons of developing process reward models in mathematical reasoning

    Zhenru Zhang, Chujie Zheng, Yangzhen Wu, Beichen Zhang, Runji Lin, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. The lessons of developing process reward models in mathematical reasoning. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar, editors,Findings of the Association for Computational Linguistics: ACL 2025, pag...

    2025

  13. [13]

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024

    Pith/arXiv arXiv 2024

  14. [14]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. 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, Proceedings, page 625–635, Berlin, Heidelberg, 2021. Springer-Verlag

    2021

  15. [15]

    Springer Science & Business Media, 2013

    Yves Bertot and Pierre Castéran.Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013

    2013

  16. [16]

    Springer Science & Business Media, 2002

    Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel.Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002

    2002

  17. [17]

    Formal mathematical reasoning: A new frontier in AI

    Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in AI. InProceedings of the International Conference on Machine Learning, 2025

    2025

  18. [18]

    AI achieves silver-medal standard solving international mathematical olympiad problems

    Google DeepMind. AI achieves silver-medal standard solving international mathematical olympiad problems. https://deepmind.google/discover/blog/ ai-solves-imo-problems-at-silver-medal-level/, 2024. Accessed: 2025-05-08

    2024

  19. [19]

    Solving olympiad geometry without human demonstrations.Nature, 2024

    Trieu Trinh, Yuhuai Wu, Quoc Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations.Nature, 2024

    2024

  20. [20]

    Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.CoRR, abs/2508.03613, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.CoRR, abs/250...

    Pith/arXiv arXiv 2025

  21. [21]

    Kimina-prover preview: Towards large formal reasoning models with reinforcement learning.ArXiv, 2025

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Paga...

    2025

  22. [22]

    Kimina- prover: Applying test-time rl search on large formal reasoning models.https://huggingface.co/blog/ AI-MO/kimina-prover, July 2025

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Ying Zhang, Zhu Zekai, Lu Jian Qiao, Hugues de Saxcéand, Thibaut Barroyer, Ebony Zhang, Bolton Bailey, Frederick Pu, Jonas Bayer, Marina Vinyes, Zhengying Liu, Li Jia, and the AI-MO team. Kimina- prover: Applying test-time rl search on large formal reasoning mod...

    2025

  23. [23]

    Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F

    Huajian Xin, Z.Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z.F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. InThe Thirteenth Internati...

    2025

  24. [24]

    Seed-prover: Deep and broad reasoning for automated theorem proving.CoRR, abs/2507.23726, 2025

    Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zha...

    Pith/arXiv arXiv 2025

  25. [25]

    Mathesis: Towards formal theorem proving from natural languages.CoRR, abs/2506.07047, 2025

    Xuejun Yu, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, and Zhenguo Li. Mathesis: Towards formal theorem proving from natural languages.CoRR, abs/2506.07047, 2025

    Pith/arXiv arXiv 2025

  26. [26]

    Herald: A natural language annotated lean 4 dataset

    Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025

    2025

  27. [27]

    miniF2F: a cross-system benchmark for formal Olympiad-level mathematics, 2022

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics, 2022

    2022

  28. [28]

    Apollo: Automated llm and lean collaboration for advanced formal reasoning

    Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. Apollo: Automated llm and lean collaboration for advanced formal reasoning. InThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025

    2025

  29. [29]

    PhD thesis, University of Washington, 2021

    Talia Ringer.Proof Repair. PhD thesis, University of Washington, 2021. Ph.D. dissertation

    2021

  30. [30]

    Thor: Wielding hammers to integrate language models and automated theorem provers

    Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. InAdvances in Neural Information Processing Systems, 2022

    2022

  31. [31]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models, 2023

    2023

  32. [32]

    A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems.Transactions on Machine Learning Research, 2025

    Roozbeh Yousefzadeh, Xuenan Cao, and Azim Ospanov. A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems.Transactions on Machine Learning Research, 2025

    2025

  33. [33]

    Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification

    Chengwu Liu, Ye Yuan, Yichun Yin, Yan Xu, Xin Xu, Zaoyu Chen, Yasheng Wang, Lifeng Shang, Qun Liu, and Ming Zhang. Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar, editors,Proceedings of the 63rd Annual Meeting o...

    2025

  34. [34]

    Tool learning with large language models: a survey.Frontiers of Computer Science, 19(8), January 2025

    Changle Qu, Sunhao Dai, Xiaochi Wei, Hengyi Cai, Shuaiqiang Wang, Dawei Yin, Jun Xu, and Ji-rong Wen. Tool learning with large language models: a survey.Frontiers of Computer Science, 19(8), January 2025

    2025

  35. [35]

    Toolllm: Facilitating large language models to master 16000+ real-world apis, 2023

    Yujia Qin, Shihao Liang, Yining Ye, Kunlun Zhu, Lan Yan, Yaxi Lu, Yankai Lin, Xin Cong, Xiangru Tang, Bill Qian, Sihan Zhao, Lauren Hong, Runchu Tian, Ruobing Xie, Jie Zhou, Mark Gerstein, Dahai Li, Zhiyuan Liu, and Maosong Sun. Toolllm: Facilitating large language models to master 16000+ real-world apis, 2023

    2023

  36. [36]

    Efficient tool use with chain-of- abstraction reasoning, 2025

    Silin Gao, Jane Dwivedi-Yu, Ping Yu, Xiaoqing Ellen Tan, Ramakanth Pasunuru, Olga Golovneva, Koustuv Sinha, Asli Celikyilmaz, Antoine Bosselut, and Tianlu Wang. Efficient tool use with chain-of- abstraction reasoning, 2025

    2025

  37. [37]

    Wtu-eval: A whether-or-not tool usage evaluation benchmark for large language models, 2024

    Kangyun Ning, Yisong Su, Xueqiang Lv, Yuanzhe Zhang, Jian Liu, Kang Liu, and Jinan Xu. Wtu-eval: A whether-or-not tool usage evaluation benchmark for large language models, 2024

    2024

  38. [38]

    Logic-LM: empowering large language models with symbolic solvers for faithful logical reasoning

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-LM: empowering large language models with symbolic solvers for faithful logical reasoning. InFindings of the 2023 Conference on Empirical Methods in Natural Language Processing (Findings of EMNLP), Singapore, Dec 2023. 12

    2023

  39. [39]

    LOGIC-LM++: Multi-step refinement for symbolic formulations

    Shashank Kirtania, Priyanshu Gupta, and Arjun Radhakrishna. LOGIC-LM++: Multi-step refinement for symbolic formulations. In Bhavana Dalvi Mishra, Greg Durrett, Peter Jansen, Ben Lipkin, Danilo Neves Ribeiro, Lionel Wong, Xi Ye, and Wenting Zhao, editors,Proceedings of the 2nd Workshop on Natural Language Reasoning and Structured Explanations (@ACL 2024), ...

    2024

  40. [40]

    Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth’ee Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding formal theorem provers with informal proofs. InInternational Conference on Learning Representations, 2023

    2023

  41. [41]

    Reviving dsp for advanced theorem proving in the era of reasoning models

    Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. InThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025

    2025

  42. [42]

    Lean-star: Learning to interleave thinking and proving

    Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving. InThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025

    2025

  43. [43]

    Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization

    Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. InThe Twelfth International Conference on Learning Representations, 2023

    2023

  44. [44]

    A read-eval-print-loop for Lean 4

    Lean FRO. A read-eval-print-loop for Lean 4. https://github.com/leanprover-community/repl, 2023

    2023

  45. [45]

    Qwen3 embedding: Advancing text embedding and reranking through foundation models.arXiv preprint arXiv:2506.05176, 2025

    Yanzhao Zhang, Mingxin Li, Dingkun Long, Xin Zhang, Huan Lin, Baosong Yang, Pengjun Xie, An Yang, Dayiheng Liu, Junyang Lin, Fei Huang, and Jingren Zhou. Qwen3 embedding: Advancing text embedding and reranking through foundation models.arXiv preprint arXiv:2506.05176, 2025

    Pith/arXiv arXiv 2025

  46. [46]

    Skywork-reward: Bag of tricks for reward modeling in llms.CoRR, abs/2410.18451, 2024

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

    Pith/arXiv arXiv 2024

  47. [47]

    Interpretable preferences via multi-objective reward modeling and mixture-of-experts

    Haoxiang Wang, Wei Xiong, Tengyang Xie, Han Zhao, and Tong Zhang. Interpretable preferences via multi-objective reward modeling and mixture-of-experts. In Yaser Al-Onaizan, Mohit Bansal, and Yun- Nung Chen, editors,Findings of the Association for Computational Linguistics: EMNLP 2024, Miami, Florida, USA, November 12-16, 2024, pages 10582–10592. Associati...

    2024

  48. [48]

    Rlhf workflow: From reward modeling to online rlhf.arXiv preprint arXiv:2405.07863, 2024

    Hanze Dong, Wei Xiong, Bo Pang, Haoxiang Wang, Han Zhao, Yingbo Zhou, Nan Jiang, Doyen Sahoo, Caiming Xiong, and Tong Zhang. Rlhf workflow: From reward modeling to online rlhf.arXiv preprint arXiv:2405.07863, 2024

    Pith/arXiv arXiv 2024

  49. [49]

    Qwen3 technical report, 2025

    Qwen Team. Qwen3 technical report, 2025

    2025

  50. [50]

    Openai o3-mini.https://openai.com/index/openai-o3-mini/, January 2025

    OpenAI. Openai o3-mini.https://openai.com/index/openai-o3-mini/, January 2025

    2025

  51. [51]

    Deepseek-v3 technical report, 2025

    DeepSeek-AI et al. Deepseek-v3 technical report, 2025

    2025

  52. [52]

    Let’s verify step by step, 2023

    Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step, 2023

    2023

  53. [53]

    Aime problems and solutions — 2025

    American Mathematics Competitions and Art of Problem Solving. Aime problems and solutions — 2025. https://artofproblemsolving.com/wiki/index.php/AIME_Problems_and_Solutions, 2025

    2025

  54. [54]

    Mathscale: Scaling instruction tuning for mathematical reasoning

    Zhengyang Tang, Xingxing Zhang, Benyou Wang, and Furu Wei. Mathscale: Scaling instruction tuning for mathematical reasoning. InForty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net, 2024. 13

    2024

  55. [55]

    Roggeveen, Erik Y

    James V. Roggeveen, Erik Y. Wang, Will Flintoft, Peter Donets, Lucy S. Nathwani, Nickholas Gutierrez, David Ettel, Anton Marius Graf, Siddharth Dandavate, Arjun Nageswaran, Raglan Ward, Ava Williamson, Anne Mykland, Kacper K. Migacz, Yijun Wang, Egemen Bostan, Duy Thuc Nguyen, Zhe He, Marc L. Descoteaux, Felix Yeung, Shida Liu, Jorge García Ponce, Luke Zh...

    2025

  56. [56]

    Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei

    Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models, 2020. 14 Appendices A Prompt and instruction templates # Hermes Tool Instruction Formally validates a **single** reasoning step using a formal Lean4 verifier. Invoke this fu...

    2020

  57. [2025]

    Association for Computational Linguistics. 10

This paper was first reviewed by deepseek-v4-flash on August 3, 2026.