Lean-STaR：学习交错思考与证明
Lean-STaR: Learning to Interleave Thinking and Proving
AI总结：
本文提出 Lean-STaR 框架，让语言模型在每个证明步骤前生成非形式化思考，并结合专家迭代提升性能，在 miniF2F-test 上取得 Pass@64 46.3% 的最优结果。
摘要：
传统的基于语言模型的定理证明假设，通过在足量形式化证明数据上训练，模型将学会证明定理。我们的关键观察是，形式化证明中不存在的大量非形式化信息，可能有助于学习证明定理。例如，人类会通盘思考证明的各个步骤，但这种思考过程在最终代码中并不可见。我们提出 Lean-STaR，这是一个训练语言模型在每个证明步骤之前产生非形式化思考的框架，从而提升模型的定理证明能力。Lean-STaR 使用回顾性的真实策略（tactic）来生成合成思考，用于训练语言模型。在推理时，经过训练的模型会在每个证明步骤预测策略之前直接生成这些思考。在 self-taught reasoner 框架的基础上，我们随后应用专家迭代（expert iteration），在模型采样并使用 Lean 求解器验证的正确证明上进一步微调模型。Lean-STaR 在 Lean 定理证明环境中的 miniF2F-test 基准上取得了最先进结果，显著优于基础模型（43.4% → 46.3%，Pass@64）。我们还分析了增强思考对定理证明过程各方面的影响，为其有效性提供了洞见。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
