Lean-STaR: Learning to Interleave Thinking and Proving

## Abstract

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 achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment, significantly outperforming base models ( 43.4 % → 46.3 % , bold-→ percent 43.4 percent 46.3 \bm{43.4\%\rightarrow 46.3\%,} bold_43.4 bold_% bold_→ bold_46.3 bold_% bold_, Pass@64). We also analyze the impact of the augmented thoughts on various aspects of the theorem proving process, providing insights into their effectiveness.

## 1 Introduction

Theorem proving is a fundamental aspect of mathematics, and mathematical reasoning is an important part of artificial intelligence [, ].
Formalized mathematics in particular provides a challenging testbed for assessing mathematical reasoning capabilities. Since theorems and proofs in this setting can be represented in the form of checkable source code, it is easy to evaluate proofs of arbitrary complexity []. Automated theorem proving, if successful, can also help discover unknown errors in previous proofs(^1^11For example, Terence Tao found a non-trivial error while using Lean to formalize a project [].), and make it easier to guarantee that new proofs are 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 [, , , ].

Recently, language models have shown promising progress in formal theorem proving [, , , , , , ].
Existing approaches typically train a model solely based on the proofs in a formal language (code) such as Lean [], Isabelle [], or Coq [].
Our key observation is that such approaches ignore a wealth of informal information that may be useful for learning to prove theorems [, ]. For instance, the underlying thought process prior to each step of a 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 a 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 [], we enable language models to interleave step-by-step rationales (i.e., thoughts) [, ] with formal proving in a two-stage process.
In an initial phase, we prompt a sufficiently capable language model, such as GPT-4 [], and generate retrospective thoughts based on a dataset of human-written proofs, such as Mathlib, the largest collection of human-written proofs in Lean [].
Subsequently, we fine-tune a thought-augmented tactic predictor [, , , ] that, given a Lean state, can generate a thought and predict the subsequent tactic.
In a second phase, we optimize this thought-augmented tactic predictor with the expert iteration algorithm [, ], using multi-step success rate in theorem proving as the reward.

Our work presents a new link between informal and formal mathematics, complementary to prior explorations that translate standalone mathematical statements [, , ] or translate informal proofs into formal proofs [, , , , ]. 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-augmented examples from Lean’s Mathlib [], then synthesize an additional 50k examples through two iterations of expert iteration.
To the best of our knowledge, this yields the first thought-augmented dataset for theorem proving. After fine-tuning an InternLM2-7b base model [] on our thought-augmented data, our final Lean-STaR model can solve $\mathbf{34.8\%}$ (pass@32) or $\mathbf{36.1\%}$ (pass@64) of the problems on miniF2F-test []. Using stronger base model InternLM2-7b-plus, Lean-STaR can achieve $\mathbf{45.4\%}$ (pass@32), significantly surpassing the previous state-of-the-art results of $43.4\%$ (pass@32). In summary, Lean-STaR offers a framework for teaching language models to interleave informal thoughts with formal verification, advancing the capabilities of language models in automated theorem proving.

Figure: Figure 1: The illustration of tactic prediction in one proof step with and without thought.
Refer to caption: extracted/5782227/direct_vs_rational_augmented_v2.png

## 2 Related Work

##### Automatic Theorem Proving & Autoformalization.

Previous work on learning-based theorem proving typically follows the GPT-f framework [], 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 [], novel proof search methods [, ], further training through curriculum learning [], retrieval augmentation [], or practical tools [].
Others use prompted models to generate tactics [, ], or fine-tune models to generate a full proof [].
A second auto-formalization [] thread incorporates informal mathematics into formal theorem proving.
Draft-Sketch-Prove [] shows that language models have some ability to use informal proofs to improve a model’s formal proving abilities, by drafting an informal proof, translating into a formal proof sketch, then completing the proof with tools like Sledgehammer [].
Draft-Sketch-Prove and related methods [, , ] 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 a thought and predict the subsequent tactic in 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 [, , ].
Although the corresponding techniques (e.g., Scratchpad and Chain-of-Thought) have proven to be effective, they require either extensive annotated training examples or exposure to numerous similar examples during pre-training []. 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 a reinforcement learning method that improves a policy through self-play.
Polu et al. [] showed that a simple RL algorithm, expert iteration, paired with curriculum learning can improve a formal theorem proving model. Self-Taught Reasoner (STaR) [] 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. [] 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 []).
Our work builds on these ideas, providing the first study of bootstrapped thought-augmented proving.

