Pith. sign in

REVIEW 4 major objections 6 minor 49 references

Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving

T0 review · 4 major / 6 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 MATH-VF is a training-free framework that translates each step of a math solution into a formal language and verifies every step with an LLM critic backed by SymPy and Z3, outperforming existing LLM-only verifiers on MATH500 and…

desk verdict Plausible stepwise verifier with tool use, but the unverified formalization-preservation assumption and overbroad 'formal verification' framing mean the paper needs major revision before the central claim is supported. read the letter →

arxiv 2505.20869 v1 pith:GG2BKORG submitted 2025-05-27 cs.AI

Kuo Zhou , Lu Zhang This is my paper
classification cs.AI
keywords MATH-VFstep-wiseverificationformalizationofsolutionsLLMmathematicalreasoningprocesssupervisionsolutiongraphsparsitySymPyZ3
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

Large language models make mistakes in multi-step mathematics, and verifying their work with another LLM is itself unreliable. This paper proposes MATH-VF, a training-free framework that first translates a natural-language solution into SimpleMath, a formal language close to ordinary mathematical text, and then uses a tool-integrated LLM critic to judge every step. The paper claims that on MATH500 and ProcessBench, this step-wise formal verification is more accurate than existing training-free verifiers, and that its accuracy remains stable as problem difficulty increases. It also reports that the dependency graph of solution steps is typically sparse, so the critic only needs the few premises relevant to each conclusion, cutting token usage.

What carries the argument

The load-bearing object is SimpleMath, a formal language built as an extension of classical first-order language with additional constants and syntactic sugar, designed so that it closely resembles the natural-language mathematical texts LLMs see during pretraining. A formalized solution is a Fitch-style context of five statement types — facts, assumptions, theorems, definitions, conclusions — which can be transformed into a Solution Graph whose edges mark direct derivation. The paper's key structural observation is that these graphs are sparse: almost every conclusion has at most four premises, so the critic only needs the relevant premises instead of the whole solution, reducing input statements from $n(n+1)/2$ to at most $4n$ in most cases. The critic itself is an LLM agent that, given a judgment $T_i \vdash Q_i$, decides whether it holds by reasoning and by calling SymPy for algebraic manipulation and Z3 for satisfiability of logical constraints.

What would settle it

Take a random sample of solutions from MATH500, have annotators mark whether each SimpleMath translation is logically faithful to the corresponding natural-language step, and compare the Critic's verdicts on the formalizations with human step-level correctness labels; if translation infidelity is common or systematically flips verdicts, the reported accuracy is an artifact of formalization rather than verification.

Watch

Extended reading notes

Core claim

The central claim is that a verifier does not need a complete formal proof to check an LLM's solution; it needs a formal context with small, fillable gaps and a critic that can decide whether each conclusion follows from its premises. The paper introduces SimpleMath, an extension of first-order logic with syntactic sugar for common definitions, and a Fitch-style context that labels statements as facts, assumptions, theorems, definitions, or conclusions. Each solution becomes a Solution Graph, and the critic verifies judgments of the form $T_i \vdash Q_i$, invoking SymPy for symbolic computation and Z3 for satisfiability checks. In experiments on MATH500, MATH-VF's discrimination accuracy ranges from 92.4% to 95.7% depending on the generator, versus 87.9% to 90.6% for a primary critic without tools; on ProcessBench, it trails a large trained process reward model in average F1 (74.1 vs 78.3) but has lower variance across difficulty levels (standard deviation 0.029 vs 0.062). The paper attributes this stability to the decomposition of solutions into fine-grained steps whose individual difficulty does not grow with overall problem difficulty.

Load-bearing premise

The whole framework rests on the assumption that the Formalizer's translation of a natural-language step into SimpleMath preserves the step's logical content, so that the Critic's verdicts on the formal statements are verdicts on the original solution; the paper asserts over 90% of statements are correctly formalized and verified but does not show per-statement evidence.

Editorial extensions

