Lean-STaR: Learning to Interleave Thinking and Proving

传统的基于语言模型的定理证明假设，通过训练足够数量的形式证明数据，模型将学会证明定理。我们的关键观察是，大量的非正式信息对于学习证明定理是有用的，这些信息在形式证明中并不存在。例如，人类会思考证明的步骤，但这个思考过程在最终的代码中是看不到的。我们提出了Lean-STaR框架，用于训练语言模型在每个证明步骤之前生成非正式的思考，从而提高模型的证明定理能力。Lean-STaR使用回顾性的真实策略来生成合成思考，以训练语言模型。在推理时，训练好的模型直接在每个证明步骤的策略预测之前生成思考。在自学推理器框架的基础上，我们进一步应用专家迭代，以在使用Lean求解器验证的正确证明上进一步微调模型。Lean-STaR在Lean定理证明环境中的miniF2F-test基准测试中取得了最新的结果，显著优于基本模型（$\boldsymbol{43.4\% \rightarrow 46.3\%,}$ Pass@64）。我们还分析了增强的思考对定理证明过程的各个方面的影响，提供了有关其有效性的见解。

该论文旨在通过训练语言模型生成 informal thoughts 来提高定理证明的能力。论文探讨了传统基于语言模型的定理证明方法的局限性，并提出了一种新的思路。

Lean-STaR 框架通过生成 informal thoughts 来训练语言模型，从而提高定理证明的能力。该框架使用回顾性的真实策略来生成合成 thoughts，然后在推理时，模型直接生成每个证明步骤中的 thoughts。此外，论文还使用专家迭代来进一步微调模型。

该论文的亮点包括：1. 使用 informal thoughts 来增强语言模型的定理证明能力；2. 使用回顾性的真实策略生成合成 thoughts 以训练模型；3. 使用专家迭代来微调模型；4. 在 miniF2F-test 基准测试中取得了最先进的结果，显著优于基础模型；5. 论文分析了增强 thoughts 对定理证明过程各方面的影响，并提供了有关其有效性的见解。

在这个领域中，最近的相关研究包括：1. 使用深度学习方法进行定理证明的研究；2. 使用强化学习来指导证明搜索的研究；3. 使用自动化技术来简化证明的研究。