Figure: 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.
Refer to caption: extracted/5782227/lean_star_example.png

## 3 Our Method: Lean-STaR

We introduce Lean-STaR, a new method for combining informal thoughts with formal theorem proving. First, we recap interactive theorem proving (§3.1). Then we present Lean-STaR’s data-generation (§3.2.1, §3.2.2) 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-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 in a complete proof of the given theorem.
We use Lean [], a popular interactive theorem prover. An example formal proof in Lean and its explanation are shown in Appendix C.

Figure: Figure 3: Examples of (input, output) pairs of retrospective rationale generation with GPT-4. The full prompt is given in Appendix F. See §3.2.2 for the detailed explanation.

### 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 (Lean-STaR).

#### 3.2.1 Direct Tactic Prediction

We define the theorem-proving problem as a Markov Decision Process (MDP) $(\mathcal{S},\mathcal{A},P_{a},R_{a})$ where proof states serve as states in MDP and tactics serve as actions.
From this perspective, a proof is a trajectory $(s_{1},a_{1},r_{1}),(s_{2},a_{2},r_{2}),\cdots$ of states $s_{i}$, tactics $a_{i}$, and rewards $r_{i}\in\mathbb{R}$, and the ITP (e.g., Lean) provides each new state $s_{i+1}$.

In the typical setting [], proving a theorem consists of providing a proof state $s$ to the language model and then generating a tactic from the language model $M$, i.e., $\pi_{M}(a|s)$.
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^{i},a^{i}):i=1,\cdots,M\}$, where final states have a reward of 1.
We refer to a language model fine-tuned on such a dataset as a supervised fine-tuning (SFT) model.

#### 3.2.2 Thought-augmented Tactic Prediction

Existing approaches typically train only on formal states and tactics []. 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_{i}$ prior to each tactic, and then extend the model to the form $\pi_{M}(a_{i},t_{i}|s_{i})=\pi_{M}(a_{i}|t_{i},s_{i})\pi_{M}(t_{i}|s_{i})$.
In thought-augmented tactic prediction, the distribution over the next tactic can then be expressed as:

$$ $\pi_{M}(a_{i}|s_{i})=\sum\limits_{t_{i}}\pi_{M}(a_{i}|t_{i},s_{i})\pi_{M}(t_{i }|s_{i}).$ $$

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-proving $\pi_{M}(t_{i}|s_{i})$ 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 [].
To develop a language model capable of generating thoughts and tactics $a_{i},t_{i}|s_{i}$, we need an entirely new dataset $D_{T}=\{(s^{i},t^{i},a^{i}):i=1,\cdots,N\}$.
However, in Lean, we only have a dataset of $D_{S}=\{(s^{i},a^{i}):i=1,\cdots,N\}$ where $(s^{i},a^{i})$ is one step in some successful proof trajectories.
Given a powerful large language model $G$, which we refer to as the oracle model(^2^22For instance, in our experiments we use the best available large language model, GPT-4.), we give the oracle model the ground-truth tactic $a_{i}$ and let the oracle model produce the thought $t_{i}$ given the current state $s_{i}$ and ground-truth tactic $a_{i}$. This helps improve the pass rate and produce thought-augmented data more efficiently.
Our few-shot prompt is provided in Appendix F.
The design principle of the prompt is to prevent the oracle model from generating hindsight-like thoughts.

We randomly select $M$ pairs $(s^{i},a^{i})\in D_{S}$ . Then the oracle model is used to produce a thought $t^{i}$ for each pair $(s^{i},a^{i})$ to create a new dataset $D_{T}\{(s^{i},t^{i},a^{i}):i=1,\cdots,M\}$. With this retrospectively annotated dataset by the oracle model $D_{T}$, we obtained our first thought-augmented tactic prediction model, Lean-CoT, by fine-tuning from the SFT model.

#### 3.2.3 Bootstrapping Thought-augmented 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 $M_{0}$ and the initial dataset $D=\{s^{i}:i=1,\cdots,M\}$, which consists of all initial states $s^{i}$ of the theorems to be proved. In iteration $1$, we use model $M$ to sample $K$ times per problem. Each time the model will produce a proof trajectory $[(s_{0},t_{0},a_{0}),(s_{1},t_{1},a_{1}),\cdots,(s_{n},t_{n},a_{n})]$. Then we create a new dataset $D_{1}$ by filtering the generated 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 $D_{T}\cup D_{1}$ to produce Lean-STaR model $M_{1}$. Then we can use $M_{1}$ as initial model to produce dataset $D_{2}$ and further fine-tune to obtain model $M_{2}$ in the next iteration.

