Lean-STaR: Learning to Interleave Thinking and Proving

Thank you for your insightful and positive feedback on our paper. We are glad that you appreciate our CoT-based method and dataset.

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

Please see the “verification mechanism or filtering process” part under the General Response.. The STaR process will filter out lower quality CoT from the synthetically generated data for further finetuning.

Concern 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 ablation result is shown in Table 3 in our paper. The final line “Expert iteration (SFT)” is the case that all other settings (expert iteration, tactic prediction) are kept as-is but no thought augmentation is added.

Concern 3: Is it possible that InternLM2-Math-base-7b may have been exposed to parts of the test data?

Our experimental setting (fine-tuning on Mathlib, evaluating on miniF2F) follows a widely used experimental setup in benchmark evaluations in neural theorem proving (e.g., InternLM was evaluated on miniF2F). Therefore, we believe that InternLM2-Math-base-7b has not been exposed to miniF2F.

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

It is about 300 input tokens and 300 output tokens on average for each case. Therefore, it costs about 3.75 for 1K data for using current GPT-4o. It mounts to about 200 for our 52,438 cases.

Question 2: I was wondering if a bottleneck would be hit very soon, or would the framework continue to benefit from more iterations?

Thank you for the question! We believe the framework could benefit from more iterations and potentially improve performance further. However, the Leandojo environment has a significant CPU bottleneck, making additional iterations very time-consuming. This is an exciting direction for future work, and with better compute resources, we expect the framework could achieve even greater results.

Thank you for your constructive and positive feedback. We are glad that you appreciate our CoT-based method and dataset.

Concern 1: COT is the absence of a verification mechanism or alternative methods to ensure its quality.

Please see the “verification mechanism or filtering processGPT-4 used in CoT generation” part under the General Responses. In short, we do have a filtering process for quality control of the GPT-4 generated COT in the STaR process.

Concern 2: Why the performance of COT in NTP is not as strong as it is in MWP.

In MWP without CoT, language models will directly give the answer. Therefore, part of the benefit of the CoT in our approach comes from that it lets the model think step by step. However, NTP is essentially step by step, so COT in NTP benefits only from combining informal thinking, which is not as strong as it is in MWP. A better analogy of MWP w/o CoT to NTP would be that the model sees the MWP problem, generates the equation for solving the problem, and the equation is symbolically solved by an external calculator

Question 1: 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?

Please see the “verification mechanism or filtering processGPT-4 used in CoT generation” part under the General Responses. In short, we do have filtering process for quality control of the GPT-4 generated COT in the STaR process. We also agree with the reviewer that only using states and ground truth tactics is just the most direct and simple approach, and that Incorporating additional proving context is worth exploring in future research.

Question 2: 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?

'N' in 'Search' refers to the total number of expansions as mentioned in Line 285 in our paper. However, 'N' in 'Sampling' refers to the number of all attempts (whether success or not). I.e., 'N' in 'Sampling' refers to the total number of tactics generated in one sampling process as mentioned in Line 293 in our paper.

Question 3: In Lines 372 and 398, should 'Table 7' be corrected to 'Table 1'?

Yes, that is a typo. Thank you for the feedback.

Question 4: 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?

Yes, InternLM model uses this leandojo training dataset in pre-training.

Question 5: On Line 449, where does the 39.8% figure originate? Should it be 34.0% instead?

Yes, that is a typo. Thank you for the feedback.

Thanks for your detailed explanations.

Regarding my major concern, I think using the LLM to generate new tactics with the COT and testing their efficacy seems sufficient. Personally, I cannot think of another low-cost, effective method for this purpose. However, I am curious about the robustness of this filtering approach. Do you have any ablation study results that compare models trained with and without this filtering method? I believe including such an experiment in the paper would be valuable.

For the other concerns and questions, your explanations have been adequate. I am now leaning towards acceptance.

Thank you for your thoughtful comments and raising the score!

To address your query, the COT model can be viewed as the version trained without the filtering method, as this "filtering" process is an integral part of STaR and not easily isolated. If you are interested in a comparison, we suggest referring to the results of LeanCOT versus LeanSTaR, which might provide the insight you’re looking for.

We truly appreciate your feedback and are happy to clarify further if needed.

Thank you for your insightful review. We are glad that you appreciate our Lean-STaR method and found our paper well-written.

Question 1:Data Leakage

