Lean-STaR: Learning to Interleave Thinking and Proving
Authors: Haohan Lin
Zhiqing Sun
Sean Welleck
Yiming Yang
Venue: ICLR 2025 Spotlight (2025)
Keywords: Automated Theorem Proving
Chain-of-Thought
Reinforcement Learning
Reasoning
Primary area: reinforcement learning

Abstract: Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, a model will learn to prove theorems. Our key observation is that a wealth of informal information that is not present in formal proofs can be useful for learning to prove theorems. For instance, humans think through steps of a proof, but this thought process is not visible in the resulting code. We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof, thereby boosting the model's theorem-proving capabilities. Lean-STaR uses retrospective ground-truth tactics to generate synthetic thoughts for training the language model. At inference time, the trained model directly generates the thoughts prior to the prediction of the tactics in each proof step. Building on the self-taught reasoner framework, we then apply expert iteration to further fine-tune the model on the correct proofs it samples and verifies using the Lean solver. Lean-STaR significantly outperform base models (43.4% → 46.3%, Pass@64). We also analyze the impact of the augmented thoughts on various aspects of the theorem proving process, providing insights into their effectiveness.

Published as a conference paper at ICLR 2025
LEAN-STAR:
LEARNING TO INTERLEAVE THINKING AND PROVING
Haohan 2
Zhiqing Sun
Sean Welleck!
Yiming Yang!
'Language Technologies Institute, Camnegie Mellon University
Institute for Interdisciplinary Information Sciences, Tsinghua University
Thachanl, ngs, swel leck, yimi ng] êcs cemu.edo
https://leanstan gitturr..g.g.u......g 1o/
ABSTRACT
Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, model will learn to prove theorems. Our key observation is that wealth of informal information that is not present formal proofs be useful for learning to prove theorems. For instance, humans think through steps of a proof, but this thought process is not visible in the resulting code. We present Lean-STaR, framework for training language models to produce informal thoughts prior to each step of proof, thereby boosting the model's 's theorem-prowe capabilities. Lean-STaR uses retrospective ground-trufe tactics generate synthetic thoughts for training the language model. At inference time, the trained model directly generates the thoughts prior the prediction of the tactics in each proof step. Building on the self self-taught reasoner framework, we then apply expert iteration to further fine-tune the model on the correct proof' it samples and verifies using the Lean solver. Lean-STaR significantly outperforming base models (43.4% - 46.3%, Pass @64) 64). We also analyze the impact of the augmented thoughts various aspects of the theorem proving process, providing insights into their effectiveness.
INTRODUCTION
Theorem proving is fundamental aspect of mathematics, and mathematical reasoning is an important part of artificial intelligence (Newell & Simon| 1956 Zhou| 2023). Formalized mathematics in particular provides challenging testbed for assessing mathematical reasoning capabilities. Since theorems and proofs in this setting can represented the form checkable source code, is easy to evaluate proofs of arbitrary complexity (De Moura et al. 2015). Automated theorem proving, if successful, can also help discover unknown errors in previous proofs and make it casier to guarantee that new proofs correct. More broadly, formal mathematics coupled with powerful automation may unlock new forms of education and collaboration, mathematical insights, and applications to
verifying critical software (Avigad) 2023
First 2023
Buzzard 2024 of Sciences 2023
Recently, language models have shown promising progress in formal theorem proving (Polu & Sutskever 2020; Rabe al.) 2020 Wu et al. 2021 Han et al. 202 Lample et al. 2022 Yang
et al. 2023 Li et al. 2024). Existing approaches typically train a model solely based on the proofs
formal language (code) such as Lean (De Moura al. 2015). Isabelle (Nipkow al. 2002).
or Coq (Coq) 1996). Our key observation is that such approaches ignore wealth of informal
information that may be useful for learning to prove theorems (Welleck et al., 2021
2022 For
WWok done during the visit at CMU.
For example, Terence Tao found non-trivial error while using Lean formalize project Tao 2023

---

Published as a conference paper at ICLR 2025
Thought-augmentedd Tactic Prediction (Lean-STaR)
Direct Tactic Prediction (SFT)
Input Leaa State
Input- Lean State
h.
Net-Ica Ien 120 3720
649 State
P.
Hat. ped 120 5
Nat 120
e 2410
Oulput Natural Language Thought
Reasentig specific
"b" from the diviser (GCD) and teast conson suttiple (UCN) with '128" need to relate the gives 600 the LOs, recognizing the fundamental theoren of groatest conson divisors which relates LOK to GCD is way. enable to establish an equation invelving facilitating the identification algebraic nesioulatior.
hypotheses about greatest comaon
Output Lean Tactic
Asd hext tactic:
have Nat. aod, 120
Output Lean Taclic
Mest get
Figure 1: The illustration of tactic prediction in one proof step with and without thought.
instance, the underlying thought process prior each step of proof is not present in formal source code. Based on this insight, we propose to train a language model that can produce a natural language chain-of-thought ("thought")) prior to each step ("tactic") of formal proof.
We introduce Lean-STaR, a framework for learning to interleave informal thoughts with steps of formal proving. Building on the Self-Taught Reasoner (STaR) framework (Zelikman al. (022).
we enable language models to interleave step-by-step rationales (i.e., thoughts) (Nye et al. 202
Wei et al., 2022) with formal proving
two-stage process. In an initial phase, we prompt sufficiently capable language model, such as GPT-4 (Achiam et al. (023). and generate retrospective thoughts based on dataset of human- wwriten proofs, such as Mathlib, the largest collection of human- written proofs in Lean (mathlib Community 2020). Subsequently. we fine-tune
tactic predictor (Bohme & Nipkow| 2010 Blanchette et al., 2016 Gloeckle et al. 2023] Czajka & Kaliszyk 2018) that, given a Lean state, can generate a thought and predict the subsequent tactic. In second phase, we optimize this thought-augmentte
tactic predictor with the expert iteration algorithm (Anthony et al. 2017: Singh et al. 2023), using multi-step success rate in theorem proving as the reward.
Our work presents new link between informal and formal mathematics, complementary to prior explorations that translate standalone mathematical statements (Szegedy) 20200 Wang et al. 2020
Wu et al. 2022) translate informal proofs into formal proofs (Agrawal al. 1022]Jiag et al.
2022;
Azerbayev et al.) 2023a] Zhou et al.) 2024a] Huang et al. (024).. Lean-STaR generates
natural language thoughts specifically for each proof step, improving formal proving capabilities by interleaving natural and formal languages.
We instantiate Lean-STaR by generating roughly 50,000 thought-augmentee examples from Lean's Mathlib (mathlib Community/ (2020), then synthesize an additional 50k examples through two iterations of expert iteration. To the best of our knowledge, this yields the first thought-augmenter dataset for theorem proving. After fine-tuning an InternLM2-76 base model (Ying et al. (024) on our -agggete data, our final STaR model can solve 34.8% (pass@32) or 36.1 % (pass@ @ 64) of the problems on miniF2F-test (Zheng et al. 2021). Using stronger base model MiermLLM2-7b-plus. Lean-STaR can achieve 45.4% (pass@32) 32), significantly surpassing the previous results of 43.4% (pass @ 32). In summary, Aean-STaR offers framework for teaching language models to interleave informal thoughts with formal verification, advancing the capabilitics of language models in automated theorem proving.
RELATED WORK
Automatic Theorem Proving & Autoformalization. Previous work on learning- bearning-based theorem proving typically follows the GPT-f framework (Polu & Sutskever (020), which trains a language model on (proof state, next-tactic) pairs, then proves theorems by using the model within a best-first tree search. Subsequent work has explored several directions, including data augmentation (Han
2

---

Published as a conference paper at ICLR 2025
et al. 2022), novel proof search methods (Lample e et al. 2022] Wang et al. 2023b), further training
through curriculum learning (Polu et al. 2022). retrieval augmentation Yang et al. (023). or practical
tools (Welleck & Saha, 2023). Others use prompted models to generate tactics (Azerbayev et al. Thakur
(T23k et al., al.]|2223 (023), or fine-tune models to generate a full proof (First et al. 2023). second fomollaomaiiztaioon Wu et al. 2022) thread incorporates informal mathematics into formal theorem proving. Draft-Sketch-Pron
@Jiang et al.) 2022) shows that language models have some ability to use informal proofs improve model's formal proving abilities, by drafting an informal proof, translating into a formal proof sketch, then completing the proof with tools like Sledgehammer (Bohme& Nipkow| 2010). Seett-Skecch-rroee and related methods (Wang al. 2023a Zhao et al.) 20ou et al. 2024b) are limited to the Isabelle prover, since they use powerful automatic proving tools like Sledgehammer. Lean lacks these tools, so generating the entire proof at once would be more unlikely in Lean. We focus on Lean, and train language models to generate thought and predict the subsequent tactic each proof step. To the best of our knowledge, we are the first to introduce thought-augmented reasoning in automatic theorem proving.
Rationale-augmented Reasoning. Recently, many works demonstrated that letting language models reason before an answer can improve their performance on tasks including math, science, and code (Nye et al. 2021] Wei et al. [2022] Chen al. 2022). Although the corresponding techniques (e.g., Scratchpad and
-hio-hhf-Thhhhh have proven to be effective, they require either extensive annotated training examples or exposure to numerous similar examples during pre- pre-training (Brown et al.) (020). The scarcity of natural language reasoning in formal theorem proving, coupled with the impracticality of manually annotating rationales for formal mathematics, thus presents a challenge. We propose a new Lean-STaR framework for synthesizing training examples by taking advantage of the correctness signal from the formal system.
Bootstrapping Language Model Reasoning. Recently, several works suggest that language models may be taught to reason via synthetic data that they generate themselves, akin to reinforcement learning method that improves a policy through self-play. Polu et al. (2022) showed that a simple RL algorithm, expert iteration, paired with currieulum learning model. Self-Taught Reasoner (STaR) (Zelikman et al. 2022) showed that we can iteratively fine-tune the language model on the correct (reasoning, answer) pairs generated by itself to gradually improve performance. Singh et al. (2023) proposed ReST-EM, which filters data generated by language model with a binary feedback signal rather than using fully manually annotated data (similar to expert iteration in (Polu et al. 2022)). Our work builds on these ideas, providing the first study of bootstrapped thought-augmentte proving.
improve formal theorem proving
3 OUR METHOD: LEAN-STAR
We introduce Lean-STaR, new method for combining informal thoughts with formal theorem proving. First, we recap interactive theorem proving ($3.I). Then we present Lean-STaR's data- generation (.... $32.22 and reinforcement learning ($3.2.3 phases. Finally, we present our evaluation protocols 3.3
3.1 PRELIMINARIES
Interactive Theorem Provers (ITPs) are typically used for step- sep-by-step automatic theorem proving in formal mathematics. At each step, we can provide the ITP with a high-level "tactic" to simplify the current goal state (e.g., the initial goal theorems to be proven) into subgoals. These subgoals will form new states, and proving all the subgoals results a complete proof of the given theorem. We use Lean De Moura et al. 2015)), a popular interactive theorem prover. An example formal proof in Lean and its explanation are shown in Appendix D
3.2 DATA GENERATION & TRAINING
We describe the data generation and training of the direct tactic prediction model (SFT), the thought- augmented tactic prediction model trained with synthetic data (Lean-CoT), and the final model trained with expert iteration SeaR..
3

