arXiv:2502.07640v2 宣告类型: replace-cross 摘要: 我们引入了Goedel-Prover，这是一个开源的大语言模型（LLM），在数学问题的自动化形式证明生成方面达到了最先进的（SOTA）性能。该领域面临的 key challenge 是形式化数学命题和证明的稀缺，我们通过以下方式应对这一挑战。我们训练声明形式化器，将 Numina 中的自然语言数学问题翻译成形式语言（Lean 4），创建了一个包含 164 万形式化声明的数据集。大语言模型用于检查这些形式化声明是否准确地保留了原始自然语言问题的内容。然后，通过训练一系列证明器，逐步构建一个大型形式化证明的数据集。每个证明器都成功证明了许多之前证明器无法证明的命题，这些新证明被添加到下一个证明器的训练集中。尽管仅使用监督微调，我们最终的证明器显著优于之前的最佳开源模型 DeepSeek-Prover-V1.5，该模型使用强化学习。在 miniF2F 验证基准上，我们的模型取得了 57.6%（Pass@32）的成功率，超越了 DeepSeek-Prover-V1.5 的 7.6%。在 PutnamBench 上，Goedel-Prover 成功解决了 7 个问题（Pass@512），在排行榜上排名第一。此外，它为 Lean Workbook 问题生成了 29,700 个形式化证明，几乎是此前工作产量的两倍。