# Lean-STaR: Learning to Interleave Thinking and Proving

**Authors:** Haohan Lin, Zhiqing Sun, Yiming Yang, Sean Welleck  
**arXiv:** [2407.10040](https://arxiv.org/abs/2407.10040)  
**Date:** 2024-07-14  
**Summary page:** https://www.summarizepaper.com/en/paper/2407.10040v3/

## Key points

- Lean-STaR is a groundbreaking approach that enhances theorem-proving capabilities of language models in formal mathematics.
- Methodology involves generating synthetic rationales using ground-truth tactics retrospectively and fine-tuning the language model to generate these rationales and predict subsequent tactics.
- Development of Lean-CoT model through expert iteration on correct proofs sampled and verified using the Lean solver.
- Noteworthy contributions include introducing the first thought-augmented theorem proving dataset, showcasing effectiveness of expert iteration, and achieving new state-of-the-art results on miniF2F-test benchmark with increased pass rate from 30.3% to 36.1%.
- Advancements improve automated theorem proving accuracy and offer a scalable framework for advancing human understanding of mathematics, impacting education, scientific discovery, and program verification.
- Limitations include computational scalability issues, small dataset for fine-tuning Lean-CoT and Lean-STaR affecting generalizability, potential biases from utilizing GPT-4 for synthetic data generation, bottlenecks in expert iteration due to CPU and IO limitations.
- Focus on integrating informal thoughts into formal mathematics sets the approach apart from existing methods in automatic theorem proving.
- Bridging gap between informal human thinking processes and formal proof generation aims to revolutionize automated theorem proving methodologies for enhanced efficiency and accuracy in mathematical reasoning applications.

## Summary

, , , , 

In this paper, we present Lean-STaR, a groundbreaking approach that significantly enhances the theorem-proving capabilities of language models in formal mathematics. Our methodology involves generating synthetic rationales using ground-truth tactics retrospectively and fine-tuning the language model to generate these rationales and predict subsequent tactics. This results in the development of the Lean-CoT model, which we further refined through expert iteration on correct proofs sampled and verified using the Lean solver. Noteworthy contributions of our work include introducing the first thought-augmented theorem proving dataset, showcasing the effectiveness of expert iteration in enhancing performance, and achieving new state-of-the-art results on the miniF2F-test benchmark with a notable increase in pass rate from 30.3% to 36.1%. These advancements not only improve automated theorem proving accuracy but also offer a scalable and efficient framework for advancing human understanding of mathematics. This could have significant impacts in education, scientific discovery, and program verification. However, it is important to acknowledge limitations of our method. One primary constraint is computational scalability issues that may impact performance. Both Lean-CoT and Lean-STaR have been fine-tuned on a relatively small dataset, which could affect their generalizability. Additionally, utilizing GPT-4 for generating synthetic data may come with a significant cost and potential biases. Moreover, expert iteration might face bottlenecks due to CPU and IO limitations, leading to slower processing speeds attributed to Lean ITP's sluggishness. In terms of related work, previous studies on learning-based theorem proving typically follow frameworks like GPT-f for training language models on (proof state, next-tactic) pairs to prove theorems within best-first tree search methods. Our focus on integrating informal thoughts into formal mathematics sets us apart from existing approaches in automatic theorem proving. Furthermore, recent research has shown that allowing language models to reason before providing an answer can enhance their performance across various tasks including math, science, and code-related challenges. While techniques like Scratchpad and Chain-of-Thought have demonstrated effectiveness in improving reasoning abilities of language models, they often require extensive annotated training examples or exposure to numerous similar instances during pre-training. Overall, our work represents a significant advancement in thought-augmented reasoning within automatic theorem proving systems like Lean-CoT and Lean-STaR. By bridging the gap between informal human thinking processes and formal proof generation through language models, we aim to revolutionize automated theorem proving methodologies for enhanced efficiency and accuracy in mathematical reasoning applications.