This method can be seen as an offline RL method [] in the theorem proving MDP. In this MDP, the cumulative reward $R\left((s_{0},t_{0},a_{0}),(s_{1},t_{1},a_{1}),\cdots,(s_{n},t_{n},a_{n})
\right)=1$ if and only if the proof trajectory is successful. The total expected reward is

$$ $J(M,D)=\sum\limits_{i}\mathbb{E}_{(s_{0},t_{0},a_{0}),\cdots,(s_{n},t_{n},a_{n })\sim\pi_{M}(\cdot|s^{i})}R\left((s_{0},t_{0},a_{0}),\cdots,(s_{n},t_{n},a_{n })\right),$ $$

and Lean-STaR’s expert iteration can be seen as optimizing this reward [].

Figure: Figure 4: The diagram of our 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 a stopping condition is met (e.g., a fixed number of iterations).
Refer to caption: extracted/5782227/lean_star_pipeline.png

Figure: Figure 5: The visualization of Best-first Search ($K=1$) and Sampling ($S=1$). Search method maintains a search tree and explores $S$ tactics on each expanded node. Sampling method explores $K$ tactic trajectories from the root and ignores illegal tactics in the trajectories.
Refer to caption: extracted/5782227/search_vs_sampling_v2.png

### 3.3 Evaluation

##### Setup.

We evaluate the model on formal theorem proving – given a theorem statement, produce a theorem that is correct according to the formal system. This requires an algorithm for producing a full proof by interacting with Lean. As a new form of theorem-proving system, it is unclear what the best strategy is when we 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-first search), and our new approach based on sampling.

##### Best-First Search.

The most popular method to evaluate the theorem proving ability of a language model $M$ is to use best-first search like GPT-f [, , , ]. In best-first search, we keep all unexpanded states $s_{i}$. Each time, we expand the “best” state $s_{i}$ and use the language model to sample $S$ next tactics $a_{i,1\cdots S}$ for the current state $s_{i}$. For each legal tactic $a_{i,j}$, a new state can be obtained by applying tactic $a_{i,j}$ on state $s_{i}$.
Following standard practice [, , ], we assume the state with maximum log-probabilities is the “best”s. Specifically, we select state $s_{i}$ with maximum $\sum\limits_{j=0}^{i-1}\log p(a_{j},s_{j})$, where $(s_{0},a_{0}),\cdots,(s_{i-1},a_{i-1})$ is the proof trajectory before state $s_{i}$ and $\log p(a_{j},s_{j})$ is the average log probability of each generated token. We expand up to $N$ states and we get a successful proof search when we 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 performs poorly with the Lean-CoT and Lean-STaR models.
We attribute this to using average log probabilities, which may not be a reliable quality indicator when the thought sequence $t_{j}$ is generated.

##### Sampling.

Motivated by these issues with applying best-first search to thought-augmented 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 is $s_{i}$, the proof trajectory before $s_{i}$ is $(s_{0},a_{0}),\cdots,(s_{i-1},a_{i-1})$ and the sampled tactic is $a_{i}$. If $a_{i}$ is a legal tactic, $(s_{i},a_{i})$ will be added to the proof trajectory and we will reach a new state obtained by applying tactic $a_{i,j}$ on state $s_{i}$. Otherwise, we ignore this $a_{i}$ and use language model $M$ to sample a new tactic given state $s_{i}$. 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 our sampling method and best-first search with equal $S\times K$ took approximately the same amount of GPU time. This sampling method can easily accommodate hidden variable “thoughts” $t_{j}$.
Figure 5 compares best-first search and our sampling method.

## 4 Experiments

We instantiate Lean-STaR using the best available open language model pre-trained on the Lean corpus (InternLM2-Math-base-7b []), and follow standard practice in using Lean’s Mathlib as the underlying training set (via the Lean Dojo dataset []).
We generate an initial set of thoughts for Mathlib using GPT-4, perform two rounds of expert iteration, then evaluate the model on miniF2F [], the de-facto standard benchmark for evaluating language-model based theorem provers.
Our experimental results show that both retrospective rationale generation and expert iteration significantly improve the theorem-proving capabilities of language models in this setting.
We describe our setup and findings in detail below.