If this is right

  • On MATH500, MATH-VF is claimed to beat a tool-free primary critic by 2.6 to 6.2 percentage points depending on the generator, and to beat the Coq-based formalization baseline by a wide margin, since under 10% of LLM solutions can be fully verified in Coq.
  • Because the method is training-free, it can be used with closed-source models as formalizer and critic, which is not feasible for fine-tuned process reward models.
  • In the candidate-selection task, choosing the solution whose every step passes verification is reported to be more accurate than self-consistency or primary-critic selection.
  • In the refinement task, passing the critic's corrective feedback back to the generator improves accuracy more than self-refinement alone; for example, DeepSeek-v3 rises from 90.1 to 92.4.

Reading between the lines

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

  • If the formalization fidelity claim holds, the same pipeline could be used to generate step-level correctness labels for large datasets without human annotation, since the critic's corrective feedback provides supervision signals.
  • The sparse-graph observation suggests that trained process reward models could also be made token-efficient by feeding them only the relevant premise set, potentially improving their robustness.
  • The method's stability on harder benchmarks hints that a verifier's difficulty should be measured per derivation step rather than per problem; this could inform how benchmarks for process supervision are designed.
  • A natural stress test is to apply MATH-VF to fields like geometry or probability, where SymPy and Z3 do not cover the needed theories and the formalizer may produce expressions the tools cannot parse, a failure mode the paper lists as a limitation.
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 / 6 minor

Summary. The paper proposes MATH-VF, a training-free framework for step-wise verification of LLM-generated mathematical solutions. A Formalizer translates the problem and natural-language solution into a formal context in a proposed language called SimpleMath, producing a sparse solution graph of premises and conclusions; a Critic, built on an LLM augmented with SymPy and Z3, then verifies each formal judgment Ti |- Qi and issues corrective feedback when a step fails. The framework is evaluated on MATH500 and ProcessBench across three tasks: deciding whether a solution is correct, selecting a correct solution from candidates, and refining incorrect solutions. The reported results in Tables 1, 3, and 4 show that MATH-VF generally outperforms training-free baselines such as Primary Critic and Self-Consistency, while Table 2 shows that it has a lower average F1 score than the trained Qwen2.5-MATH-PRM-72B but with smaller standard deviation.

Significance. If the central assumption were established, MATH-VF would be a practically useful contribution: it is training-free, combines LLM reasoning with symbolic tools, and exploits solution-graph sparsity to reduce the input length to the critic. The idea of formalizing each step into a first-order-like language rather than a full ITP proof, thus tolerating small gaps, is sensible and potentially more scalable than Lean/Coq pipelines. The paper also evaluates across multiple generator models and three downstream tasks, which makes the claims falsifiable and gives credit to the empirical scope. However, the significance is currently conditional: the faithfulness of the Formalizer is asserted rather than demonstrated, and the absence of statistical support and the mismatch between the abstract and Table 2 weaken the central claims as they stand.

major comments (4)
  1. [Section 3.1 and Section 4.2]
  2. [Tables 1, 3, and 4]
  3. [Abstract and Section 4.2, Table 2]
  4. [Section 3.2.2]
minor comments (6)
  1. [Section 2.2]
  2. [Figure 5]
  3. [Section 3.1]
  4. [Section 3.1]
  5. [Table 2]
  6. [Section 3.1]

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity; the main caveat is an unverified formalization-fidelity claim, not a definitional loop.

full rationale

MATH-VF's verification accuracy is measured on external benchmarks (MATH500 and ProcessBench), so its success criteria are not derived from the method itself. The token-count reduction C2(n) <= n*M is a direct combinatorial bound rather than a fitted result. The paper contains no load-bearing self-citations by the current authors; references to Zhou et al. are to different authors. The Section 3.1 claim that 'over 90% of the statements ... can be correctly formalized and verified' is asserted without per-statement evaluation or a formal semantics for SimpleMath, so the step from formal-context verdicts to natural-language correctness is an unverified assumption. That is an evidentiary gap and a correctness risk, but it is not circular: the benchmark labels are external, and no parameter is fitted and then renamed as a prediction. Accordingly the circularity score is low.

Assumptions & free parameters 3 free parameters · 4 assumptions · 2 invented entities

This framework rests on empirical assumptions about LLM behavior rather than a closed-form derivation; the formalizable content is an LLM's translation, so there are no fitted mathematical constants. The main assumptions are semantic preservation, tool correctness, and graph sufficiency.