---

Published as a conference paper at ICLR 2025
Tactic
doca
have h
Nat. get.:gedd_laaiaaaeee Lea 120
Not. loe 120 b 1720 Mat god 120 216
Bac: les 130 2030
240
detereiie specifie value 's frem cives fucetheses about its greatess commoy
Thought
the LON, recagrizing the Surmeentta theree cowstest
siss 128
colate the given G2D
Ressensng
the given stillitie hi Not les 128 with hes ges 120 the preduct of the greatess commas diviser comes waltiple the
in spocific viy. this eill evaie
eetabhisn squation snuglxing Pactiitattng identificttio sinisiatton
Taetic
[ho, h.] h
Thougls
[gea) namters pcoduct the suabuss, This auspurky given te "b" facsistating the secivation the destzed equality.
Tacti
Gool
nlinarith
No goals!l1
Not ged 128 6
Thouget
3120 120
vs Dessoning
prove
fepothests that cansen stutase (gea) 120 and
Geoa
simplify the equation x 5725 118 5 to 5726 80 15 b.,
considering
hsis sisplirication will snabls disses salculacion
Figure 2: An example of Lean proof and thoughts generated by Lean-STaR. Note that there is a calculation error in the thought (in red), but this does not affect the correctness of the proof because the calculation task is actually completed by the interactive theorem prover (i.e., Lean's nlinarith) instead of the language model. This shows a benefit of combining neural and symbolic systems.
3.2.1 DIRECT TACTIC PREDICTION
We define the theorem- prrovin-proving problem as a Markov Decision Process (MDP) (S, Pa, Ra) where proof states serve states in MDP and tactics serve actions. From this perspective, proof is trajectory ($1, 01, r1), ($2; 022 r2), .. of states $,, tactics a; and rewards r; E R. and the ITP (e.g.. Lean) provides each new state 81+1-
In the typical setting (Polu& & Sutskever, 2020). proving a theorem consists of providing a proof state to the language model and then generating tactic from the language model M, i.e., TM (als). The language model can be fine-tuned for this task using a dataset of (proof state, next-tactic) pairs from successful proof trajectories, i.e. D {(s a²) i 1,... M). where final states have reward of 1. We refer to a language model fine-tuned on such dataset as a supervised fine-tuning (SFT) model.
3.2.2 THOUGHT-AUUMENTTO TACTIC PREDICTION
Existing approaches typically train only on formal states and tactics (Polu & Sutskever 2020). We hypothesize that incorporating a latent thought can improve a model's ability to predict the next tactic. Formally, we introduce a hidden "thought" variable t, prior each tactic, and then extend the model to the form a (a,, t, (/|s;) = TM (a: [,, s.)T (t)]s)). In thought-augmenteed tactic prediction, the distribution over the next tactic can then be expressed as:
(ails))
Σ mi((altt,
The key challenge is obtaining (state, thought, tactic) pairs for training a model. To this end, we introduce retrospective rationale generation. Our motivating observation is that the distribution of natural language thoughts in theorem theorem-proving T (f, (s:) is scarce in the pre-training corpus of large language models. In turn, we find that even the most powerful GPT-4 model does not perform well in generating the correct rationale through few-shot prompting (Brown et al., 2020). To develop language model capable of generating thoughts and tactics ds; 4 we need an entirely new dataset Dr = {(s', 12, a²) i l,... N). However, in Lean, we only have a dataset of Dg {(s', a²) i = 1,... .N) where (s', a²) is one step in some successful proof trajectories.
Given a powerful large language model G, which we refer to as the oracle mode we give the oracle
For instance, in our experiments use the best available large language model, GPT-4
4

---

Published as a conference paper at ICLR 2025
Base Dataset
CoT Dataset
Retrospective Bationale
Generation
Expert Iteration
STaR dataset
GFT-4
Leah-CoT
Finetune
Expert Iteration
Base Modial
Finetune
SFT Rodel
Finetune
Sean-STaB
Figure 3: The diagram of pipeline. (1) Produce CoT dataset through GPT-4. (2) Fine-tune the SFT model with the CoT' dataset to obtain Lean-CoT. (3) Use expert iteration to generate the STaR dataset through the model in the last iteration (Lean-CoT in the first iteration) and then fine-tune Lean-CoT on the updated STaR dataset to obtain the model in the next iteration. We continue performing this step until stopping condition is met (e.g., fixed number of iterations).
model the ground-truth tactic a, and let the oracle model produce the thought t; given the current state s, and ground-truth tactic a,. This helps improve the pass rate and produce data more efficiently. Our few-shot prompt is provided in Appendix G The design principle of the prompt is to prevent the oracle model from generating hindsight-likk like thoughts.
We randomly select M pairs (s', .a) E Ds Then the oracle model is used to produce a thought t' for each pair (s',a") a²) to create new dataset i tt,, a') i 1, ... .M). With this retrospectively annotated dataset by the oracle model Dr, we obtained our first thought-augmenteed tactic prediction model, Lean-CoT, by fine-tuning from the SFT model.
3.2.3 BOOTSTRAPPING THOUGHT-AUGMENTE THEOREM PROVING
We propose to apply expert iteration to further improve the performance of Lean-CoT. Specifically, we start from the initial Lean-CoT model Mo and the initial dataset D {s² i 1....... }. which consists of all initial states s² of the theorems to be proved. In iteration 1, we use model M sample K times per problem. Each time the model will produce a proof trajectory [(s, to, ao). (s1, f1, a.).... (8n, Iu, an)]. Then we create a new dataset D1 by filtering the gener- ated trajectories to include only the successful ones. De-duplication is then applied to the collected trajectories. Now, we can further fine-tune the SFT model M on dataset DT U Dj to produce Lean-STaR model M1. Then we can use M1 as initial model to produce dataset D2 and further fine-tune to obtain model M2 in the next iteration.
This method can be seen as an offline RL method (Singh et al. (023) in the theorem proving MDP. In this MDP, the cumulative reward R ((so, tg, ag), (31, &1, a1), (Sn: Ens a,)) = 1 if and only if the proof trajectory is successful. The total expected reward is
JMM, D)
Σ E(so, (eat ((sp, lo, ao). (8n, bn, an)),
and LeaR-STaR's expert iteration can be seen optimizing this reward (Singh et al. 2023
3.3 EVALUATION
Setup. We evaluate the model on formal theorem proving - given a theorem statement, produce a theorem that is correct according the formal system. This requires algorithm for producing full proof by interacting with Lean. As a new form of theorem-proving system, it is unclear what the best strategy is when have informal thoughts. Our preliminary experiments indicate that best-first search with beam search does not work well for the thoughts in the natural language format. Thus we describe the traditional strategy (best-fire first search), and new approach based sampling.
5

---

Published as a conference paper at ICLR 2025
Sampling =
Best-First Search (K= 1)
State (Fooo)
(Root) log 1st expanded
Jegar
legal
logal
illegll
log p-0.3 pw0.7
log p=1.4
lllggl
State 2 log p 0.7 3rd expanded
State
illegal
State
log p 2nd expanded
log p 1 Snd expanded
Suipped
logai
lecal
logai
log 1.5
log p 0.8
State log -1.0 expanded
State 6 Ing p Gnd expended)
Stare
Statte 5
log p 7nd expandedd
lopal
logal
Figure 4: The visualization of Best-first Search (K = 1) and Sampling (S = 1). Search method maintains search tree and explores S tactics each expanded node. Sampling method explores K tactic trajectories from the root and ignores illegal tactics in the trajectories.
Best-First Search. The most popular method to evaluate the theorem proving ability of language model M is to use best-firs first search like GPT-f (Polu & Sutskever, 2020 Yang et al., [2023] Azerbayey al. 2023b Welleck & Sahal 2023). In best-first search, we keep all unexpanded states 8,. Each time, we expand the "best" state 8; and use the language model to sample S next tacties a1,1.. for the current state 8g. For each legal tactic 0g
state can be obtained by applying tactic ag on state s;. Following standard practice (Polu & Sutskever] 22000 Yang et al. [023) Welleck & Saha 2023). we assume the state with maximum negative log- probabilities is the "best"s. Specifically,
select state 8; with maximum
logp(a,, 8y), where (o), " (8;-1, 01-1 the proof
trajectory before state 83 and log p(a,. 8y) is the average log probability of each generated token. We expand up to N states and we get successful proof search when reach any proof state with no goals. Then, we can attempt the search K times to obtain a pass rate pass@K. However, we found that the best-first search method performed poorly in the Lean-CoT and Lean-STaR models, as detailed in the Appendix [ We attribute this to using average log probabilities, which may not be a reliable quality indicator when the thought sequence ty is generated.
Sampling. Motivated by these issues with applying best-first search to thought-aagmenttd proving, we develop a new method based on sampling trajectories in parallel. Specifically, our method samples K times in parallel for each problem, each time generating at most N tactics. Also, illegal sampled tactics will be ignored during sampling. Specifically. in a sample, suppose our current state s; the proof trajectory before is (Sp, ag), ........... (s;-1, a;-1) 1) and the sampled tactic is a; If a, is legal tactic, (8s, az) will be added to the proof trajectory and we will reach a new state obtained by applying tactic 0z,j on state s;. Otherwise, we ignore this a; and use language model M to sample new tactic given state st. We limit the number of times a tactic can be generated by language model M to a total of N per time in K sampling times. The sampling method is roughly equivalent to the search with S 1. except that the sampling ignores illegal tactics. We assume that in the sampling method we have S 1. In this setting, evaluating took approximately the same amount of GPU time. This sampling method can easily accommodate hidden variable "thoughts" 1z. Figure compares fert-first search and sampling method.
sampling method and best-first search with equal S K

---

Published as a conference paper at ICLR 2025
Table Pass rates on the minif2f-test and Leandojo dataset with Lean. This table shows the pass rates of previous works and our work. S is the number of tactics attempted at each expanded node (assumed be 1 in sampling) and K the total number of search or sampling attempts per problem. In sampling we use temperature 0.7, and in search we use beam search when generating the next tactic. We use a random subset of Leandojo4-v9ttest (novel premises) with size of 320 as test set of leandojo. Note that we sample 32 examples twice when K 64 in sampling.
APPROACH
DECODING
N
K
S
MINIFFF
LEANDOJO
GPT-3.5
ACHIAM
2023
(FEW-SHOT)
SAMPLING
50
1
1
2.8%
GPT-4
ACHIAM ET AI..
2023
(FEW-SHOT)
SAMPLING
50
1
11.9%
TRANSFORMER Polu ET AL.
2022
(W/o RL)
SEARCH
512
1
8
24.6%
LLEMMA-34B
AZERBAYEV AL.
2023B
SEARCH
50
32
25.8%
LLEMMA-7B
AZERBAYEV ET AL.
2023B
SEARCH
50
32
26.2%
REPROVER YANG
2023
SEARCH
50
64
26.5%
TRANSFORMER POLU EY AL..
2022
(W/ RL)
SEARCH
512
29.6% 8
INTERNLM2-344 YING ET AL.
2024
SEARCH
50
32
29.5%
COPRA (WITH GPT-4)
ET AL.
2023
CUSTOMIZED
29.9%
COPRA (WITH GPT-4)
THAKUR ET AL.
2023
CUSTOMIZED
100
30.7%
INTERNLM2-7B YING ET AL.
2024
SAMPLING
50
32
1
28.7%
29.7%
INTERNLM2-78 YING 2024
SEARCH
50
1
32
30.3%
SFT (INTERNLM2-77
SAMPLING
50
32
1
29.5%
30.6%
SFT (INTERNLM2-27)
SEARCH
50
1
32
30.7%
LEAN-COT (INTERNLMM-78)
SAMPLING
50
32
1
32.8%
35.6%
LEAN-STAR (ITER-1) (INTERNLM2-7D)
SAMPLING
50
32
1
34.0%
38.4%
LEAN-STAR (ITER-2) (INTERNLM2-7B)
SAMPLING
50
32
1
34.8%
39.4%
LEAN-STAR (ITER-2) (INTERNLM2-78)
SAMPLING
50
64
36.1%
4 EXPERIMENTS
We instantiate Lean-STaR using the best available open language model pre-trained on the Lean corpus (InternLM22 Math-bbae-7bb (Ying et al. (024)). and follow standard practice in using Lean's 's Mathlib the underlying training set (via the Lean Dojo dataset (Yang al. 2023)). We generate an initial set of thoughts for Mathlib using GPT-4, perform two rounds of expert iteration, then evaluate the model miniF2F (Zheng et al. 202T) and leandojo (Yang et al.] 2023), the de-facto standard benchmark for evaluating language-model model based theorem provers. Our experimental results show that both retrospective rationale generation and expert iteration significantly improve the theorem-pree prroving capabilities of language models in this setting. We describe our setup and findings in detail below.
4.1 EXPERIMENTAL SETUP
We use LeanDojo Benchmark v9 as the supervised fine-tuning (SFT) dataset containing 231, 240 data examples. We fine-tune for 1 epoch to obtain the SFT model. For the learning rate, we use warmup in the first 20% steps from to 2 x 10-5, followed by a cosine schedule decaying to zero.
We randomly select 17, 256 different successful proof trajectories from LeanDojo Benchmark 4 dataset (Yang et al. 2023), and use GPT-4-0125 (OpenAl (023) to annotate 52, 438 thoughts from those proof trajectories. We filtered out all proof steps (s" a') for which a' contains the newline symbol "nn" before annotating. We perform two iterations expert iteration, and provide the details in Appendix I.I due space.
We evaluate our method on the MiniF2F benchmark (Zheng et al. 2021). We use similar evaluation setting previous works (Yang et al. 2023 Welleck & Saha 2023 Ying et al.) 2024), but use
7

---

Published as a conference paper at ICLR 2025
Table Pass rates about InternL.V2-Plus-7B on the minif2f-test dataset with Lean. This table shows the pass rates of previous works and our work. The evaluation setting is the same as Table
APPROACH
DECODING
N
K
PASS RATE
INTERNLM2-PLUS-TE
YING 2024
(FROM PAPER)
SEARCH
1000
1
32
43.4%
INTERNL.M2-PLUS-77 YING ET AL.
2024
(REPRODUCED)
SEARCH
1000
1
32
42.6%
INTERNLM2-PLUS YING ET AL..
2024
SAMPLING
50
32
40.9%
SET (INTERNI.2--PLUI--7)) (YING
2024
SAMPLING
32
41.3%
LEAN-COT (INTERNLM2-PLUS-
SAMPLING
50
32
43.4%
LEAN-STAR (ITER-1) (INTERNLM2 PLUS-7B)
SAMPLING
32
45.4%
INTERNLM2-PLUS-T YING ET AL. 2024
SAMPLING
50
64
42.2%
SFT (INTERNLM2-PLUS-TT) YING ET AL.
2024
SAMPLING
64
43.4%
LEAN-COT (INTERNLM2-PLUUS-7)
SAMPLING 50
64
45.5%
LEAN-STAR (ITER-1) (INTERNLM2-PLE) PL)
SAMPLING
64
46.3%
sampling method instead of best-first search for the evaluation of our thought-angmented theorem proving model as discussed in ($3.3). We choose these settings resemble the inference budget used in our baselines, which follow previous work (Welleck & Saha 2023: Azerbayev et al. 2023b
Ying et al., 2024). Namely, for best-first search baselines we use beam search to generate the next tactic with 5 = 32, K = (Welleck & Saha 2023 Azerbayev et al., 2023b Ying et al. 2024). We do not compare with methods designed for other formal languages such as Jiang et al. (2022): Xin al. 2023) since language differences greatly influence the pass rate due to the different tactics and automation. also not compare with Lample et al. al. (2022) since they only report S = 32, 64 on best-first search, which is approximately equivalent to S 1, K 512 for the sampling method, which is too computationally expensive for us.
4.2 MAIN RESULTS
Our main results are reported in Table 1 Lean-STaR gives significant improvement over the base model. For instance, with similar inference budget, Lean-STaRe achieves 34.8% versus 30.3% in InternIM2 (Ying et al. 2024) using best-first search and 30.7% in COPRA (Thakur et al. 2023) using GPT-4. With a larger compute budget, SeansS performance improves further to 36. %.
Thought augmentation improves theorem proving. The first phase of Lean-STaR trains a model synthesized dataset of thought-augmented
to interleave thoughts and tactics, by fine-tuning examples. The fine-tuned model from this phase, denoted LEAN-COT in Table achieves a pass rate of 32.8%. which is higher than the model prior to this phase, denoted SFT (29.5%). We conclude that the first phase of Lean-STaR can improve the theorem proving ability of a language model, even one that already specialized for generating tacties in Lean such the SFT model.
Bootstrapping improves thought-auugmented theorem proving. The second phase of Lean-STaR consists of generating new thoughts and tactics with the current language model, saving those that result in correct proofs, and training on the union of the initial thought-augmentte augmented dataset and the
saved examples (i.e., expert iteration (Polu et al. 2022 Zelikman et al. 2022 Singh et al. 2023
Refer to Appendix A. for details.
We perform two iterations of expert iteration, and present the results in Table I denoted LEAN-STAR. Each iteration improves the model's theorem proving performance, from 32.8% (the initial model) to 34% (LEAN-STAR after iteration 1) to 34.8% (LEAN-STAR after iteration 2). Furthermore, find that the model is amenable to further improvement via additional sampling, achieving 36. % by doubling the sampling budget. We conclude that Lean-STaR's second phase can further improve a model's ability to generate thoughts and tactics that lead to correct proofs. We include three qualitative examples in the Appendix, which show the model interleaving thoughts and proof steps.
8

---

Published as a conference paper at ICLR 2025
Table 3: Results for the MM and our Lean-CoT, Lean-STaR, and expert iteration without COT. We use sampling with N 50, K 32, & T = 0.7.
APPROACH
Pass 32 OF INTERNLM BASE
Pass@ 32 OF INTERNLM PLUS
FEW-SHOT
28.7%
40.9%
SFT
29.5%(+0.8%)
41.3%((+0.4%)
LEAN-COT
32.8% (+33.%%
13.4%((+..1%%)
LEAN-STAR
84.0%(+1.29%)
45.5%(+2..1%
EXPERT ITERATION (SFT)
30.7%(+1.225)
43.0% 43.0%(+1.79%))
4.3 EXPERIMENTS WITH STRONGER BASE MODEL. AND MORE DATA
We instantiate Lean-STaR using a stronger language model MaeeemLLM-Mathppluss (Ying et al.. 2024)), which was released after the experiment above. We follow similar setup to the previous experiment.
In this experiment, we used 140, 000 thoughts annotated by GPT-4o (OpenAl 2023) to fine-tune model ("Lean-CoT"). Then we performed only one iteration of expert iteration and collected about 60, 000 (proof state, thoughts, next-tactic) pairs in data, named "STaR dataset" Dj. We further fine-tuned the Lean-CoT model on dataset D1 to get the Lean-STaR model.
Our new results are reported in Table We can see that Lean-STaR still gives significant improve- ment over the baseline. For instance, Lean-STaR achieves 45.4% versus 40.9% in InternLM -plus using sampling with similar inference budget and 43.4% using best-first search with more inference budget reported in (Ying et al. 2024). This results show that both retrospective rationale generation and expert iteration improve the theorem- theorem-proving capabilities stronger base model.
4.4 EXPERIMENTS ON EXPERT ITERATION WITHOUT CoT
Table the result of expert iteration without CoT (i.e., using (state, tactic) pairs only) well as the result of Lean-CoT and Lean-STaR. Expert iteration alone achieves 43.0%, which is less than Lean-STaR (45.4%) in InternI.M-plu and achieves 30.7% verus 34.0% in InternI.M-ban This performae
shows that Lean-STaR's performance gains do not only come from the use of expert iteration.
5 CONCLUSION & LIMITATIONS
In this paper, presented Lean-STaR, a novel approach that significantly enhances the theorem- proving capabilities of language models in formal mathematics by integrating Chain-of- -hain-of-Thhuuht (CoT) rationales into each proof step. Our method begins with generating synthetic rationales using ground-truth tactics retrospectively, followed by fine-tuning the language model to generate these rationales and predict subsequent tacties, resulting in the Lean-CoT model. We further improved this model using expert iteration, fine-tuning it correct proofs it samples and verifies using the Lean solver. Our contributions include the introduction of the first thought- augmented theorem proving dataset, demonstrating that expert iteration can further improve performance, and achieving new results on the miniF2F-test benchmark, increasing the pass rate from 30.3% to 36.1 %. These advancements
not only about improving the accuracy of automated theorem proving. but also offer a scalable and efficient framework for advancing human understanding of mathematics, which may lead to significant impacts in education, scientific discovery, and program verification (Carter & Monks 2013 Kang et al. 2020 Szegedyy [2020] Avigad 2023 First 2023 of Sciences 2023).
The primary limitation of method is that its performance may be constrained by issues of computational scalability, Both Lean-CoT and Lean-STaR have been fine-tuned on a dataset that not very large. Additionally, the use of GPT-4 generate synthetic data may incur significant

---

Published as a conference paper at ICLR 2025
cost and possibly introduce biases. Also, expert iteration could face bottleneck due CPU and I0 limitations, which might slow down the process due to a sluggish speed of Lean ITP.
ACKNOWLEDGMENTS
We thank the anonymous reviewers and area chair for their helpful comments. Zhiqing Sun acknowl- edges the support of the Google PhD Fellowship. Sean Welleck thanks NSF SCALE (NSF DMS 2134012) and Convergent Research.
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303. 08774, 2023.
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022.
Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. Advances in neural information processing systems, 30, 2017.
Jeremy Avigad. Mathematics and the formal turn, 2023.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leve mathematics. arXiv preprint arXiv:2302.1243: 2023a.
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. Xiviv preprint arXiv:2310.10631, 2023b.
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards qed. Journal of Formalized Reasoning, 11):101-444, 2016.
Sascha Bohme and Tobias Nipkow. Sledgehammer: judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 5, pp- 107-121. Springer, 2010.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et Language models are few-shot learners. Advances in neurul information processing systems, 13:117771901
Kevin Buzzard. Lean in lean- 20247 2024.
Nathan Carter and Kenneth G Monks. Lurch: a word processor that can grade students' proofs. In CICM Workshops, 2013.
Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. Program of thoughts prompt- ing: Disentangling computation from reasoning for numerical reasoning tasks. arXiv preprint arXiv:2211.12588 2022.
Projet Coq. The coq proof assistant-referrnce manual. INRIA Rocquencourt and ENS Lyon, version, 5, 1996.
Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. Journal of automated reasoning, 61:423-451 2018.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doomn, and Jakob von Raumer. The lean theorem prover (system description). In Automated IeduuctionCAADE 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378-388. Springer, 2015.
10

---

Published as a conference paper at ICLR 2025
Emily First. Automating the Formal Verification of Software. PhD thesis, 2023. URL https: /schhlaaworks. umass edu disserttsssrt 2/2812.
Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European
Software Engineering Conference and Symposium on the Foundations of Software Engineer-
ing, ESEC/FSE 2023, pp. 1229-1241, New York, NY. USA, 2023. Association for Com-
puting Machinery. ISBN 9798400703270, doi: 00.1145/6611643336662455 URL https
//doi.org/10. 111.1....111111111/111 361664443333
Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, and Gabriel Synnaeve. Temperature-scaled large language models for lean proofstep prediction. In The 3rd Workshop on Mathematical Reasoning and Al at NeurIPS'23, 2023.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203 2021.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co- training for theorem proving with language models. In International Conference on Learning Representations, 2022. URL http::sss/ppeeeeeeeeeee.eet wtw.:/rr.weeeeoueeee.emm (ot.oorrumm....pXJJ
Dan Hendrycks. Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2 003.0000000 103.03874, 2021.
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. Mustard: Mastering uniform synthesis of theorem and proof data. arXiv preprint arXiv:2402.088: 08957, 2024.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothee Lacroix, Yuhuai Wu, and Guillaume Lample. Draft. sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprini arXiv:2210. 12283, 2022.
Dongyeop Kang, Andrew Head, Risham Sidhu, Kyle Lo, Daniel Weld, and Marti A Hearst. Document-level definition detection in scholarly documents: Existing models, error analyses, and future directions. arXiv preprint arXiv:2010.05129, 2020.
Guillaume Lample. Timothee Lacroix, Marie- Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 18:26337-263444 2022.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey deep learning for theorem proving, 2024.
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp- 367-381, New York, NY. USA, 2020. Association for Computing Machinery. ISBN 1781450370974, doi: 10.1145/ 3372885.3373824, URL httph:ttt//ccct /ttpp::/doo..oooo /ttp///11.1113111111111 3373824
Allen Newell and Herbert Simon. The logic theory machine-a a complex information processing
system. IRE Transactions on information theory, 2(3):61-79, 1956.
Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002.
Maxwell Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski. Jacob Austin, David Bieber, David Dohan, Aitor Lewkowyez, Maarten Bosma, David Luan, et al. Show your work: Scratchpads for intermediate computation with language models. arXiv preprint arXiv:21122.0111, 2021.
National Academies of Sciences. Artificial intelligence to assist mathematical mathemanicalreasoonngg. reasoning: Proceedings of workshop, 2023.
OpenAI. OpenAl: GPT-4, 2023. URL httpt::// http:://ppeaaiiii. http:/pperaa...cmm/aaeaarcc/////
11

---

Published as a conference paper at ICLR 2025
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03:3 03390, 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng. Mantas Baksys, Igor Babuschkin, and Ilya
Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
Markus Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757 2020.
Avi Singh, John D Co-Reyes, Rishabh Agarwal, Ankesh Anand, Piyush Patil, Peter Liu, James Harrison, Jachoon Lee, Kelvin Xu, Aaron Parisi, al. Beyond human data: Scaling self-training for problem-solving with language models. arXiv preprint vrXiv:23/2.06560 2023.
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26 26-31, 2020, Proceedings 13, pp. 3-20. Springer, 2020.
Terence Tao. https://mathstt http://toooooaeeeeea//11211222/2
2023.
Amitayush Thakur, Yeming Wen, and Swarat Chaudhuri. A language-agent approach formal theorem-proving. arXiv preprint 3rXiv:23100043333 2023.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in- context learning agent for formal theorem-proving. 2024. URL
7310..4355
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang. Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li. Heng Liao, and Xiaodan Liang. Lego-prover: Neural theorem proving with growing libraries, 2023a.
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi. Yujun Li, Lin Li, et al. Di-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 12632-12646 2023b.
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 85-98, 2020.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoe V Le, Denny Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824-24831 2022.
Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions lean. arXiv preprint MrXiv:2310.8847. 2023.
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. arXiv preprint arXiv:2104.01112, 2021.
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models, Advances Neural Information Processing Systems, 35:4913 4927. 2022.
Yuhuai Wu, Markus Rabe, Wenda Li, Jimmy Ba, Roger B Grosse, and Christian Szegedy. Lime: Learning inductive bias for primitives of mathematical reasoning. In International Conference Machine Learning, pp. 11251-11262. PMLR, 2021.
Yuhuai Wu, Albert Qiaochu Jiang. Wenda Li. Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368, 2022.
12

---

Published as a conference paper at ICLR 2025
Huajian Xin, Haiming Wang, 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 arXhv:2310.00656, 2023.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmente language models. In Neural Information Processing Systems (NeurIPS). 2023.
Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong. Kuikun Liu, Ziyi Wang. Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-matee math: Open math large language models toward verifiable reasoning, 2024.
Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. Star: Bootstrapping reasoning with reasoning. Advances Neural Information Processing Systems, 35:15476- 2022.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstra- tion learning for formal theorem proving, 2024. /t//:tttsss//ppennee.e..e..eeeee
id=xooxVv0695
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXi::2109.00/10, 2021.
Denny Zhou. Teach language models reason. h
io/
LIMs - Reas-Reao----ee Taiwan 2023. pdf 2023. Accessed: 2024-05-21.
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't trust: groiddng IIm quantitative reasoning with autoformalization. arXiv preprint arXiv:2403. 18/20, 2024a.
Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't 't trust: Verify grounding LLM quantitative reasoning with autoformalization. The Twelfth International Conference Learning Representations, 2024b. URL URL.ttpss: /ttp:://///eeeeeeeeee revi ew net. Forum? d=
13

---

Published as a conference paper at ICLR 2025
A ADDITIONAL EXPERIMENT SETUP
A.1 LEAN-STAR EXPERT ITERATION
The second phase of Lean-STafk consists of generating new thoughts and tacties with the current language model, saving those that result in correct proofs, and training on the union of the initial thought-augen augmented dataset and the saved examples (i.e., expert iteration (Polu et al., [022] Zelikman al., 2022 Singh al. (023]). We perform two iterations of expert iteration, and provide details on our specific experimental setup below.
In each iteration we use sampling on the LeanDojo Benchmark 4 dataset, and save the (state, thought, tactic) examples that are part of successful proofs. For each problem, we sample = 32 times in parallel with temperature T 1.0, and limit the number of times a tactic can be generated to total N per problem. Also, sampling limited to minute per problem. In this setup, each problem needs average about 0.5 A100 minutes. We collect successfully sampled trajectories to produce a "STaR dataset" D1. and up to 3 proof trajectories were collected for each problem. We collected 32, 231 different (proof state, thoughts, next-tactic) pairs in successful proof trajectories during expert iteration, which takes about 4 days with 8 x A100 GPUs. Then, we further fine-tune SFT model for epoch on the combination of GPT-4 annotated reasoning data and expert iteration data Dr U D to get the Lean- Sean-STaRR model. We use the same learning rate setup that was used for the SFT model. In the second iteration, we generate a dataset D2 a similar fashion. Then, we chose to further fine-tune model from iteration 1, M1, on the generated dataset D2 (roughly 19k pairs).
The setup of experiment about InternLM2-plu is slightly different. The details are shown in Section 4.3 and Appendix
B STATISTICS FOR OUR METHODS AS WELL AS THE BASELINES
Table 4: Statistics for the baselines and our Lean-CoT, Lean-STaR on MiniF2F dataset. We use sampling method with hyperparameters N 50 & K 32 & 0.7.
APPROACH
(CONTINUAL) TRAINING DATA
Pass@:
INTERNLM2-MATH-77 (FEW-SHOT)
28.7%
SFT
231, 240
29.5%
+0.8%
LEAN-COT
52, 438
32.8%
+3.3%
LEAN-STAR (ITER-1)
32, 231
31.0%
+1.2%
LEAN-STAR (ITER-2)
19, 324
34.8%
+0.8%
14

---

Published as a conference paper at ICLR 2025
C DATA LEAKAGE
risk of using GPT-4 for generating thought annotations is data leakage. Sine miniF2F has been used dataset for formal theorem proving for while, it is possible that miniF2F dataset is already seen by GPT-4 or intern.M during pre-training process. However, there are several reasons to believe that data leakage is not likely to be true.
First, our experimental setting (fine-tuning on Mathlib, evaluating on miniF2F) follows a widely used experimental setup in benchmark evaluations in neural theorem proving and InternLM was also evaluated on miniF2F. Therefore, we believe that InternIM has not been exposed to miniF2F.
Also, observed that most of the proofs generated by Lean-STaR completely different from the manually written proofs in the miniF2F test dataset. Table shows the analysis of proof generated by Lean-STaR on miniF2F test dataset for Lean. From Table 5 we can that almost all proofs generated by LeanSTaR are different from the proofs mentioned in the miniF2F. If we set aside straightforward simple cases, there is only one proof generated by LeanSTaR is the same the proofs mentioned in the miniF2F.
Table 5: Analysis of proof generated by Lean-STaR on miniF2F test dataset for Lean. Similar to the analysis in Thakur et al. (2024).
Proofs NOT miniF2F
Proofs found miniF2F-test
Total
Longer
Single-Tactic Simple Proofs
Two-Tactic Proofs
OR
Total
Complex
Proofs
tactics
Tactics
OR
Used
linarith
norm_num
nlinarith
two factics
tactic
sorry
multi-args
Prool
12
2
18
39
82
162
244
Count
Exact
Match
Successful
4
0
7
0
7
Proof
Count
1st
Tactic
Match
4
0
0
7
Successful
Pronf Count
Distinct
Successful
7
43
(80.36%)
Proof
Count
Distinct
Successful
Proof
12
18
20
38
Count
Single- Tactic
All
Successful
12
48
112
Proof
Count
D AN EXAMPLE AND EXPLANATION OF A FORMAL PROOF IN LEAN
An example of formal proof in Lean with its visualization shown in Figure 5 taken from (Lample et al. 2022). In the proof. the tactic induction is is applied to the initial state < m + k) and the ITP converts the current state to subgoals case ih: n mAn+ k I m
(n < m = n
A case
n (k (k++)) m +1+ The case 0: m is our hypothesis ho so it can be proven by case 0: Dxexact ho tactic. Then, we rewrite the case ih through the nat succ le_ succ ff which is theorem in Lean library means S
m
15

---

Published as a conference paper at ICLR 2025
After tactics case 0:exact hy and case ih:rw nat succ le succuucc_t iff, the goal state converted to n + I m + which is the hypothesis introduced by induction. Therefore, we can complete this proof using tactic exact k ih.
theorem add_le_ _e__ad____rr_eee right (m n & N) (ho S m)
k + 1=
induction with zero =>
exact ho succ k ih => ant.succ_le_sst
exact
(m mank:Ni [he n =
induction
.n O m + 0
k n t k_nkkuccccaaa s m k_n.succ
exact he
EW nat..uoc auco__ac_____ iff
[k m k): n+k_nmm+k_n
exact kh
Figure 5: A example proof and its visualization of taken from (amplee et al., 2022).. The induction on tactic reduces the initial statement to two subgoals. Then tactics case 0:exact hg and case ih:re rw nat lts_suuce__uu__eeeeeeeeeeeeeeeee iff, case ih:exact i can be applied turn to complete the proof.
n m k in Lean,
16

---

Published as a conference paper at ICLR 2025
Table 6: Counts of problems successfully proved in minif2f-test benchmark, split by type and difficulty. The methods use sampling with N = 50, K = 32. Thought-augmented methods improve performance on all categories, while Lean-STafe significantly improves Number Theory performance.
TEST SET
LEAN-STAR (ITER-2)
TOTAL
INTERNLM2-7B
SFT LEAN-COT
SIZE
IMO
0
AIME
15
2
AMC
45
3
3
LEVEL 5
1
2
LEVEL 4
7
ALGEBRA
LEVEL 3
14
9
9
11
11
LEVEL 2
14
10
10
11
LEVEL
9
MATH
LEVEL 5
16
6
LEVEL 4
11
5
5
4
NUMBER THEORY
LEVEL 3
4
5
LEVEL
LEVEL 1
8
ALGEBRA
18
0
1
CUSTOM
NUMBER THEORY
0
0
INDUCTION
sectionPerformance Analysis by Types and Difficulties Tasks in minif2f-test are manually formalized from Olympiad type problems, drawn from multiple sources including AIME, AMC, IMO problems, and problems from the MATH dataset (Hendrycks al. (02T). These problems can have different levels of difficulty and types. reports the number problems successfully proved, partitioned by type and difficulty. We see that Lean-CoT improves performance in solving difficult problems on all categories, especially those from mathematics competitions. On top of these improvements, Lean-STaR's improvements come mainly in Number Theory.
D.1 PERFORMANCE ANALYSIS BY TYPES AND DIFFICULTIES USING INTERN..M-PP..S..
Table 7 reports the number of problems successfully proved, partitioned by type and difficulty using IntemLM2-plue We see that Lean-CoT improves performance mainly Number Theory and Lean- STaR improves performance in solving difficult problems on all categories, which is the opposite of the performance of the InternL.M2-ban
COMPARISON BETWEEN SEARCH METHOD AND SAMPLING METHOD
17

---

Published as a conference paper at ICLR 2025
Table 7: Counts of problems successfully proved in minif2f-test benchmark using InternLMM--llu-7b. split by type and difficulty. The methods use sampling with N = 50, K = 32.
TEST SET SIZE
INTERNLM2-PLUS-78 LEAN-COT LEAN-STAR
TOTAL
(ITER-I)
IMO
20
AIMH
AMC
45
10
LEVEL 5
14
LEVEL 4
14
ALGEBRA
LEVEL 3
LEVEL 2
LEVEL
14
10
10
10
MATH
LEVEL 5
16
LEVEL 4
NUMBER THEORY
LEVEL 3
11
LEVEL 2
11
LEVEL
10
10
10
ALGEBRA
CUSTOM
NUMBER THEORY
INDUCTION
Table 8: Comparison between search method and sampling method. We use sampling method with
hyperparameters = 50 = 1 & = 32 and BFS method with N = 50 = 32 & All sampling decoding in the paper uses temperature of 0.7. We use BFS denotes Best-First Search.
APPROACH
BFS (SAMPLING)
BFS (BEAM SEARCH)
SAMPLING
TACTIC PREDICTION PROVING
BFS SAMPLING
BFS
SAMPLING SAMPLING
TOKEN DECODING IN TACTICS
INTERNLM2-7R (FEw-SHOT)
29.1%
30.3%
28.7%
SFT
29.9%
30.7%
29.5%
LEAN-COT
27.0%
25.4%
32.8%
LEAN-STAR (ITER-1)
29.1%
26.2%
34.0%
LEAN-STAR (ITER-2)
29.5%
26.2%
31.8%
F PERFORMANCE DIFFERENCE OF JOINT TRAINING AND CONTINUE TRAINING
As shown in Table the joint training method performs better using Interm.M2--baee but training method performs much better using InternLM2-plus. It seems that there are difference between these two methods. Therefore, this performance can be depend on the quantity data or the model. (We use much more data when using InterLM22-p and the quantity of "STaR data" is relatively small.)
F.1 SEARCH AND SAMPLING BUDGET
Table 10 reports the trends of the pass rate against the search size sampling budget S x K. We find that STaR benefits more as increases, especially when K relatively large. The result suggests that additional sampling with thoughts improves performance, while additional sampling without thoughts may saturate. We believe this because thoughts increase the diversity of outputs and contribute to exploration in the theorem proving space. Therefore, Lean-STaR is more scalable
18

---

Given Tactic: Published as a conference paper at ICLR 2025
Table 9: Performance difference of joint training and continue training on Lean-STaR. We use sampling method with hyperparameters N = 50 & K = 32 & T 0.7. In continue training, we further fine-tune the Lean-CoT model on "STaR data" to get Lean-STaR model and joint training we fine-tune the SFT model on combination of GPT-4 annotated reasoning data and "STaR data".
APPROACH
INTERNLM2-BASER
INTERNLM2-PLUSS-T
LEAN-COT
32.8%
43.4%
LEAN-STAR (ITER-1)
34.0 %
43.9%
(JOINT TRAINING)
LEAN-STAR (ITER-1)
33.2%
45.5 %
(CONTINUE TRAINING)
Table 10: Performence of SFT-Direct and our Lean-STaR at different search size sampling times K. We fix N 50. We use beam search in search and temperature 7 0.7 in sampling when generating the next tactic. We have K = 1 in search and S 1 in sampling. Note that we sample 32 examples twice when = 64 in sampling.
SFT-DIRECT (SEARCH)
SFT-DIRECT (SAMPLING)
LEAN-STAR (ITER-2) (SAMPLING)
S K
13.5%
20.9%
21.7%
S =
18.0% (+4.55%)
22.5% (+1.6%)
24.6%(+2.9%))
8 K
23.3% (+5.33%)
25.0% (+2.5%%
27.5%((2..9%
8 K =
27.5% (+-4.2%)
27.0% (+2.00%)
30.7% (+3.2%)
x K 16
29.9% (+2.4%)
28.3% (+1.3%)
33.6% (+2.9%)
8 X K 32
30.7% (+0.8%)
29.5% (+1.2%)
34.8% (+1.2%)
S K 64
30.7% (+0.0%)
30.3% (+-0.8%)
36.1% (+1.3%%
(in terms of inference-tine compute), and may be amenable to further improvements with additional iterations of expert iteration.
G RETROSPECTIVE RATIONALE GENERATION PROMPT OF GPT-4
Please act as professional mathematician Your goal is to accurately prove math theorem in lean4. You are given the first tactic that should be taken to prove the Given Theorem.
Example:
Given Theorem:
.. """lean Type u_1
Y Type u_2
instt' Topologicallsaace x
instt TapologicalSpace
f: X -
PContinucus
FIsOpen (FFun.preimage Set.univ)
1eand
exact 100pen_univ
19

---

Published as a conference paper at ICLR 2025
#Hi State
a :
+ --nn * 0) +==
### Tactic
lean4
simp only [not_and and or, ne_eq, not_not)
### Reasoning
To prove the equivalence between negation conjunction and disjunction, we utilize logical cquivalences, specifically the negation of a conjunction -(" (P A Q)' being equivalent to the disjunction of the negations 0 Q =0 and simplifications related to negation and inequality.
Figure 6: Examples of (input, output) pairs of retrospective rationale generation with GPT-4. The full prompt is given in Appendix G See $32.2 for the detailed explanation.
Assistant Output:
### FLANNING OF REASONING
Given the above goal and the given the target tactic "exact isOpen_univ", should produce reasoning that only based on the goal and conclude to the 'exact iscpen_uriv', but not in the hindsight format.
### REASONING
By directly using the hypothesis "h PContinuous f', we state that for any open set, its preimage via "f" is also open, and this applies to set.univ' well.
### TACTIC
leann
exact isOpen_unii
To achieve the goal, you have three jobs.
Write down the planning of reascning.
Write down the reasoning that result in the selection the Given Tactic.
Write down the Given Tactic.
You have four principles to do this.
Craft reasening that is comprchensive yet concise, contained ideally within two sentences.
Begin reascning with the objective of the Given Theorem, ensuring logical progression, rather than constructing it retrospactively from the Given Tactic.
Avoia mentioning the Given Tactic and specific statement
from the
Given Tactic throughout your reasoning.
Position the conclusion of the tactic after presenting all reasons, ensuring that details regarding the Given Tactic are not introduced the start of your reasoning.
Your output should be strictly in the following format and should not contain extra content:
### PLANNING OF REASONING
Given the above goal and the given the target tactic <Given Tactic>, should produce a reasoning that only based on the goal, and conclude to the exact <Given Factie>, but not in the hindsight format.
# REASONING
20

---

Published as a conference paper at ICLR 2025
<your reasoning to the Given Tactic>
### TACTIC
<Given Tactic>
Given Thecrem:
1ean4 [theorem| "sstate_before""""
Given Tactic:
leand [theorem(" ["tacti"]])
21

---

Published as a conference paper at ICLR 2025
H EXAMPLES OF GENERATED LEAN PROOFS WITH THOUGHTS
theorem aime_ _mm__990_pp p4 (x : R) (ho
0
<
x)
(h1
: x 2 10 x 29 # 0)
(h2 : x
10
x 45
* 0)
(ba 1 x 2 10 * x 69 7 0)
(h4 : / (x 2
2
10 * 29)
1x
2 10
45) 2 / (x
" 2 10
69) 0)
x :
norm_num at h1 h2 ha Reasoning: To prove 'x - 13', we examine the conditions under which the given equation hoids, specifically
focusing the non-equality of the expressions involving "x 69".
10
*x 29", 'x A Simplifying these expressions using properties algebra allows us to directly compare them with their respective values, uitimately identifying x = 13" as the unique solution that satisfies all constraints.
10
45', and ^ 10
real numbers and
field_simp at Reasoning: prove \xx 131,, we leverage the given equalities involving rational fractions of (xx2 10x - cl) for various constants (el), where (00 < x() and each (xx22 - 10x el) is non-zero. By aigebraically manipuiating these expressions, aim to derive relationship among 1 (x)) and these constants, specifically focusing on (13V), under the given non-zero conditions for the quadratic expressions.
ring_nf at h4 + - Reasoning: To establish the equality =x=13 need to manipulate the algebraic under the given conditions, expression given by 'h4" reveal its dependence on 'x', recognizing that the presence of 'x' in the expressions may affect the equation's truth value. The application of algebraic transformations on both sides of the equation will facilitate the ident of 'x''s value, taking into consideration the inequality conditions previded ('hi, 'm2", 'ha').
nlinarith Reasoning: To prove (xx - 131), we must manipulate the equation given by (ha to isolate (xx), using the algebraic properties of equality and the assumption (hol) which states (/0 x)). This requires careful rearrangement and application of algebraic identities to simplify and rearrange terms, facilitating the direct application of the properties of real numbers to reach the desired conclusion.
theorem amc12a_2002_p6
N) (ho : 0 < n)
: 3 n, m > n A E m p S m + p=
use n + 1, by linarith only [ho] -- Reasoning: To demonstrate the existence of such an 'm' and 'p" that satisfy the given reeualitiess leverage the property of natural numbers that ensures an increase in 'n" from "0" leads to the possibility of finding such 'm" and 'p". This approach is supported by the fundamental property of natural numbers and their arithmetic operations, suggesting that for given 'n' greater than '0' there exists successor 'm" and number 'p" that satisfy the conditions outlined.
exact (0, by simp ) -- Reasoning: To demonstrate that there exists an Vnn lin N1) such that (((n I) x p \leq a + 1 + pl) holds for some (p Vin No, we recognize that setting (p = 01) satisfies the inequality by the properties of zero in arithmetic. This is because \ (n + 01) by assumption, ensuring the left-hand side is non-negative and the right-hand side simplifies to \n 11), making the inequality trivially true.
22


Reviews:
[{"review_id": "pScTao9LnY", "reviewer": "Reviewer_TwP5", "summary": "This paper introduces a novel approach to neural theorem proving (NTP). One previous drawback of step-by-step approaches to NTP is the lack of Chain-of-Thought (CoT) or SketchPad techniques before generating each tactic. These techniques have proven to be very useful in the domain of mathematical word problems (MWP). To address this, the paper proposes using GPT-4 to generate an initial CoT before each tactic on the Mathlib dataset, and subsequently bootstrapping the model with expert iteration. The experimental results show that adding CoT before generating the tactic leads to performance gains.", "questions": "- Are there any alternative methods employed in Lean-StaR to ensure the quality of the COT generated by GPT-4? Why was the state and ground truth tactic the sole approach used to generate these COTs? Would incorporating additional proving context improve the quality of the generated COTs?\n\n- In Table 1, does the 'N' in 'Sampling' and 'Search' have different meanings? Is 'N' in 'Search' referring to the total number of expansions (nodes to explore), while 'N' in 'Sampling' refers to the number of failure retry attempts when the LLM generates a faulty tactic? I believe clarifying this in the caption would enhance understanding.\n\n- In Lines 372 and 398, should 'Table 7' be corrected to 'Table 1'?\n\n- It appears that the SFT finetune model does not show significant performance differences compared to InternLM2-7B. Is this due to the fact that these models have already been pre-trained on the Lean dataset?\n\n- On Line 449, where does the 39.8% figure originate? Should it be 34.0% instead?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "- The problem the paper aims to address is long-standing, and the paper provides strong empirical results demonstrating that the Chain-of-Thought (CoT) reasoning before each tactic application is useful.\n- The newly proposed sampling method is novel and, based on its performance, appears to be a promising approach compared to Best-First Search.\n- The proposed CoT-augmented dataset should be useful for future research in neural theorem proving.\n- The paper is well-written and easy to follow.", "weaknesses": "- One issue with the generated COT is the absence of a verification mechanism or alternative methods to ensure its quality. The paper does not provide a detailed evaluation of these generated COTs; it only presents the final pass rate information. I believe that having a robust evaluation is crucial for improving the performance of this method. Moreover, in prompting GPT-4 to generate COTs, the authors have only explored one approach in constructing the prompt. I hope for a more in-depth analysis on how to create these prompts and a detailed examination of the structure of COTs that would better facilitate formal theorem proving.\n- Another concern is that while the method demonstrates effectiveness, the ablation study reveals only a modest improvement of 2.5% (Lean-STaR versus Expert iteration (SFT) as shown in Table 3 in InternLM-Plus and 3.3% in InternLM-Base. Given that COT is expected to significantly enhance performance in the MWP (Math Word Problem) domain, I had anticipated a more substantial improvement. Could you provide any insights into why the performance of COT in NTP is not as strong as it is in MWP.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "TAA3vgLzQO", "reviewer": "Reviewer_kzhz", "summary": "This paper introduces a framework called Lean-STaR for training LLMs that incorporates both informal reasoning in the form of natural language (called thoughts) with formal reasoning in the form of Lean code to improve a LLMs theorem-proving capabilities. More concretely, the paper proposes to construct a tactic predictor as p(tactic | proof context) = Expectation_{thought ~ p(thought | proof context)} p(tactic | thought, proof context). This contrasts with direct tactic prediction which directly construct p(tactic | proof context) as is done in previous works. To train the tactic predictor, the authors propose the following pipeline. First, they introduce retrospective rationale generation to create a \"thought-augmented\" dataset (called CoT dataset) which consists of tuples of (tactic, proof context, thought) where each (tactic, proof context) are taken from an existing Lean corpus (Mathlib) and each thought is generated by GPT-4 with a specially-crafted prompt. Second, they take InternLM2-Math-base-7b, a LLM that is pre-trained on Mathlib, and perform supervised fine-tuning on the CoT dataset to create a model called Lean-CoT. Third, the authors use expert iteration to construct a Lean-STaR model by fine-tuning the Lean-CoT model on a dataset of proof trajectories that it generates. The authors show that Lean-STaR outperforms direct tactic prediction on minif2f and LeanDojo benchmarks.", "questions": "- I believe that the learned distribution is p(tactic, thought | proof context) as opposed to  p(tactic | proof context) = Expectation_{thought ~ p(thought | proof context)} p(tactic | thought, proof context) as presented in the paper. In particular, I cannot find at any point in the paper how the expectation is handled (e.g., with a Monte Carlo estimate). Moreover, the dataset associates a single thought with a single (tactic, proof context) tuple so that we do not have multiple thoughts for a given proof context. Finally, my understanding of Figure 2 is that it is consistent with p(tactic, thought | proof context) since a single thought is generated and then used to generate a tactic as opposed to multiple thoughts that are marginalized. If so, it's not really a fair comparison with direct tactic prediction since you are basically comparing p(tactic | thought, proof context) vs. p(tactic | proof context) which means your approach gets strictly more information. In other words, the thought is not really treated as a latent variable and what is presented in the paper is not what is actually done. Looking forward to clarifying this.\n- Is there an intuitive reason why sampling works better than best first-search for your method?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "- The idea for constructing and training a tactic predictor p(tactic | proof context) = Expectation_{thought ~ p(thought | proof context)} p(tactic | thought, proof context) by introducing a latent variable in the form of thoughts is novel. \n- There are numerous experiments.", "weaknesses": "The presentation of the paper could be improved and I have one major concern about soundness of the results (see questions for the authors).\n\n- In general, I found the abbreviations and terminology of the paper to be confusing. For example, the text refers to the dataset as a thought-augmented dataset but it is abbreviated as CoT dataset. A model for direct tactic prediction is abbreviated as a SFT model. Lean-STaR is both the name of the framework and a model that is produced by the framework.\n- Automatic theorem proving and interactive theorem proving are used interchangeably throughout the text even though they are not the same concept.\n- The paper seems to argue that GPT-4 does not perform well in generating \"correct rationale through few-shot prompting\" (lines 196) and then proceeds to use GPT-4 to generate rationale for the CoT dataset. \n- Figure 3 is not very clear for me. For instance, I would expect the Base Dataset to be fed into GPT-4 as opposed to directly into the CoT dataset. The Expert Iteration loop is also not clear. I would expect Expert Iteration from Lean-CoT to feed into Lean-STaR, and a separate arrow kind/color to indicate the usage of models in inference mode to generate datasets (also for GPT-4).\n- Table 7 -> Table 1.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "L3xmca50j0", "reviewer": "Reviewer_QMzb", "summary": "Lean-STaR uses the STaR (Self-Taught Reasoner) framework to mix step-by-step reasoning (\"thoughts\") with formal proof steps. It combines this with expert iteration, where the model learns from successful proofs to improve further. This approach allows Lean-STaR to reach a pass@32 rate of 45.4% on miniF2F, indicating that adding informal CoT reasoning can enhance formal automated proving capabilities.", "questions": "My main concern is the impact of data leakage (as highlighted in the weakness section) which needs to be studied further. The paper is well-written, I don't have any other questions.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "**1. Simple yet very effective approach:**\nThe authors use retrospective rationale generation to come up with the thoughts given the state and ground truth action. The idea to train another model Lean-CoT for generation of thought-augmented tactics, is simple but works very well in this setting.\n\n**2. Use of expert iteration while informal thought generation:**\nWhile expert iteration has been used in previous works to improve formal theorem proving, the authors demonstrate that the same holds true for models that generate thought-augmented tactics.\n\n**3. Search based on Sampling:**\nThe authors used sampling-based search instead of BFS which is new and seems more effective for this setting. The idea that negative log-likelihood doesn't make proof search effective and a simple sampling technique can perform better is very elegant. The authors avoid the overkill of training a value function model which predicts the quality of generated tactics for choosing the search direction during the proof search. I'm surprised to see the effectiveness of a simple sampling-based search and would like to see a broader comparison with BFS in a formal proof-search setting.", "weaknesses": "**1. Data Leakage:**\nWhile the authors talk about the limitations of their approach, they don't discuss potential data leakage due to the use of GPT-4 for generating thought annotations. It can very well happen that miniF2F-related proof-steps are leaked in the thought generation process. Also, miniF2F has been used for a while for evaluating approaches for formal theorem proving, there is a chance that the base pre-trained model itself is trained on miniF2F repository. The worst part is that proofs are already checked in miniF2F repository, I would like to understand how much overlap exists between proofs generated by LeanStar and the proofs already checked in the miniF2F repository. Even the LeanDojo dataset, has existed in the public domain for quite some time, the pre-trained models like InternLM might as well be trained on this mix. I would like to see a broad study about how data leakage \"impacts\"/\"doesn't impact\" the overall results. I can also recommend some new benchmarks like Putnam Bench (https://arxiv.org/abs/2407.11214), which don't have proofs checked in online, for further evaluation.\n\nIt is a well-written paper, I will be more than happy to increase my score if the authors address some of my concerns.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "iHcQqN70iw", "reviewer": "Reviewer_MECo", "summary": "Generally, this paper takes motivation from a hypothesis that informal thought process can be valuable for LLMs to learn formal theorem proving. This work presents the following main contributions:\n\n1. The first thought (informal language) augmented for theorem proving in Lean (formal math).\n2. Lean-STaR: a framework which combines tactic prediction, thought augmentation with synthetic data, and two iterations of expert iteration.", "questions": "1. Related to the first weakness, the heavy use of GPT-4 to generate thought data (which are usually not short) can add a lot of computational and financial burdens. I would be curious to see a direct analyses of such overheads.\n\n2. The authors only performed two iterations of expert iteration. Both iterations lead to performance gains, and the first gains more than the second. Such findings all make sense and align with my expectation of applying expert iteration. However the author stopped right after only 2 iterations. I was wondering if a bottleneck would be hit very soon, or would the framework continue to benefit from more iterations?\n\n3. Minor suggestions: A few works that appear related to this paper, which the authors may consider citing/discussing.\n\n* [1] Multilingual Mathematical Autoformalization. Albert Q. Jiang, Wenda Li, Mateja Jamnik. arXiv 2311.03755. 2023.\n\n[1] is a work in autoformalization, which the authors did discuss in their related works. One thing that especially connects [1] to this paper is that [1] constructs <informal, formal> statement pairs in a backward manner, leveraging the fact that auto-informalization is a much easier task than autoformalization for LLMs. I feel this aligns in spirit with the retrospective rationale generation in this paper, which generates informal thought data from formal data using GPT-4.\n\n* [2] Towards Large Language Models as Copilots for Theorem Proving in Lean. Peiyang Song, Kaiyu Yang, Anima Anandkumar. arXiv 2404.12534.\n\n[2] is an open-source tool work in using LLMs as Copilots in Lean. The authors did discuss one related work LLMStep as practical tools in the field and may want to include [2] for completion. To my knowledge, they are so far the only two works that try to set up a ML framework easily usable in Lean.\n\n* Finally (and a very minor point), I think when discussing related works in this field, it may be beneficial to include some ML + ITP works in other proof assistants. Of course one does not need to expand in detail about them, but would be great to have a broader view.", "limitations": "", "rating": 8, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Prior to this work, people have been arguing how informal thought process can potentially benefit formal theorem proving, yet no one has taken the effort to explore how to interleave those two. People either used a standard tactic prediction model that operates only on formal code, or use a general-purpose model that only chats in an informal manner. While the methods (e.g. STaR, expert iteration) are not new themselves, the idea of combining the two and curating a resulting dataset sounds to me as a nice step. It is nice to have this work verify that known methods apply well to this domain of AI for math, especially given the many differences between this and other application areas.\n\n2. Theorem proving in Lean as a field suffers from a lack of data. Works like this with a large dataset size (50,000 from mathlib + 50,000 synthetic data) can greatly benefit the field.\n\n3. It seems that the framework is quite generally usable, and multiple models can be plugged in. This means the method proposed has a great potential to generalize. Similarly, its potential to be used alongside other synthetic data generation methods such as autoformalization without any approach-wise conflict sounds promising too.", "weaknesses": "1. The thought data generation in this paper is by few-shot prompting a general-purpose model (GPT-4). Data quality is usually a concern of synthetic data generation. People in the field either try to design data filtering mechanisms or recruit domain experts to sample and check. However, it seems that this work did not apply such techniques or analyses after synthetically generating thought data.\n\n2. The framework is composed of multiple methods. This paper could benefit a lot from having more thorough ablations. For instance, the authors can do an ablation on the thought augmentation, which is connected to their main hypothesis and contribution. What would the performance if all other settings (expert iteration, tactic prediction) are kept as-is but no thought augmentation is added? The authors can perform similar analyses on other factors they feel important too.\n\n3. Potential data contamination seems insufficiently discussed. Is it possible that InternLM2-Math-base-7b may have been exposed to parts of the test data? I think some analysis would be needed here.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Spotlight)