**Table 1: Pass rates on the minif2f-test 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 to be $1$ in sampling) and $K$ is 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. Note that we sample $32$ examples twice when $K=64$ in sampling.**
| Approach | Decoding | $N$ | $K$ | $S$ | Pass rate |
| --- | --- | --- | --- | --- | --- |
| GPT-3.5 [] (Few-Shot) | Sampling | 50 | 1 | 1 | $2.8\%$ |
| GPT-4 [] (Few-Shot) | Sampling | 50 | 1 | 1 | $11.9\%$ |
| Transformer [] (w/o RL) | Search | 512 | 1 | 8 | $24.6\%$ |
| Llemma-34b [] (Few-Shot) | Search | 50 | 1 | 32 | $25.8\%$ |
| Llemma-7b [] (Few-Shot) | Search | 50 | 1 | 32 | $26.2\%$ |
| ReProver [] | Search | 50 | 1 | 64 | $26.5\%$ |
| Transformer [] (w/ RL) | Search | 512 | 1 | 8 | $29.6\%$ |
| InternLM2-34b [] (Few-Shot) | Search | 50 | 1 | 32 | $29.5\%$ |
| COPRA (with GPT-4) [] | Customized | - | 60 | 1 | $29.9\%$ |
| COPRA (with GPT-4) [] | Customized | - | 100 | 1 | $30.7\%$ |
| InternLM2-7b [] (Few-Shot) | Sampling | 50 | 32 | 1 | $28.7\%$ |
| InternLM2-7b [] (Few-Shot) | Search | 50 | 1 | 32 | $30.3\%$ |
| SFT (InternLM2-7b) | Sampling | 50 | 32 | 1 | $29.5\%$ |
| SFT (InternLM2-7b) | Search | 50 | 1 | 32 | $30.7\%$ |
| Lean-CoT (InternLM2-7b) | Sampling | 50 | 32 | 1 | $32.8\%$ |
| Lean-STaR (Iter-1) (InternLM2-7b) | Sampling | 50 | 32 | 1 | $34.0\%$ |
| Lean-STaR (Iter-2) (InternLM2-7b) | Sampling | 50 | 32 | 1 | $\mathbf{34.8\%}$ |
| Lean-STaR (Iter-2) (InternLM2-7b) | Sampling | 50 | 64 | 1 | $\mathbf{36.1\%}$ |

### 4.1 Experimental Setup

We use LeanDojo Benchmark 4 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 a warmup in the first $20\%$ steps from 0 0 to $2\times 10^{-5}$, followed by a cosine schedule decaying to zero.

We randomly select $17,256$ different successful proof trajectories from LeanDojo Benchmark 4 dataset [], and use GPT-4-0125 [] to annotate $52,438$ thoughts from those proof trajectories. We filtered out all proof steps $(s^{i},a^{i})$ for which $a^{i}$ contains the newline symbol “\n” before annotating.
We perform two iterations of expert iteration, and provide the details in Appendix A.1 due to space.

We evaluate our method on the MiniF2F benchmark []. We use a similar evaluation setting as previous works [, , ], but use our sampling method instead of best-first search for the evaluation of our thought-augmented theorem proving model as discussed in (§3.3).
For each problem, Lean-STaR samples $K=32$ times in parallel with temperature $T=0.7$, and limits the number of times a tactic can be generated to a total of $N=50$. We also limit sampling to $10$ minutes per problem.
We choose these settings to resemble the inference budget used in our baselines, which follow previous work [, , ].
Namely, for best-first search baselines we use beam search to generate the next tactic with $S=32,K=1$ [, , ]. We do not compare with methods designed for other formal languages such as Jiang et al. [], Xin et al. [] since language differences greatly influence the pass rate due to the different tactics and automation.
We also do not compare with Lample et al. [] since they only report $S=32,K=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.