Our experimental setting (fine-tuning on Mathlib, evaluating on miniF2F) follows a widely used experimental setup in benchmark evaluations in neural theorem proving (e.g., InternLM was evaluated on miniF2F). Therefore, we believe that InternLM2-Math-base-7b has not been exposed to miniF2F. Also, GPT-4 is only used for synergizing the informal thoughts of the Mathlib dataset. It should not cause data leakage since problems in Mathlib and miniF2F are quite different.

Thank you for your thoughtful comments！Following your suggestion, we do an analysis similar to the analysis in https://arxiv.org/pdf/2310.04353. The result is shown in the following table. From the following table, we can see 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 as the proofs mentioned in the miniF2F.

Thank you for your insightful review of our paper. We're glad to hear that you appreciate our Lean-STaR method in formal theorem proving. We address your questions below.

Concern 1: 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.

We understand the reviewer’s concern regarding the abbreviations and terminology. To clarify:

1. Following the convention in LLM post-training, the SFT model specifically refers to a model that is fine-tuned on the instruction-tuning dataset (i.e., Leandojo dataset in our paper). However, not all models designed for direct tactic prediction are SFT models. For example, a pretrained model that skips the SFT phase could still perform direct tactic prediction but would not qualify as an SFT model.
2. The term thought-augmented dataset refers to data that includes chain-of-thought (CoT) annotations. We abbreviate this as the CoT dataset.
3. Lastly, the Lean-STaR model is the product of the Lean-STaR framework. Although the same name is used for both, this follows a common practice in LLM research where frameworks and their outputs often share a name (e.g., RLHF algorithm and RLHF models, PPO algorithm and PPO models).

We hope this clarification addresses the concern and aligns our terminology with established conventions in the field.

Concern 2: Automatic theorem proving and interactive theorem proving are used interchangeably throughout the text even though they are not the same concept.

We use “interactive theorem proving” (Section 3.1) to mean a proving environment like Lean while we use “automatic theorem proving” to mean the task we solve. We hope this is clear.

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

Sorry for the confusion in Figure 3. Arrows there means we use some model/dataset to produce a new model/dataset. For example, we use Base dataset and GPT-4 to produce CoT Dataset, and we use Lean-CoT model and Base dataset to produce Lean-STaR model. We will update the caption to make it more clear.

Question 1: 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. 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.

We would like to clarify that the thought (CoT) is treated as a strictly latent variable in our framework. For a given proof context, the model first generates a thought from the distribution p(thought | proof context), and then generates a tactic conditioned on both the thought and the proof context, using p(tactic | thought, proof context). The overall distribution of the tactic given the proof context is thus computed as p(tactic | proof context) = Expectation_{thought ~ p(thought | proof context)} p(tactic | thought, proof context), meaning it marginalizes over all possible thoughts. During evaluation, thoughts are dynamically generated for each proof context, which ensures that the process reflects the marginalization. Regarding fairness, both our method and direct tactic prediction rely solely on the proof context as input. The difference is that our approach explicitly models an intermediate reasoning step by generating thoughts before predicting tactics, while direct tactic prediction skips this step and directly maps the proof context to the tactic. This decomposition does not provide additional input information but introduces informal reasoning through the latent variable. Thus, the comparison is fair as both methods are ultimately conditioned on the same proof context.

Question 2: Is there an intuitive reason why sampling works better than best first-search for your method?

In Section 3.3, we claim that the sampling method performs better when using thought based models, and hypothesize that it may be because the average log probabilities used in the Best First Search method could be unreliable with the natural language-based CoT thoughts.

We're happy to clarify any confusion further.

Can you please justify how to convert sampling P(tactic, thought | proof context) to sampling P(tactic | proof context) unless you marginalize P(tactic, thought | proof context) with respect to thoughts?

When sampling $(x, y) \sim P(X, Y \mid Z)$, the likelihood of obtaining a specific $X = x$ is given by the law of total probability:

P(X = x \mid Z) = \sum_y P(X = x, Y=y \mid Z) \quad \text{(for discrete Y)},

or equivalently,

P(X = x \mid Z) = \int P(X = x, Y=y \mid Z) dy \quad \text{(for continuous Y)}.

This corresponds directly to the definition of the marginal distribution $P(X \mid Z)$.

Consequently, to draw a sample from $P(\text{tactic} \mid \text{proof context})$, one can simply sample from $P(\text{tactic}, \text{thought} \mid \text{proof context})$, and then discard the $\text{thought}$. This approach is exactly what we implemented in our method.