free parameters (3)
  • Number of candidate solutions in task two = 8
    Section 4.1 fixes the candidate count at 8 without sensitivity analysis.
  • Maximum number of premises per conclusion M = 4 (observed bound)
    Section 3.2.2 uses M as an empirical cap from the authors' statistics; no distribution is given.
  • Maximum refinement iterations = not reported
    Section 3.4 mentions a limit but the value is not given.
assumptions (4)
  • domain assumption LLM Formalizer preserves the semantics of the natural-language solution when translating into SimpleMath
    Section 3.1 states formalization accuracy is high but provides no formal semantics or per-statement proof; if translation changes meaning, Critic verdicts do not apply to the original solution.
  • domain assumption SymPy and Z3 return ground-truth results for the formal statements they are asked to check
    The Critic treats tool outputs as authoritative; Section 3.2.1 lists capabilities but no correctness guarantees for the translation from SimpleMath to tool inputs.
  • domain assumption The solution graph identifies all premises relevant to each conclusion, and statements not connected are irrelevant
    Section 3.1 defines the graph and claims sparsity; if a relevant premise is excluded, the Critic could misjudge a step.
  • domain assumption Few-shot prompts are sufficient to make the LLMs follow SimpleMath grammar and invoke tools correctly
    Section 3.1 says LLMs can effectively follow instructions, but no prompt details are provided.
invented entities (2)
  • SimpleMath formal language
    purpose: Formal representation of natural-language solutions for stepwise verification
    A new language designed in this paper; its semantics are described by examples only, and no external formal specification is provided.
  • Solution Graph
    purpose: Sparse dependency structure over solution statements to select premises for the Critic
    Introduced here as a method component; its correctness is assumed, supported only by the authors' internal statistics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving." pith.science (2026). https://pith.science/paper/GG2BKORG

@misc{pith2026250520869,
  author       = {Pith},
  title        = {Pith review of: Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GG2BKORG}},
  note         = {Machine review of arXiv:2505.20869}
}
read the original abstract

Large Language Models (LLMs) have demonstrated formidable capabilities in solving mathematical problems, yet they may still commit logical reasoning and computational errors during the problem-solving process. Thus, this paper proposes a framework, MATH-VF, which includes a Formalizer and a Critic, for formally verifying the correctness of the solutions generated by large language models. Our framework first utilizes a Formalizer which employs an LLM to translate a natural language solution into a formal context. Afterward, our Critic (which integrates various external tools such as a Computer Algebra System and an SMT solver) evaluates the correctness of each statement within the formal context, and when a statement is incorrect, our Critic provides corrective feedback. We empirically investigate the effectiveness of MATH-VF in two scenarios: 1) Verification: MATH-VF is utilized to determine the correctness of a solution to a given problem. 2) Refinement: When MATH-VF identifies errors in the solution generated by an LLM-based solution generator for a given problem, it submits the corrective suggestions proposed by the Critic to the solution generator to regenerate the solution. We evaluate our framework on widely used mathematical benchmarks: MATH500 and ProcessBench, demonstrating the superiority of our approach over existing approaches.

Figures

Figures reproduced from arXiv: 2505.20869 by the authors.

