InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems

大型语言模型（LLMs）在数学定理证明中已经崭露头角，尤其是在使用如LEAN这样的形式语言时。主要的学习范式是专家迭代，这需要一个预先定义的数据集，包含大量数学问题。在这个过程中，LLMs会尝试证明数据集中的问题，并通过自我训练发现的证明来逐步优化其能力。我们提议使用大规模的LEAN问题数据集Lean-workbook进行专家迭代，该数据集包含超过20,000个CPU天的任务。在专家迭代过程中，我们发现已解决的问题数量与证明长度和CPU使用量之间存在对数线性关系。我们训练了一个评估模型，用于选择相对简单的问题供策略模型进行尝试，并引导模型搜索更深层次的证明。InternLM2.5-StepProver在MiniF2F、Lean-Workbook-Plus、ProofNet和Putnam基准测试中取得了开源领域的最佳成绩。具体来说，它在MiniF2F-test上达到了65.9%的通过率，并且在Lean-Workbook-Plus中证明（或反驳）了17.0%的问题，相比Lean-Workbook-Plus发布时仅能证明9.5%的问题，这是一个显著的提升。我们已将我们的模型和搜索到的证明开源，相关资源可在以下网址获取：https://github.com/InternLM/InternLM-Math 和 https://huggingface.co/datasets/internlm/Lean-Workbook。

该论文试图通过使用大规模LEAN问题数据集来提高大型语言模型（LLMs）在数学定理证明中的性能。这是一个具有挑战性的问题，特别是在利用形式语言如LEAN进行自动化定理证明方面。

论文的关键思路是通过专家迭代（expert iteration）的方法，让LLMs在解决数学问题的过程中不断自我训练和优化。此外，引入了一个批评模型（critic model）来选择相对简单的问题，从而引导策略模型（policy models）更有效地搜索证明路径。这种方法在现有研究基础上，通过大规模数据集和自训练机制，显著提高了模型的证明能力。

论文在多个基准测试中取得了显著的性能提升，特别是在MiniF2F、Lean-Workbook-Plus、ProofNet和Putnam等基准上。具体来说，模型在MiniF2F-test上的通过率为65.9%，在Lean-Workbook-Plus上能够证明或证伪17.0%的问题，而之前这一比例仅为9.5%。此外，作者开源了模型和搜索到的证明，提供了丰富的资源供社区进一步研究和改进。

近期在数学定理证明领域，有几项相关研究值得关注。例如，'Formal Mathematics Statement Curriculum Learning' (Wang et al., 2021) 探索了通过课程学习方法来提高模型的证明能力；'Learning to Prove Theorems via Interacting with Proof Assistants' (Lample and Charton, 2019) 提出了与证明助手交互的学习方法；'Neural Proof Nets' (Allamanis et al., 2017) 则研究了神经网络在形式化证明中的应用。