**Table 2: 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-STaR significantly improves Number Theory performance.**
| TOTAL | Test Set<br>Size | InternLM2-7b | SFT | Lean-CoT | Lean-STaR<br>(Iter-2) |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- |
| IMO | 20 | 0 | 0 | 0 | 0 |  |  |
| AIME | 15 | 2 | 1 | 2 | 3 |  |  |
| AMC | 45 | 3 | 3 | 7 | 5 |  |  |
| MATH | Algebra | Level 5 | 14 | 1 | 2 | 3 | 3 |
| Level 4 | 14 | 7 | 7 | 7 | 7 |  |  |
| Level 3 | 14 | 9 | 9 | 11 | 11 |  |  |
| Level 2 | 14 | 10 | 10 | 9 | 11 |  |  |
| Level 1 | 14 | 9 | 10 | 10 | 10 |  |  |
| Number Theory | Level 5 | 16 | 6 | 6 | 6 | 7 |  |
| Level 4 | 11 | 5 | 5 | 4 | 5 |  |  |
| Level 3 | 11 | 4 | 5 | 5 | 6 |  |  |
| Level 2 | 11 | 6 | 5 | 5 | 6 |  |  |
| Level 1 | 11 | 8 | 8 | 9 | 9 |  |  |
| CUSTOM | Algebra | 18 | 0 | 1 | 1 | 1 |  |
| Number Theory | 8 | 0 | 0 | 0 | 0 |  |  |
| Induction | 8 | 0 | 0 | 1 | 1 |  |  |

### 4.2 Main Results

Our main results are reported in Table 1.
Lean-STaR gives a significant improvement over the previous state-of-the-art in Lean.
For instance, with a similar inference budget, Lean-STaR achieves 34.8% versus $30.3\%$ in InternLM2 [] using best-first search and $30.7\%$ in COPRA [] using GPT-4.
With a larger compute budget, Lean-STaR’s performance improves further to 36.1%.

**Table 3: Pass rates about InternLM2-Plus-7B on the minif2f-test 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 to be $1$ in sampling) and $K$ is 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. Note that we sample $32$ examples twice when $K=64$ in sampling. In search we follow the setup in [] and limit each search to $20$ minutes.**
| Approach | Decoding | $N$ | $K$ | $S$ | Pass rate |
| --- | --- | --- | --- | --- | --- |
| InternLM2-plus-7b [] (Few-Shot) (from paper) | Search | 1000 | 1 | 32 | $43.4\%$ |
| InternLM2-plus-7b [] (Few-Shot) (reproduced) | Search | 1000 | 1 | 32 | $42.6\%$ |
| InternLM2-plus-7b [] (Few-Shot) | Sampling | 50 | 32 | 1 | $40.9\%$ |
| SFT (InternLM2-plus-7b) [] (Few-Shot) | Sampling | 50 | 32 | 1 | $41.3\%$ |
| Lean-CoT (InternLM2-plus-7b) | Sampling | 50 | 32 | 1 | $43.4\%$ |
| Lean-STaR (Iter-1) (InternLM2-plus-7b) | Sampling | 50 | 32 | 1 | $45.4\%$ |
| InternLM2-plus-7b [] (Few-Shot) | Sampling | 50 | 64 | 1 | $42.2\%$ |
| SFT (InternLM2-plus-7b) [] (Few-Shot) | Sampling | 50 | 64 | 1 | $43.4\%$ |
| Lean-CoT (InternLM2-plus-7b) | Sampling | 50 | 64 | 1 | $45.5\%$ |
| Lean-STaR (Iter-1) (InternLM2-plus-7b) | Sampling | 50 | 64 | 1 | $\mathbf{46.3\%}$ |

##### Thought augmentation improves theorem proving.

The first phase of Lean-STaR trains a model to interleave thoughts and tactics, by fine-tuning on a synthesized dataset of thought-augmented examples.
The fine-tuned model from this phase, denoted Lean-CoT in Table 1, 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 is already specialized for generating tactics in Lean such as the SFT model.

##### Bootstrapping improves thought-augmented 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-augmented dataset and the saved examples (i.e., expert iteration [, , ]).
Refer to Appendix A.1 for details.

We perform two iterations of expert iteration, and present the results in Table 1, 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, we find that the model is amenable to further improvement via additional sampling, achieving 36.1% 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.

### 4.3 Performance 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 [].
These problems can have different levels of difficulty and types. Table 2 reports the number of 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.