Figure 1
Figure 1. Methods for verifying mathematical reasoning. (a) - (c) from previous work , (d) is our work [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Examle of Fitch-style proof and provide feedback. A step-level Critic dataset MathCritic-76k was proposed to fine-tune a Critic model(Xi et al., 2024) . Recent findings by (Zheng et al., 2024) show that while prompt methods can effectively enable Large Language Models (LLMs) to Critic each solution step by step, existing pro￾cess reward models typically fail to generalize to more challenging math problems beyond GSM… view at source ↗
Figure 3
Figure 3. The overview framework of MATH-VF including a solution formalizer and a tool-integreated critic is [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: On the left side of the figure is a dense Solution Graph, where each statement is direct conclusion of all [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: Prop3 is direct conlusion of Prop1 and Prop2 , [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: The example of critic workflow. In this example, we input context and the conclusion to verify, and then [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

49 extracted references · 16 canonical work pages

  1. [1]

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774

    arXiv 2023

  2. [2]

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433

    arXiv 2023

  3. [3]

    Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. 2011. Automatic proof and disproof in isabelle/hol. In Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011, Saarbr \"u cken, Germany, October 5-7, 2011. Proceedings 8 , pages 12--27. Springer

    work page 2011

  4. [4]

    Cameron B Browne, Edward Powley, Daniel Whitehouse, Simon M Lucas, Peter I Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez, Spyridon Samothrakis, and Simon Colton. 2012. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in games, 4(1):1--43

    2012

  5. [5]

    Yuri Chervonyi, Trieu H Trinh, Miroslav Ol s \'a k, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V Le, and Thang Luong. 2025. Gold-medalist performance in solving olympiad geometry with alphageometry2. arXiv preprint arXiv:2502.03544

    arXiv 2025

  6. [6]

    Debrup Das, Debopriyo Banerjee, Somak Aditya, and Ashish Kulkarni. 2024. Mathsensei: A tool-augmented large language model for mathematical reasoning. arXiv preprint arXiv:2402.17231

    arXiv 2024

  7. [7]

    Leonardo De Moura and Nikolaj Bj rner. 2008. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337--340. Springer

    work page 2008

  8. [8]

    Michael Genesereth and Eric Kao. 2022. Introduction to logic. Springer Nature

    work page 2022

Show all 49 references
  1. [9]

    Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Minlie Huang, Nan Duan, and Weizhu Chen. 2023. Tora: A tool-integrated reasoning agent for mathematical problem solving. arXiv preprint arXiv:2309.17452

    2023 arXiv

  2. [10]

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. 2025. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948

    2025 arXiv

  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. arXiv preprint arXiv:2103.03874

    2021 arXiv

  4. [12]

    G \'e rard Huet, Gilles Kahn, and Christine Paulin-Mohring. 1997. The coq proof assistant a tutorial. Rapport Technique, 178

    1997

  5. [13]

    Ryo Kamoi, Yusen Zhang, Nan Zhang, Jiawei Han, and Rui Zhang. 2024. https://doi.org/10.1162/tacl_a_00713 When can LLM s actually correct their own mistakes? a critical survey of self-correction of LLM s . Transactions of the Association for Computational Linguistics, 12:1417--1440

    2024 doi

  6. [14]

    Muhammad Khalifa, Lajanugen Logeswaran, Moontae Lee, Honglak Lee, and Lu Wang. 2023. Grace: Discriminator-guided chain-of-thought reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 15299--15328

    2023

  7. [15]

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

    2023 arXiv

  8. [16]

    Zicheng Lin, Zhibin Gou, Tian Liang, Ruilin Luo, Haowei Liu, and Yujiu Yang. 2024. Criticbench: Benchmarking llms for critique-correct reasoning. arXiv preprint arXiv:2402.14809

    2024 arXiv

  9. [17]

    Zhan Ling, Yunhao Fang, Xuanlin Li, Zhiao Huang, Mingu Lee, Roland Memisevic, and Hao Su. 2024. Deductive verification of chain-of-thought reasoning. Advances in Neural Information Processing Systems, 36

    2024

  10. [18]

    Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. 2024 a . Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437

    2024 arXiv

  11. [19]

    Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and Andrew C Yao. 2024 b . Efficient neural theorem proving via fine-grained proof structure analysis. arXiv preprint arXiv:2501.18310

    2024 arXiv

  12. [20]

    Liangchen Luo, Zi Lin, Yinxiao Liu, Lei Shu, Yun Zhu, Jingbo Shang, and Lei Meng. 2023. Critique ability of large language models. arXiv preprint arXiv:2310.04815

    2023 arXiv

  13. [21]

    Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al. 2024. Self-refine: Iterative refinement with self-feedback. Advances in Neural Information Processing Systems, 36

    2024

  14. [22]

    Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ond r ej C ert \' k, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. 2017. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103

    2017

  15. [23]

    Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. 2024. Gsm-symbolic: Understanding the limitations of mathematical reasoning in large language models. arXiv preprint arXiv:2410.05229

    2024 arXiv

  16. [24]

    Leonardo de Moura and Sebastian Ullrich. 2021. 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 28, pages 625--635. Springer

    2021

  17. [25]

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

    2023

  18. [26]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. In The 2023 Conference on Empirical Methods in Natural Language Processing

    2023

  19. [27]

    Archit Parnami and Minwoo Lee. 2022. Learning from few examples: A summary of approaches to few-shot learning. arXiv preprint arXiv:2203.04291

    2022 arXiv

  20. [28]

    Shashank Pathak. 2024. Gflean: An autoformalisation framework for lean via gf. arXiv preprint arXiv:2404.01234

    2024 arXiv

  21. [29]

    Aarne Ranta. 2004. Grammatical framework. Journal of Functional Programming, 14(2):145--189

    2004

  22. [30]

    Mohammad Raza and Natasa Milic-Frayling. 2025. Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. arXiv preprint arXiv:2501.16961

    2025 arXiv

  23. [31]

    Jan Frederik Schaefer and Michael Kohlhase. 2020. Glif: A declarative framework for symbolic natural language understanding. In FCR@ KI, pages 4--11

    2020

  24. [32]

    Mingyang Song, Zhaochen Su, Xiaoye Qu, Jiawei Zhou, and Yu Cheng. 2025. Prmbench: A fine-grained and challenging benchmark for process-level reward models. arXiv preprint arXiv:2501.03124

    2025 arXiv

  25. [33]

    Yuhong Sun, Zhangyue Yin, Xuanjing Huang, Xipeng Qiu, and Hui Zhao. 2025. Error classification of large language models on math word problems: A dynamically adaptive framework. arXiv preprint arXiv:2501.15581

    2025 arXiv

  26. [34]

    Maciej \'S wiechowski, Konrad Godlewski, Bartosz Sawicki, and Jacek Ma \'n dziuk. 2023. Monte carlo tree search: A review of recent modifications and applications. Artificial Intelligence Review, 56(3):2497--2562

    2023

  27. [35]

    Vernon Y. H. Toh, Deepanway Ghosal, and Soujanya Poria. 2024. https://arxiv.org/abs/2410.12608 Not all votes count! programs as verifiers improve self-consistency of language models for math reasoning . Preprint, arXiv:2410.12608

    2024 arXiv

  28. [36]

    Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. 2024. https://doi.org/10.18653/v1/2024.acl-long.510 Math-shepherd: Verify and reinforce LLM s step-by-step without human annotations . In Proceedings of the 62nd Annual Meeting...

    2024 doi

  29. [37]

    Self-consistency improves chain of thought reasoning in language models

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations

  30. [38]

    Yaqing Wang, Quanming Yao, James T Kwok, and Lionel M Ni. 2020. Generalizing from a few examples: A survey on few-shot learning. ACM computing surveys (csur), 53(3):1--34

    2020

  31. [39]

    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

  32. [40]

    Zhiheng Xi, Dingwen Yang, Jixuan Huang, Jiafu Tang, Guanyu Li, Yiwen Ding, Wei He, Boyang Hong, Shihan Do, Wenyu Zhan, et al. 2024. Enhancing llm reasoning via critique models with test-time and training-time supervision. arXiv preprint arXiv:2411.16579

    2024 arXiv

  33. [41]

    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

  34. [42]

    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. arXiv preprint arXiv:2408.08152

    2024 arXiv

  35. [43]

    Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2024. Satlm: Satisfiability-aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36

    2024

  36. [44]

    Zhenru Zhang, Chujie Zheng, Yangzhen Wu, Beichen Zhang, Runji Lin, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. 2025. The lessons of developing process reward models in mathematical reasoning. arXiv preprint arXiv:2501.07301

    2025 arXiv

  37. [45]

    Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. 2024. Processbench: Identifying process errors in mathematical reasoning. arXiv preprint arXiv:2412.06559

    2024 arXiv

  38. [46]

    Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. 2024 a . Don't trust: Verify--grounding llm quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations

    2024

  39. [47]

    Lexin Zhou, Wout Schellaert, Fernando Mart \' nez-Plumed, Yael Moros-Daval, C \`e sar Ferri, and Jos \'e Hern \'a ndez-Orallo. 2024 b . Larger and more instructable language models become less reliable. Nature, 634(8032):61--68

    2024

  40. [48]

    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...

  41. [49]

    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.