arXiv:2502.07640v3 宣传类型: replace-cross 摘要：我们介绍了一种开源语言模型Goedel-Prover，截至2025年4月5日，在数学问题自动形式证明方面达到了最先进的性能。该领域的一个关键挑战是正式化数学陈述和证明的稀缺性，我们通过以下方法解决了这一问题。首先，我们训练LLM将Numina数据集中的自然语言数学问题转换为等效的Lean 4形式声明。这一过程创建了包含164万条形式声明的Goedel-Pset-v1数据集。接下来，我们通过训练一系列证明器开发了一个大型形式证明数据集。每个新的证明器可以证明之前无法证明的许多陈述，这些新的证明被添加到下一个证明器的训练集中。最后，我们获得了包含Goedel-Pset-v1中超过80万条陈述证明的Goedel-Pset-v1-solved数据集。基于Goedel-Pset-v1-solved进行监督微调（SFT）的DeepSeek-Prover-V1.5-Base得到了Goedel-Prover-SFT，该模型在miniF2F上的成功率为57.6%（Pass@32），超过了之前领导者DeepSeek-Prover-V1.5-RL（使用SFT + RL训练的专有数据集）7.6%。在PutnamBench上，Goedel-Prover-SFT成功解决了7个问题（Pass@512），在排行榜上排名第一。我们详细讨论了我们的训练方法，强调了对Goedel-Prover强有力表现起关键作用的设计选择。进一步的RL训练（包括DPO）将Goedel-Prover-SFT在miniF2F上的成功率提高到超过60%（Pass@32）。 我们还提供了关于我们训练方法和设计选择的详细讨论，以助力未来的研究。我们还完全开源了我们的代码、模型和数据集。此外，我们还开源了在Lean Workbook中的29,700个问题的形式证明，几乎是之前证明器解决的15,700个问题的两倍。