**Table 4: Performence of SFT-Direct and our Lean-STaR at different search size or sampling times $S\times K$. We fix $N=50$. We use beam search in search and temperature $T=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 $K=64$ in sampling.**
|  | SFT-Direct (Search) | SFT-Direct (Sampling) | Lean-STaR (Iter-2) (Sampling) |
| --- | --- | --- | --- |
| $S\times K=1$ | $13.5\%$ | $20.9\%$ | $21.7\%$ |
| $S\times K=2$ | $18.0\%$ ($+4.5\%$) | $22.5\%$ ($+1.6\%$) | $24.6\%$($+2.9\%$) |
| $S\times K=4$ | $23.3\%$ ($+5.3\%$) | $25.0\%$ ($+2.5\%$) | $27.5\%$($+2.9\%$) |
| $S\times K=8$ | $27.5\%$ ($+4.2\%$) | $27.0\%$ ($+2.0\%$) | $30.7\%$ ($+3.2\%$) |
| $S\times K=16$ | $29.9\%$ ($+2.4\%$) | $28.3\%$ ($+1.3\%$) | $33.6\%$ ($+2.9\%$) |
| $S\times K=32$ | $30.7\%$ ($+0.8\%$) | $29.5\%$ ($+1.2\%$) | $34.8\%$ ($+1.2\%$) |
| $S\times K=64$ | $30.7\%$ ($+0.0\%$) | $30.3\%$ ($+0.8\%$) | $36.1\%$ ($+1.3\%$) |

### 4.4 Search and sampling budget

Table 4 reports the trends of the pass rate against the search size or sampling budget $S\times K$. We find that Lean-STaR benefits more as $K$ increases, especially when $K$ is relatively large. The result suggests that additional sampling with thoughts improves performance, while additional sampling without thoughts may saturate. We believe this is because thoughts increase the diversity of outputs and contribute to exploration in the theorem proving space. Therefore, Lean-STaR is more scalable (in terms of inference-time compute), and may be amenable to further improvements with additional iterations of expert iteration.

### 4.5 Experiments with stronger base model and more data

We instantiate Lean-STaR using a stronger language model (InternLM2-Math-plus-7b []), which was released after the experiment above. We follow a similar setup to the previous experiment.

In this experiment, we used $140,000$ thoughts annotated by GPT-4o [] to fine-tune a 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” $D_{1}$. We further fine-tuned the Lean-CoT model on dataset $D_{1}$ to get the Lean-STaR model.

Our new results are reported in Table 3.
We can see that Lean-STaR still gives a significant improvement over the baseline. For instance, Lean-STaR achieves $45.4\%$ versus $39.8\%$ in InternLM-plus using sampling with a similar inference budget and $43.4\%$ using best-first search with more inference budget reported in [].
This results show that both retrospective rationale generation and expert iteration can improve the theorem-proving capabilities on a stronger base model.

### 4.6 Experiments on expert iteration without CoT

Table 5 shows the result of expert iteration without CoT (i.e., using (state, tactic) pairs only) as well as the result of Lean-CoT and Lean-STaR.
Expert iteration alone achieves 43.0%, which is less than Lean-STaR (45.4%).
This shows that Lean-STaR’s performance gains do not only come from the use of expert iteration.

**Table 5: Results for the InternLM2-plus-7b and our Lean-CoT, Lean-STaR, and expert iteration without CoT. We use sampling with $N=50,K=32,\&\ T=0.7$.**
| Approach | # (Continual) Training Data | Pass@32 |  |
| --- | --- | --- | --- |
| InternLM2-plus-7b (Few-Shot) | - | $40.9\%$ | - |
| SFT | $231,240$ | $41.3\%$ | $+0.4\%$ |
| Lean-CoT | $140,000$ | $43.4\%$ | $\mathbf{+2.1\%}$ |
| Lean-STaR | $60,000$ | $45.5\%$ | $\mathbf{+2.1\%}$ |
| Expert iteration (SFT) | $60,000$ | $43.0\%$ | $+1.7\%$ |

## 5 Conclusion & Limitations

