Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

我们推出了Goedel-Prover，这是一个开源的大规模语言模型（LLM），在数学问题的自动化形式证明生成方面达到了最先进的（SOTA）水平。该领域的关键挑战在于形式化数学陈述和证明的稀缺性，我们通过以下方式应对这一挑战。我们训练了陈述形式化器，将Numina中的自然语言数学问题翻译成形式语言（Lean 4），创建了一个包含164万条形式化陈述的数据集。使用大规模语言模型（LLM）来确保这些形式化陈述准确地保留了原始自然语言问题的内容。然后，我们通过训练一系列证明者迭代构建一个大型的形式证明数据集。每个新的证明者能够成功证明之前无法证明的许多陈述，并且这些新证明被添加到下一个证明者的训练集中。尽管仅使用监督微调，我们的最终证明者显著超越了之前的最佳开源模型DeepSeek-Prover-V1.5，后者采用了强化学习方法。在miniF2F基准测试中，我们的模型实现了57.6%的成功率（Pass@32），比DeepSeek-Prover-V1.5高出7.6个百分点。在PutnamBench上，Goedel-Prover成功解决了7个问题（Pass@512），在排行榜上位列第一。此外，它为Lean Workbook问题生成了29.7万个形式证明，几乎是先前工作生成的15.7万个的两倍。

论文试图解决自动化形式化数学证明生成中的关键挑战，即形式化数学陈述和证明的稀缺性。这是一个长期存在的问题，但Goedel-Prover通过大规模的数据生成和迭代训练提供了一个新的解决方案。

关键思路在于通过训练语句形式化器将自然语言数学问题转化为形式语言（Lean 4），并创建一个包含164万个形式化陈述的大规模数据集。然后，通过迭代训练一系列证明者来逐步扩展形式证明的数据集。每个新的证明者都能证明前一代无法证明的命题，并将其添加到下一个证明者的训练集中。这种方法在没有使用强化学习的情况下显著提升了性能。

该研究在miniF2F基准上达到了57.6%的成功率，比之前最好的开源模型DeepSeek-Prover-V1.5高出7.6%。在PutnamBench上，它解决了7个问题，排名第一。此外，它为Lean Workbook问题生成了29.7K个形式证明，几乎是之前工作的两倍。该研究提供了开源代码，使得其他研究人员可以复现和进一步改进这些结果。

最近在这个领域中，相关的研究包括：1. DeepSeek-Prover系列，它使用强化学习进行证明生成；2. Lean社区的多种工具和库，用于形式化数学；3. 其他形式化证明助手如Coq和Isabelle的发展。一些相关研究的论文标题包括《Formalizing mathematics in Lean》、《Reinforcement Learning for Theorem Proving》等。