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）。我们还分析了增强思考对定理证明过程各个方面的影响，提供了有关其有效性的见解。

本文试图提出一种新的框架，通过训练语言模型来生成证明前的非正式想法，以提高模型的证明能力。这个框架的目标是解决传统基于语言模型的定理证明方法无法利用非正式信息的问题。

Lean-STaR框架使用回溯的ground-truth策略来为语言模型生成合成的想法，以训练模型。在推理时，经过训练的模型直接在每个证明步骤的策略预测之前生成想法。然后，通过专家迭代来进一步微调模型。Lean-STaR在miniF2F-test基准测试中取得了最先进的结果。

本文提出了一种新的框架，通过训练语言模型来生成证明前的非正式想法，以提高模型的证明能力。Lean-STaR框架使用回溯的ground-truth策略来为语言模型生成合成的想法，以训练模型。实验结果表明，该框架在miniF2F-test基准测试中取得了最先进的结果。此外，本文还分析了增强想法对定理证明过程各个方面的影响，并提供了一些见解。

在最近的相关研究中，也有一些关于使用语言模型来进行定理证明的研究。例如，Neural Theorem Prover和DeepMath都是基于语言模型的定理证明方法。