In this paper, we presented Lean-STaR, a novel approach that significantly enhances the theorem-proving capabilities of language models in formal mathematics by integrating Chain-of-Thought (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 tactics, resulting in the Lean-CoT model. We further improved this model using expert iteration, fine-tuning it on 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 state-of-the-art results on the miniF2F-test benchmark, increasing the pass rate from $30.3\%$ to $36.1\%$. These advancements are 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 [, , , , , ].

The primary limitation of our 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 is not very large. Additionally, the use of GPT-4 to generate synthetic data may incur a significant cost and possibly introduce biases. Also, expert iteration could face a bottleneck due to CPU and IO limitations, which might slow down the process due to a sluggish speed of Lean ITP.

## Appendix A Additional Experiment Setup

### A.1 Lean-STaR Expert Iteration

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-augmented dataset and the saved examples (i.e., expert iteration [, , ]).
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 $K=32$ times in parallel with temperature $T=1.0$, and limit the number of times a tactic can be generated to a total of $N=5$ per problem. Also, sampling is limited to $1$ minute per problem. In this setup, each problem needs on average about $0.5$ A100 minutes. We collect successfully sampled trajectories to produce a “STaR dataset” $D_{1}$, 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\times A100$ GPUs. Then, we further fine-tune SFT model for $1$ epoch on the combination of GPT-4 annotated reasoning data and expert iteration data $D_{T}\cup D_{1}$ to get the Lean-STaR model.
We use the same learning rate setup that was used for the SFT model.
In the second iteration, we generate a dataset $D_{2}$ in a similar fashion. Then, we chose to further fine-tune model from iteration $1$, $M_{1}$, on the generated dataset $D_{2}$ (roughly 19k pairs).

The setup of experiment about InternLM2-plus is slightly different. The details are shown in Section  4.5 and Appendix  E.

## Appendix B Statistics for our methods as well as the baselines

**Table 6: Statistics for the baselines and our Lean-CoT, Lean-STaR on MiniF2F dataset. We use sampling method with hyperparameters $N=50\ \&\ K=32\ \&\ T=0.7$.**
| Approach | # (Continual) Training Data | Pass@32 |  |
| --- | --- | --- | --- |
| InternLM2-Math-7b (Few-Shot) | - | $28.7\%$ | - |
| SFT | $231,240$ | $29.5\%$ | $+0.8\%$ |
| Lean-CoT | $52,438$ | $32.8\%$ | $\bm{+3.3\%}$ |
| Lean-STaR (Iter-1) | $32,231$ | $34.0\%$ | $+1.2\%$ |
| Lean-STaR (Iter-2) | $19,324$ | $\mathbf{34.8\%}$ | $+0.8\%$ |

## Appendix C An Example and Explanation of A Formal Proof in Lean

An example of a formal proof in Lean with its visualization is shown in Figure 6, taken from []. In the proof, the tactic induction k is is applied to the initial state ($n\leq m\Rightarrow n+k\leq m+k$) and the ITP converts the current state to subgoals case 0 $\land$ case ih: $n\leq m\land n+k\leq m+k\Rightarrow n+(k+1)\leq m+(k+1)$. The case 0: $n\leq m$ is our hypothesis $h_{0}$ so it can be proven by case 0:exact $h_{0}$ tactic. Then, we rewrite the case ih through the nat.succ_le_succ_iff which is a theorem in Lean library means $n\leq m\Leftrightarrow n+1\leq m+1$. After tactics case 0:exact $h_{0}$ and case ih:rw nat.succ_le_succ_iff, the goal state is converted to $n+k\leq m+k$ which is the hypothesis introduced by induction. Therefore, we can complete this proof using tactic exact k_ih.

Figure: Figure 6: A example proof and its visualization of $n\leq m\Rightarrow n+k\leq m+k$ in Lean, taken from []. The induction tactic reduces the initial statement to two subgoals. Then tactics case 0:exact $h_{0}$ and case ih:rw nat.succ_le_succ_iff, case ih:exact k_ih can be applied in turn to complete the proof.
Refer to caption: extracted/5782227/visualization.png

## Appendix D Performance Analysis by Types and Difficulties using InternLM2-plus-7b

Table 7 reports the number of problems successfully proved, partitioned by type and difficulty using InternLM2-plus. We see that Lean-CoT improves performance mainly in Number Theory and Lean-STaR improves performance in solving difficult problems on all categories, which is the opposite of the performance of the InternLM2-base.

**Table 7: Counts of problems successfully proved in minif2f-test benchmark using InternLM2-plus-7b, split by type and difficulty. The methods use sampling with $N=50,K=32$.**
| TOTAL | Test Set<br>Size | InternLM2-plus-7b | Lean-CoT | Lean-STaR<br>(Iter-1) |  |  |
| --- | --- | --- | --- | --- | --- | --- |
| IMO | 20 | 0 | 0 | 0 |  |  |
| AIME | 15 | 3 | 3 | 4 |  |  |
| AMC | 45 | 9 | 9 | 10 |  |  |
| MATH | Algebra | Level 5 | 14 | 6 | 6 | 6 |
| Level 4 | 14 | 9 | 9 | 9 |  |  |
| Level 3 | 14 | 11 | 13 | 13 |  |  |
| Level 2 | 14 | 11 | 11 | 11 |  |  |
| Level 1 | 14 | 10 | 10 | 10 |  |  |
| Number Theory | Level 5 | 16 | 7 | 7 | 7 |  |
| Level 4 | 11 | 6 | 8 | 8 |  |  |
| Level 3 | 11 | 6 | 7 | 9 |  |  |
| Level 2 | 11 | 7 | 9 | 9 |  |  |
| Level 1 | 11 | 10 | 10 | 10 |  |  |
| CUSTOM | Algebra | 18 | 4 | 3 | 4 |  |
| Number Theory | 8 | 0 | 0 | 0 |  |  |
| Induction | 8 | 1 | 1 | 1 |  |  |

## Appendix E Performance difference of joint training and continue training

As shown in Table 8, the joint training method performs better using InternLM2-base but training method performs much better using InternLM2-plus. It seems that there are no difference between these two methods. Therefore, this performance can be depend on the quantity of data or the model. (We use much more data when using InternLM2-plus and the quantity of "STaR data" is relatively small.)

**Table 8: 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 in joint training we fine-tune the SFT model on combination of GPT-4 annotated reasoning data and "STaR data".**
| Approach | InternLM2-base-7b | InternLM2-plus-7b |
| --- | --- | --- |
| Lean-CoT | $32.8\%$ | $43.4\%$ |
| Lean-STaR (Iter-1)<br>(joint training) | 34.0% | $43.9\%$ |
| Lean-STaR (Iter-1)<br>(continue training) | $33.2\%$ | 45.5% |

## Appendix F Retrospective Rationale Generation Prompt of GPT-4

## Appendix G Examples of generated Lean proofs with thoughts

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
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?

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

- In Lines 372 and 398, should 'Table 7' be corrected to 'Table 1'?

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

- On Line 449, where does the 39.8% figure originate? Should it be 34.0% instead?
soundness: 4
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.
- The newly proposed sampling method is novel and, based on its performance, appears to be a promising approach compared to Best-First Search.
- The proposed CoT-augmented dataset should be useful for future research in neural theorem proving.
- The paper is well-written and easy to follow.
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.
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.
- 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.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 2
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.
- Is there an intuitive reason why sampling works better than best first-search for your method?
soundness: 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. 
- There are numerous experiments.
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.
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).

