arXiv:2502.07640v1 声称类型: cross 摘要: 我们介绍了一种开源的大语言模型 (LLM)，名为 Goedel-Prover，在数学问题的自动化形式证明生成方面达到了目前的最高水平 (SOTA)。这一领域的主要挑战在于形式化的数学命题和证明的稀缺性，我们通过以下方式应对这一挑战。我们训练声明形式化器，将 Numina 中的自然语言数学问题翻译成形式语言 (Lean 4)，从而创建了一个包含 164 万条形式化声明的数据集。大语言模型用于验证这些形式化声明是否准确地保留了原始自然语言问题的内容。然后，我们通过训练一系列证明器迭代构建了大量形式化证明的数据集。每个证明器成功证明了前一个证明器无法证明的许多声明，并将这些新证明添加到下一个证明器的训练集中。最终的证明器在全证明生成方面优于所有现有的开源模型。在 miniF2F 基准上，它以 57.6% 的成功率 (Pass@32) 超越了之前最好的开源模型 7.6%。在 PutnamBench 上，Goedel-Prover 成功解决了 7 个问题 (Pass@512)，在排行榜上排名第一。此外，它为 Lean Workbook 问题生成了 29,700 个形式化证明，几乎是早期工作生成的 15,700 个证明的两倍。