REVIEW 5 major objections 6 minor 2 cited by
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
T0 review · 5 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash
Pith's one-line read Proof-state exploration drives a 7B Lean prover to 60.74% on MiniF2F
desk verdict Solid engineering contribution to tree-search ATP with a clean data-synthesis pipeline, but the headline gains over baselines are confounded by unmatched search budgets and benchmark-tuned hyperparameters. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is the proof-state exploration loop with constrained decoding over the curated tactic set $T$. $T$ contains the 60 tactic operators that survive a nucleus filter with $P=0.999$ applied to usage frequencies in a large Lean corpus, and every synthetic transition uses an operator from $T$ while premise completion is delegated to the policy model, so the data generator can produce diverse proof steps without needing complete proofs as ground truth. The adaptive beam schedule, which starts wide and linearly decays to a narrow beam as the expansion budget is consumed, converts the broad exploration data into focused proof completion during search.
What would settle it
Take a theorem whose only Lean 4 proof uses a tactic operator outside the 60-tactic set or below the frequency threshold of 0.999, run the full exploration, fine-tuning, and adaptive-beam pipeline on it, and check whether any search succeeds; a failure on such a theorem would show that the curated tactic set is a real ceiling. A separate check is to fix the beam size at its best constant value and compare against the adaptive schedule under the identical budget of one search and 600 expansions, which isolates how much of the reported gain comes from the schedule rather than from the synthetic data.
Extended reading notes
Core claim
The central claim is that a Lean 4 policy model fine-tuned on synthetic proof transitions collected by exploring intermediate proof states can solve formal theorems with one-shot best-first search. Exploration decouples the tactic operator from its premises: at each state, constrained decoding forces the model to sample a batch of operators from a curated set of 60 high-frequency tactics, the same model fills in premises for each operator, and the Lean 4 prover advances the states; the batch deliberately includes low-probability operators that the policy would otherwise never emit. The resulting dataset of roughly 20 million transitions is combined with human-authored Lean library data and used for a single supervised fine-tuning pass, without expert iteration. At search time, an adaptive beam schedule shrinks the beam from a large initial value to a small final value as the number of expansions grows, and each child state is scored by the log-probability of the tactic that produced it plus the parent's score. Under Pass@1 with $K=1$ and $E=600$, the paper reports average success rates of 60.74% on MiniF2F and 21.18% on ProofNet.
Load-bearing premise
The entire pipeline assumes that the 60 high-frequency tactic operators found in the seed corpus are enough to prove the evaluation problems, because any proof requiring an operator outside that set is never generated during exploration and therefore can never be emitted by the trained model.
Editorial extensions
If this is right
- If the central claim is right, one exhaustive exploration pass over existing formalized statements can generate enough proof-step data to train a capable policy, removing the need for repeated expert-iteration loops.
- The adaptive beam schedule implies that fixed beam sizes waste a fixed budget: wide early beams find candidate branches, and narrow late beams stop the search from being trapped in one subtree.
- Because the method records all valid transitions, not just successful proofs, even unsolved or partially solved seeds contribute training data, so data volume scales with search expansion rather than with the number of completed proofs.
- The method depends only on a proof assistant that can check single proof steps, so the same recipe should transfer to other interactive provers once an equivalent high-frequency tactic set is built.
- The reported Pass@1 numbers under a one-search, 600-expansion budget provide a concrete target for later work: any competing tree-search method should be compared at the same expansion count and with the same pass definition.
Reading between the lines
- The 60-tactic set acts as an upper bound on expressiveness: if a benchmark theorem needs an operator outside that set, neither exploration nor the trained policy can ever produce it, so part of the reported success may reflect how well the seed corpus's tactic distribution covers the evaluation benchmarks.
- If the diversity mechanism is the active ingredient, then increasing the exploration budget or the number of seed problems should improve performance most on out-of-distribution benchmarks such as ProofNet; this scaling prediction is testable but not reported.
- The scoring function rates the tactic, not the resulting proof state, so the adaptive beam is a heuristic patch over a weaker signal; a learned value estimator on states might dominate both the fixed and the adaptive schedules.
- The same synthetic-transition data could plausibly be reused as a warm start for reinforcement learning or whole-proof generation, since it exposes the policy to precisely the states where search currently loses budget.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a data synthesis pipeline called proof-state exploration for LLM-based automated theorem proving in Lean 4. Starting from seed problems in the STP dataset, the method uses constrained decoding over a curated set of 60 tactics, followed by premise completion and Lean verification, to generate a large corpus of intermediate proof-state transitions. The resulting data is used to fine-tune Qwen2.5-Math-7B, and at inference the paper proposes an adaptive beam size strategy that starts with a large beam and decays it as search progresses. The authors report Pass@1 averages of 60.74% on MiniF2F and 21.18% on ProofNet under K=1, E=600, claiming these results outperform the tree-search baselines InternLM2.5-StepProver and BFS-Prover. The paper also introduces the DoBeVi REPL and visualization tool and reports confidence intervals for the main results.
Significance. If the empirical claims are substantiated, the paper makes a useful contribution: it describes a concrete, reproducible data synthesis method that goes beyond Expert Iteration by collecting diverse intermediate proof states rather than only successful full proofs, and it releases code and a model checkpoint. The fixed-beam result of 59.51% on MiniF2F at B=8 is itself competitive with strong baselines, and the paper provides confidence intervals, which is good practice. The main scientific value is the demonstration that large-scale synthetic proof-state data can improve the policy model in a one-shot training pass. However, the paper's central attribution claim is currently under-supported because the headline comparison in Table 1 does not isolate the data synthesis contribution from differences in search effort, and the adaptive beam hyperparameters are selected on the test benchmarks.
major comments (5)
- [Section 4.1/Table 1] The statement in Section 4.2 that baselines are evaluated under the same computational budget is not supported by the paper's own budget definition K×B×E. In Table 1, BFS-Prover at B=2 and E=600 spends 1,200 tactic generations per theorem; InternLM2.5-StepProver at B=32 and E=600 spends 19,200; Ours fixed at B=8 spends 4,800; the adaptive schedule for MiniF2F (Bmax=16, Bmin=4, λ=15) spends approximately 2,900; and the adaptive schedule for ProofNet (Bmax=48, Bmin=24, λ=2) spends approximately 18,000. Thus the reported deltas of +5.25 points over BFS-Prover on MiniF2F and +1.29 points over InternLM2.5-StepProver on ProofNet are confounded with total search effort. The paper should report matched-budget comparisons, for example by giving a pass-rate-vs-total-tactic-generations curve for all methods, or by fixing a single total budget and letting each method choose its beam configuration within that budget.
- [Section 4.2 and Appendix A.4] The adaptive beam hyperparameters Bmax, Bmin, and λ are set separately for MiniF2F and ProofNet, and the fixed beam sweep B∈{4,8,16,32} is also reported on the test sets, with no validation split defined. Because the adaptive schedule is tuned per benchmark after seeing test performance, the reported adaptive gains (60.74% vs 59.51% on MiniF2F, 21.18% vs 20.75% on ProofNet) may reflect test-set selection rather than a generally effective search strategy. The paper should specify a validation procedure, or report a single schedule chosen on a held-out set and then evaluated on both benchmarks, to make the adaptive strategy comparison meaningful.
- [Section 3.1 (post-processing)] The decontamination step is described only as using BLEU similarity to remove examples with high overlap with the evaluation benchmarks, but neither the BLEU threshold nor the number of removed examples is reported. Since the final training set comprises approximately 20 million proof transitions drawn from STP and Mathlib, and MiniF2F and ProofNet are small public benchmarks, this omission leaves open the possibility that the reported pass rates are inflated by near-duplicate training examples. The authors should report the decontamination threshold and the quantity of data removed, and ideally verify that no benchmark theorem or close paraphrase appears in the training set.
- [Section 4.2 (experimental design)] No ablation isolates the contribution of the proof-state exploration data synthesis. The comparison against InternLM2.5-StepProver and BFS-Prover changes the base model, the training data, and the search procedure simultaneously, so the superiority of 'Ours (fixed beam size)' does not establish that the synthetic exploration data is the cause of the improvement. A control experiment training the same base model on existing data (for example, STP-only data, or data obtained by rejection sampling on successful proofs) under the same search budget is needed to support the paper's central claim that scalable synthetic data generation is the decisive factor.
- [Section 3.1 and Appendix A.6] The 60-tactic set T is derived by frequency filtering on the STP dataset, but no coverage analysis is reported for MiniF2F or ProofNet. Because data synthesis uses constrained decoding over T, any tactic outside T will never appear in the synthetic training data, and the fine-tuned policy will have low probability of emitting it at inference. The paper asserts that such a curated set is sufficient for the vast majority of problems, but it does not provide evidence. The authors should report what fraction of human-written or baseline-generated proof steps on the two benchmarks use tactics from T, and discuss the resulting completeness limitation.
minor comments (6)
- [Algorithm 1] There is a typo in Algorithm 1: 'lean_prvoer' should be 'lean_prover'.
- [Section 4.1] The phrase 'same search budget' in Section 4.2 is ambiguous because the paper's own metric K×B×E includes the beam size B, which differs across rows; please replace it with an explicit statement of which quantities are fixed (K and E) and which are allowed to vary.
- [Appendix A.2] In the example theorem statement 'amc12a_2009_p6', the type annotation '(m n p q : R) R' appears malformed; it should likely be a single type annotation for the variables.
- [Appendix A.3/Figure 3] The node terminology is inconsistent between the text ('Open Node', 'Error Node', 'ProofFinished Node') and the figure caption ('Internal', 'Proof', 'LeanError'); please unify the labels.
- [Section 1] The sentence 'An fundamental cause is that LLMs are typically trained for general-purpose language understanding' contains a grammatical error ('An' should be 'A').
- [Appendix A.7] Figure 5 includes a curve for B=2, but Table 1 does not report a fixed-beam result for B=2 for the proposed model; please clarify whether this configuration was evaluated and, if so, why it is omitted from the main table.
Circularity Check
Adaptive-beam headline is tuned on the evaluation benchmarks, but the data-synthesis core is independently supported.
-
fitted input called prediction
[Section 4.2 / Appendix A.4 (Eq. 2, Table 1)]
"the optimal beam sizes for our policy model are found to be 8 on MiniF2F and 32 on ProofNet, respectively. By adopting our adaptive beam size strategy, we are able to further improve performance without searching for the best beam size settings. ... Regarding the choice of hyperparameters in the adaptive beam size strategy, we set Bmax = 16, Bmin = 4, and λ = 15 for MiniF2F, and Bmax = 48, Bmin = 24, and λ = 2 for ProofNet."
The adaptive beam size strategy is presented as a general method that improves performance 'without searching for the best beam size settings,' but Appendix A.4 reports per-benchmark hyperparameters (Bmax, Bmin, λ) that are set separately for MiniF2F and ProofNet. No held-out validation split is described, so these values are effectively selected on the same benchmarks used for the reported Pass@1 numbers. The adaptive results (60.74% on MiniF2F, 21.18% on ProofNet) are therefore evaluations of a configuration fitted to the target benchmarks, not independent predictions of a fixed strategy. This makes the claimed adaptive-beam improvement partly an artifact of test-set tuning rather than a derivation from the method itself.
full rationale
The core data-synthesis contribution is not circular: proof states are generated by constrained decoding over a 60-tactic set, verified by Lean, and then used to fine-tune a policy that is evaluated against external baselines. The fixed-beam results (e.g., 59.51% at B=8 on MiniF2F and 20.75% at B=32 on ProofNet) provide independent evidence that the synthetic-data approach works, and the paper contains no load-bearing self-citation chain or imported uniqueness theorem. The genuine circularity is confined to the adaptive-beam headline: Appendix A.4 fixes Bmax/Bmin/λ separately for each benchmark, and Section 4.2 presents the resulting Pass@1 as a general strategy achieved 'without searching for the best beam size settings.' That is test-set selection presented as a prediction, so the adaptive gains are partially constructed by the choice of hyperparameters. Separate non-circular concerns include the unequal tactic-generation budgets in Table 1 under the paper's own K×B×E accounting, and the coverage limitation of the 60-tactic set; these are correctness or robustness issues rather than circularity. Overall, because the central synthetic-data claim retains independent fixed-beam support, the circularity is partial rather than total.
Assumptions & free parameters
free parameters (15)
- alpha (pruning ratio) =
0.25
- beta (top branches kept) =
not specified numerically
- gamma (budget reduction factor) =
0.9
- exploration beam size B =
32
- nucleus threshold P for tactic filtering =
0.999
- adaptive beam Bmax (MiniF2F) =
16
- adaptive beam Bmin (MiniF2F) =
4
- lambda (MiniF2F) =
15
- adaptive beam Bmax (ProofNet) =
48
- adaptive beam Bmin (ProofNet) =
24
- lambda (ProofNet) =
2
- search expansion budget E =
600
- global timeout =
1800 seconds
- tactic execution timeout =
20 seconds
- early termination threshold =
0.5 times beam size
assumptions (5)
- domain assumption The curated 60-tactic set T is sufficient to prove the vast majority of MiniF2F and ProofNet problems.
- domain assumption The STP seed dataset provides a representative distribution of proof states for the target benchmarks.
- domain assumption Fine-tuning a 7B LLM on the synthesized transitions improves its pass rate in proof search.
- domain assumption The scoring function log P(t|s) correlates with progress toward proof completion.
- domain assumption Exploration-generated proof states are a valid training signal even without proof completion.
invented entities (1)
-
DoBeVi REPL
independent evidence
Cite this review
Pith. "Pith review of LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation." pith.science (2026). https://pith.science/paper/72EFKVXW
@misc{pith2026250512031,
author = {Pith},
title = {Pith review of: LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation},
year = {2026},
howpublished = {\url{https://pith.science/paper/72EFKVXW}},
note = {Machine review of arXiv:2505.12031}
}
abstract
Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.
Figures
Figures from the paper (2 more)
Forward citations
Cited by 2 Pith papers
-
Search Hardness-Aware LLM-Based Problem Formulation for Expensive Simulation-Driven Design
SHA-PF uses initial simulation data to select a 'hard but promising' anchor satisfaction state and evolves LLM-generated formulations that prioritize it, reaching target designs with fewer expensive simulations on ant...
-
ProofCompass: Enhancing Specialized Provers with LLM Guidance
A hybrid method uses LLM-generated proof strategies and lemma selection to raise a specialized Lean prover's miniF2F pass rate to 55.3% at 128 attempts, above the baseline's 54.9% at 3200 attempts.
Reference graph
Works this paper leans on
-
[2]
Large language models for mathematical reasoning: Progresses and challenges
Janice Ahn, Rishu Verma, Renze Lou, Di Liu, Rui Zhang, and Wenpeng Yin. Large language models for mathematical reasoning: Progresses and challenges. arXiv preprint arXiv:2402.00157,
-
[3]
Large language model-based agents for software engineering: A survey
Junwei Liu, Kaixin Wang, Yixuan Chen, Xin Peng, Zhenpeng Chen, Lingming Zhang, and Yiling Lou. Large language model-based agents for software engineering: A survey. arXiv preprint arXiv:2409.02977,
-
[4]
Niklas Muennighoff, Zitong Yang, Weijia Shi, Xiang Lisa Li, Li Fei-Fei, Hannaneh Hajishirzi, Luke Zettlemoyer, Percy Liang, Emmanuel Candès, and Tatsunori Hashimoto. s1: Simple test-time scaling. arXiv preprint arXiv:2501.19393,
-
[6]
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 28, pages 625–635. Springer,
2021
-
[7]
URL https://arxiv. org/abs/2504.21801. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640,
-
[8]
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024a. Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu,...
-
[9]
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, and Jingbo Shang. Learn from failure: Fine-tuning llms with trial-and-error data for intuitionistic propositional logic proving. arXiv preprint arXiv:2404.07382,
-
[10]
Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024b. 11 Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematic...
arXiv 2020
Show all 30 references
-
[13]
Autofor- malizing euclidean geometry
Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autofor- malizing euclidean geometry. arXiv preprint arXiv:2405.17216,
-
[14]
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393,
2009 arXiv
-
[15]
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344,
-
[16]
Internlm2
Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700,
-
[17]
Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438,
-
[18]
Lexically constrained decoding for sequence generation using grid beam search
Chris Hokamp and Qun Liu. Lexically constrained decoding for sequence generation using grid beam search. arXiv preprint arXiv:1704.07138,
-
[22]
Leanabell-prover: Posttraining scaling in formal reasoning
Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttraining scaling in formal reasoning. arXiv preprint arXiv:2504.06122,
-
[23]
Kimina-prover preview: Towards large formal reasoning models with reinforcement learning
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025a. Ruida...
-
[24]
arXiv preprint arXiv:2406.01940,
-
[25]
Lego-prover: Neural theorem proving with growing libraries
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656,
-
[26]
Deepseekmath: Pushing the limits of mathematical reasoning in open language models
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300,
-
[27]
13 A Appendix A.1 Prompts used for policy model For the policy model, we use the similar prompt template as in GPT-f [Polu and Sutskever, 2020], where the prompt only describes the current proof state without introducing any additional information. The template and an example ...
2020
-
[28]
search tree
:= by norm_num rw [h3] field_simp [Real.log_mul, Real.log_rpow, mul_assoc] ring_nf ] 14 Example: Rudin_exercise_4_11a in ProofNet theorem exercise_4_11a {X : Type*} [MetricSpace X] {Y : Type*} [MetricSpace Y] (f : X → Y) (hf : UniformContinuous f) (x : N → X) (hx : CauchySeq x...
2023
-
[29]
or the lemma library construction approach in Wang et al. [2023]. An ineffective scoring function. One major drawback of tree search methods compared to whole- proof methods lies in the complexity of the neural-symbolic system: it involves many interacting components, making i...
2023
-
[30]
Moreover, the empirically optimal beam size varies across benchmarks and is not a fixed value
can sometimes unlock greater potential from the policy model. Moreover, the empirically optimal beam size varies across benchmarks and is not a fixed value. • Other budget-related factors. These include parameters like K, E, and the timeout threshold. Compared to the previous ...
2024
-
[2017]
Qwen2.5-math technical report: Toward mathematical expert model via self-improvement
An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, Keming Lu, Mingfeng Xue, Runji Lin, Tianyu Liu, Xingzhang Ren, and Zhenru Zhang. Qwen2.5-math technical report: Toward mathematical expert model via se...
-
[2020]
ISBN 9781450370974
Association for Computing Machinery. ISBN 9781450370974. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145/3372885.3373824. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large langua...
-
[2021]
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023a. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Pas...
-
[2022]
Lean workbook: A large-scale lean problem set formalized from natural language math problems
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847,
-
[2023]
Lean-star: Learning to interleave thinking and proving
12 Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040,
-
[2024]
Puzzle solving using reasoning of large language models: A survey
Panagiotis Giadikiaroglou, Maria Lymperaiou, Giorgos Filandrianos, and Giorgos Stamou. Puzzle solving using reasoning of large language models: A survey. arXiv preprint arXiv:2402.11291,
-
[2025]
Towards system 2 reasoning in llms: Learning how to think with meta chain-of-though
Violet Xiang, Charlie Snell, Kanishk Gandhi, Alon Albalak, Anikait Singh, Chase Blagden, Duy Phung, Rafael Rafailov, Nathan Lile, Dakota Mahan, et al. Towards system 2 reasoning in llms: Learning how to think with meta chain-of-though. arXiv preprint arXiv:2501.04682,
Reviewed August 15, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.