- 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.
- Automatic theorem proving and interactive theorem proving are used interchangeably throughout the text even though they are not the same concept.
- 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. 
- 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).
- Table 7 -> Table 1.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 4
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.
soundness: 3
strengths: **1. Simple yet very effective approach:**
The 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.

**2. Use of expert iteration while informal thought generation:**
While 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.

**3. Search based on Sampling:**
The 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.
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.
weaknesses: **1. Data Leakage:**
While 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.

It is a well-written paper, I will be more than happy to increase my score if the authors address some of my concerns.

---

confidence: 5
contribution: 3
initial_rating: 6
presentation: 3
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.

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

3. Minor suggestions: A few works that appear related to this paper, which the authors may consider citing/discussing.

* [1] Multilingual Mathematical Autoformalization. Albert Q. Jiang, Wenda Li, Mateja Jamnik. arXiv 2311.03755. 2023.

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

* [2] Towards Large Language Models as Copilots for Theorem Proving in Lean. Peiyang Song, Kaiyu Yang, Anima Anandkumar. arXiv 2404.12534.

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

* 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.
soundness: 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.

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

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

1. The first thought (informal language) augmented for theorem proving in Lean (formal math).
2. Lean-STaR: a framework which combines tactic prediction, thought augmentation with synthetic data, and two iterations of expert iteration.
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.

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

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

Meta-review: This paper proposes a novel framework, Lean-STaR, which interleaves informal reasoning in natural language (or "thoughts") with formal reasoning in Lean (tactic prediction). The Lean-STaR framework combines several interesting techniques including LLM fine-tuning, self-taught reasoner, and expert iteration; although each idea is not new, the combination in theorem proving regarding leveraging informal reasoning is novel. The effectiveness of Lean-STaR has been shown convincingly through extensive experimental evaluations. Overall, Lean-STaR is an instance of a much general and promising framework with great potentials in theorem proving.

Decision: Accept (Spotlight)