Lean-STaR: Learning to Interleave Thinking and Proving

TL;DR

Lean-STaR introduces a novel approach where language models generate informal thoughts before proof steps, significantly improving theorem-proving performance by leveraging additional reasoning context.

Contribution

The paper presents Lean-STaR, a framework that trains models to produce informal thoughts prior to proof steps, enhancing proof accuracy and state-of-the-art results on miniF2F.

Findings

Achieves 46.3% Pass@64 on miniF2F benchmark

Outperforms baseline models significantly

Provides insights into the role of informal thoughts in proof success

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 ($\boldsymbol{43.4\% \rightarrow 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.