开源自动化的前沿模型定理证明：Goedel-Prover:

Goedel-Prover:开源自动化的前沿模型定理证明

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

https://arxiv.org/pdf/2502.07640

摘 要

我们提出 Goedel-Prover——一个开源语言模型，在数学问题的自动形式化证明生成任务中达到截至 2025 年 4 月 5 日的最先进水平。该领域的一个关键挑战是形式化数学陈述与证明的稀缺性，我们通过以下方法应对：
首先，我们训练 LLM 将 Numina 数据集中自然语言数学问题转换为 Lean 4 中的等效形式化陈述，由此构建包含 164 万条形式化陈述的数据集 Goedel-Pset-v1。
其次，我们通过一系列证明器迭代训练，构建大规模形式化证明数据集：每个新证明器都能证明前代无法解决的大量陈述，并将这些新证明加入下一轮训练集。最终得到 Goedel-Pset-v1-solved，包含超过 80 万条已证明陈述。
在 Goedel-Pset-v1-solved 上对 DeepSeek-Prover-V1.5-Base 进行监督微调（SFT，无强化学习），所得模型在 miniF2F 基准上达到 57.6% 的成功率（Pass@32），超越此前领先的 DeepSeek-Prover-V1.5（使用 SFT+RL 在私有数据上训练）7.6%。在 PutnamBench 上，Goedel-Prover-SFT 成功解决 7 道题（Pass@512），位居排行榜首位。进一步采用 RL 训练（包括 DPO）后，miniF2F 上的成功率提升至 60% 以上（Pass@32）。

为促进后续研究，我们详细讨论了训练方法与设计选择，并完全开源代码、模型和数据集。此外，我们开源了 Lean Workbook 中 29,700 道题目的形式化证明，几乎将此前证明器解决的 15,700 题翻倍。

1 引言

近期大型语言模型（LLMs）在推理任务中展现出卓越能力，尤其在解决数学问题方面（Guo 等，2025；Yang 等，2024a）。这些模型擅长通过自然语言进行推理，即所谓“非形式化推理”。然而，基于自然语言的推理难以被机器自动验证，削弱了其在实际应用中的可靠性，也阻碍了语言模型推理能力的进一步提升。

相比之下，形式化推理以机器可验证的格式进行，为验证与自动化开辟了新可能。特别是 Lean（De Moura 等，2015；Moura & Ullrich，2021）、Isabelle（Paulson，1994）和 Coq（Barras 等，1997）等证明助手提供了可机械验证的形式语言。因此，训练 LLM 使用这些形式语言书写证明具有重大意义。

在形式语言中训练 LLM 进行定理证明的一大挑战是形式化数学陈述与证明的极度稀缺。用形式语言书写定理证明要求极高，需深厚领域专业知识，因此现有公开形式化数据集规模有限。例如，Lean Workbook（含 Lean Workbook Plus）（Ying 等，2024a；Wu 等，2024）共包含 14 万条形式化陈述（指不含证明的 Lean 问题陈述），但其中仅有 1.57 万条配有形式化证明，由 InternLM2.5-StepProver 和 InternLM-Math-Plus 生成（Ying 等，2024a；Wu 等，2024；Ying 等，2024b）。此外，Open Bootstrapped Theorems 数据集（Wang 等，2024）包含 10.7 万条来自 Mathlib4（mathlib4，2023）的带证明陈述，但 Mathlib4 与通用解题基准（如广泛使用的 miniF2F（Zheng 等，2021））存在显著分布偏移（详见第 5 节）。

与形式语言数据的稀缺形成鲜明对比的是，非形式化数学问题与解答资源极为丰富。例如，Numina（Li 等，2024a）包含 86 万条高质量问答对，来源包括 MATH（Hendrycks 等，2021）、GSM8K（Cobbe 等，2021）、AMC（aop）、AIME（MAA，2024）、AoPS 论坛（aop）、中国 K-12 考试（Shao 等，2024）、国际奥赛及合成数据（Mitra 等，2024）。

我们首先训练 LLM 将该数据集中的问题陈述形式化为 Lean 代码。为增加形式化风格的多样性，我们训练了两个形式化器：一个在 Lean Workbook 的非形式化-形式化（I-F）陈述对上训练，另一个在由 Claude-sonnet-3.5（Anthropic，2024）标注的 I-F 对上训练。我们使用这两个形式化器生成形式化陈述，并利用 LLM 确保形式化内容忠实于原始非形式化陈述。最终获得 164 万条形式化陈述。

基于这一大规模形式化陈述数据集，我们采用专家迭代（expert iteration）（Polu 等，2022）训练证明器生成证明。值得注意的是，我们训练的模型仅基于陈述生成完整证明，生成过程中不与 Lean 编译器交互，此方法称为整证生成（whole-proof generation）（Jiang 等，2022；Wang 等，2024；Xin 等，2024a,b）。

在专家迭代初期，我们使用先前的 SOTA 模型 DeepSeek-Prover-V1.5-RL 为数据集中每条形式化陈述生成 16 个证明候选，并用 Lean 编译器验证其正确性。收集正确证明后，基于 DeepSeek-Prover-V1.5-Base 训练出 iter-1 证明器。在后续轮次中，我们使用 iter-k 证明器收集新证明并加入训练数据，再从 DeepSeek-Prover-V1.5-Base 出发进行新一轮监督微调，得到 iter-(k+1) 证明器。我们共进行了 8 轮迭代，从第一轮起即观察到持续性能提升。

我们证明，结合大规模形式化陈述的专家迭代可实现形式化证明生成的 SOTA 性能：

• 我们的模型 Goedel-Prover-SFT 在 miniF2F 上超越 DeepSeek-Prover-V1.5-RL（此前 SOTA）7.6%，Pass@32 达 57.6%（即对每道题生成 32 个证明，57.6% 的题目至少有一个被 Lean 验证为正确），而 DeepSeek-Prover-V1.5-RL 为 50.0%（见图 1 左）。在所有采样预算下（Pass@32、64 至 25600），Goedel-Prover-SFT 均稳定优于前者（见图 1 中）。

• 我们在 Lean Workbook 中累计解决了 29,700 道题，显著超过 InternLM2.5-StepProver 和 InternLM-Math-Plus 此前解决的 15,700 题（见图 1 右）。
• Goedel-Prover-SFT 在 PutnamBench 上通过 Pass@512 解决 7 道题，位列排行榜第一（表 2）。

• 我们开源了代码²、模型³⁴⁵⁶、数据集⁷⁸，以及在 Lean Workbook 中发现的新证明⁹，以促进未来研究。

为理解 Goedel-Prover 卓越性能背后的因素，我们深入讨论了训练方案，分析了训练数据规模扩展、自动形式化引入的多样性、数据集间的相关性以及替代数据合成策略的影响。此外，尽管我们的最终模型仅通过监督微调训练，我们也探索了在其基础上构建的直接偏好优化（DPO）和强化学习（RL）技术。Goedel-Prover-DPO 和 Goedel-Prover-RL 在 miniF2F 上 Pass@32 成功率超过 60%。但我们同时发现，DPO 和 RL 训练的模型倾向于过拟合“捷径”，且从推理时计算资源增加中获益较少。

2 相关工作

自动定理证明（Automated theorem proving, ATP）是符号人工智能中的一个长期研究问题（Robinson & Voronkov, 2001）。传统方法将定理表示为一阶逻辑，并使用决策过程（De Moura & Bjørner, 2008；Barbosa 等, 2022）和搜索策略（Kovács & Voronkov, 2013；Schulz 等, 2019）进行证明。后续研究通过用机器学习技术替代手工设计的启发式规则来增强证明搜索（Urban 等, 2011；Kaliszyk 等, 2018）。然而，基于一阶逻辑的方法难以扩展到复杂定理，且通常无法生成人类可读的证明。

近年来，基于学习的定理证明经历了显著变革。Polu 与 Sutskever（2020）提出了一种重要方法：利用大型语言模型（LLM）辅助在 Lean（De Moura 等, 2015；Moura & Ullrich, 2021）和 Isabelle（Paulson, 1994）等证明助手中进行定理证明。后续研究探索了多种方向，例如：检索有用引理（Irving 等, 2016；Mikuła 等, 2024；Yang 等, 2024b）、使用蒙特卡洛树搜索进行证明发现（Lample 等, 2022），以及利用 LLM 进行自然语言推理（Jiang 等, 2022；Lin 等, 2024）。值得注意的是，Polu 等（2023）首次将专家迭代（expert iteration）（Anthony 等, 2017）应用于定理证明。该方法交替进行两个阶段：(1) 尝试证明未解决的定理；(2) 将新发现的证明加入训练数据以增强证明器。专家迭代已在多个近期证明器中取得显著提升（Wu 等, 2024；Xin 等, 2024b），包括我们的 Goedel-Prover。

大多数自动定理证明器采用逐步式（stepwise）方式运行，即生成单个证明步骤，再通过证明搜索算法将其组合成完整证明。近期研究表明，整证生成（whole-proof generation）也是可行的（First 等, 2023；Xin 等, 2024a；Wang 等, 2024）。该方法避免了昂贵的搜索过程，从而降低延迟，并可能在测试阶段更高效地利用计算资源。虽然 Goedel-Prover 也采用整证生成，但我们的数据和方法原则上也可用于开发逐步式证明器。

自动形式化与合成数据生成。高质量形式化数学数据的匮乏是训练定理证明模型的重大瓶颈。尽管强化学习等技术可减少对人工编写证明的依赖（Google DeepMind, 2024），但仍需大量形式化定理陈述。一种有前景的方法是通过自动形式化（autoformalization）合成形式化陈述，即利用大型语言模型（LLM）将非形式化数学陈述翻译为形式化版本（Wu 等, 2022；2024；Xin 等, 2024a,b）。

DeepSeek-Prover（Xin 等, 2024a）和 InternLM2.5-StepProver（Wu 等, 2024）已成功采用此策略，将大量陈述形式化为 Lean 代码以用于专家迭代。我们采用了类似方法，但存在差异：Liu 等（2024）聚焦于形式化其内部数据集，而我们则专注于形式化 Numina 数据集（Li 等, 2024a）以及一个私有收集的数据集。此外，我们训练了两个形式化器以增强形式化风格的多样性，我们在第 4 节中证明了这种多样性具有实际益处。

3 方法

我们首先将非形式化陈述（以自然语言表达）翻译为形式化陈述（以 Lean 表示）。利用这些形式化陈述，我们通过迭代训练的方式训练我们的证明器：由证明器生成证明，并由 Lean 编译器验证其正确性。以下各小节将详细阐述每个步骤。

3.1 陈述形式化

我们首先训练陈述形式化器（statement formalizers），将 Numina 中的非形式化陈述翻译为形式化陈述，如图 2 所示。为增强形式化陈述的多样性，我们训练了两个模型来执行这一翻译任务：

• 形式化器 A（Formalizer A）：使用来自 Lean Workbook 的形式化-非形式化（F-I）陈述对训练该模型。
• 形式化器 B（Formalizer B）：我们使用 Claude-sonnet-3.5 对 Numina 中的 23 万条陈述进行形式化，从中筛选出 17 万条能成功通过 Lean 编译的陈述。这 17 万对 F-I 陈述被用于训练形式化器 B。

形式化器 A 和 B 均基于 Qwen2.5-Coder-32B 模型，采用监督微调（supervised fine-tuning）进行训练。在 8 块 H100 GPU 上，两个形式化器的训练均耗时不到 24 小时。

附录 A.1 展示了两个形式化器生成的形式化陈述示例。我们观察到，即使针对同一问题，不同形式化风格也会影响证明器的性能。

质量评估。我们采用两项测试来评估形式化陈述的质量：

第一，形式化陈述必须符合 Lean 语法，并能成功编译（将可能的证明部分替换为占位符 “:= by sorry”）。这一语法检查在文献中被称为编译正确性（Compiling Correctness, CC）（Ying 等，2024a）。

第二，形式化陈述必须准确捕捉原始非形式化问题，包含所有假设、条件和隐含定义。我们将这一测试称为忠实性与完整性（Faithfulness and Completeness, FC）测试。对于 FC 测试，我们使用 Qwen2.5-72B-Instruct 模型，具体细节见附录 A.2。

除了对 86 万条开源的 Numina 数据集（Li 等，2024a）进行形式化外，我们还形式化了由 Numina 团队收集并处理的、来自 Art of Problem Solving（AOPS）的 6.8 万条私有数学问题。

在总计 92.8 万条非形式化陈述中，76 万条同时获得了由形式化器 A 和 B 生成的两个有效形式化版本，12.3 万条仅有一个有效形式化版本。

在完成 Numina 和 AOPS 数据集的形式化后，我们进一步整合了来自 Lean Workbook（包括 Lean Workbook Plus）的 14 万条陈述。最终，我们共获得 178 万条形式化陈述。

3.2 专家迭代

在第 3.1 节获得大量形式化陈述后，我们采用专家迭代（expert iteration）方法训练证明器（Liu 等，2024；Wu 等，2024；Li 等，2024b），如图 3 所示。具体而言，我们首先使用 DeepSeek-Prover-V1.5-RL¹² 为每条陈述生成 16 个证明候选，然后通过 Lean 编译器验证这些证明。若至少有一个证明能成功解决该陈述，我们就为该陈述保留一个证明；当存在多个有效证明时，随机采样其中一个。这些收集到的证明被用于在 DeepSeek-Prover-V1.5-Base¹³ 基础上进行监督微调（SFT），从而得到 iter-1 证明器。

我们持续这一专家迭代过程：每次使用 iter-k 证明器为所有陈述生成解答，并累积收集正确的证明，用于训练下一轮的 iter-(k+1) 证明器（仍以 DeepSeek-Prover-V1.5-Base 为起点）。更多关于每轮迭代的细节见附录 B。

我们尝试了两种学习率（1×10⁻⁴ 和 5×10⁻⁵），并分别训练 1 或 2 个 epoch。为加速训练，我们采用 packing 技巧（Tunstall 等，2022），并使用较小的批大小（8）。在每次迭代中，使用 4 块 H100 GPU 训练 1 个 epoch 约需 12 小时。对 178 万条陈述进行 Pass@16 推理（即每条生成 16 个证明候选）耗时约 6 小时，使用 64 块 H100 GPU。此外，对这些证明进行验证需 10 小时，使用 8,000 个 CPU 核心。

4 结果

基准测试。遵循（Wang 等，2024；Xin 等，2024a；Wu 等，2024；Li 等，2024b）的工作，我们主要使用 miniF2F（Zheng 等，2021）作为核心评估基准。此外，我们还追踪模型在 Lean Workbook（Ying 等，2024a）中解决的问题数量，并在 ProofNet（Azerbayev 等，2023）和 PutnamBench（Tsoukalas 等，2024）上评估性能。同时，我们从形式化数据集中均匀采样一个子集，构建一个保留的评估数据集。以下是对各数据集的描述：

• miniF2F（Zheng 等，2021）：一个形式化定理证明基准，包含 488 道 Lean 问题陈述（244 验证集 + 244 测试集），题目来自高中练习题及高中竞赛（如 AIME、AMC 和国际数学奥林匹克 IMO）。原始版本基于 Lean 3，我们在分析中采用 Xin 等（2024a）提供的 Lean 4.9.0 版本。
• ProofNet（Azerbayev 等，2023）：一个面向本科数学的形式化定理证明基准，包含 371 道 Lean 问题（185 验证 + 186 测试），题目主要源自本科纯数学教材，涵盖实分析、复分析、线性代数、抽象代数和拓扑等主题。原始版本为 Lean 3，我们使用 Xin 等（2024a）提供的 Lean 4.9.0 版本。
• Lean Workbook（Ying 等，2024a）：一个大规模 Lean 4 问题集，由自然语言数学问题（主要来自 AoPS 论坛）形式化而来，共包含 14 万条 Lean 4 陈述。我们在专家迭代过程中持续监控模型在该数据集上解决的问题。值得注意的是，Lean Workbook 被包含在我们的训练数据中，这与 DeepSeek-Prover-V1.5（Xin 等，2024a）和 InternLM2.5-StepProver（Wu 等，2024）的做法一致。
• PutnamBench（Tsoukalas 等，2024）：一个基于 William Lowell Putnam 数学竞赛（1962–2023 年）的形式化定理证明基准，包含 644 条 Lean 4 陈述，覆盖代数、分析、数论、几何、组合、概率与集合论。
• NuminaTest：我们从形式化的 Numina 数据集中随机采样 250 条陈述，作为保留测试集，称为 NuminaTest。

主要结果。miniF2F 上的性能见表 1。我们的 Goedel-Prover-SFT 在 Pass@32 下达到 57.6% 的成功率，超越此前开源 SOTA 模型 DeepSeek-Prover-V1.5-RL 7.6%。我们观察到，Goedel-Prover-SFT 的 Pass@32 甚至优于 DeepSeek-Prover-V1.5-RL 的 Pass@3200（高出 2.7%）。当两者均以 Pass@3200 评估时，我们的模型达到 62.7%，比 DeepSeek-Prover-V1.5-RL 的 54.9% 高出 7.8%。

图 1 展示了 Goedel-Prover-SFT、DeepSeek-Prover-V1.5-RL 和 DeepSeek-Prover-V1.5-SFT 的推理时间扩展曲线。在所有推理计算预算下，Goedel-Prover-SFT 均显著优于另两个模型。图 4 展示了每轮迭代中模型性能的变化，整体呈现出各轮次间相对稳定的持续提升。

PutnamBench 性能。Goedel-Prover-SFT 在 PutnamBench 的 644 道题中解决了 7 道（Pass@512），在排行榜上位列第一。此前的 SOTA 方法 ABEL（Gloeckle 等）同样解决 7 题，但使用了略高的推理预算（Pass@596）；InternLM2.5-StepProver（Wu 等，2024）解决 6 题（Pass@2×32×600）。性能汇总见表 2。

在 Lean Workbook 中发现的证明。Lean Workbook（含 Lean Workbook Plus）（Ying 等，2024a；Wu 等，2024）形式化了 14 万道高质量问题，源自 AoPS 和 Compfiles 数据。目前，仅 15,700 条陈述的证明由 InternLM2.5-StepProver（Wu 等，2024）和 InternLM-Math-Plus（Ying 等，2024b）找到并开源。相比之下，我们的模型在 Lean Workbook 中累计解决了 29,700 道题，数量显著更多（见图 1 右）。我们已将所有由模型发现的证明完全开源，以惠及研究社区。

5 剖析培训配方

扩大形式化陈述数量可提升模型性能。图 5 展示了在不同规模形式化陈述集上训练的证明器（在 miniF2F、ProofNet 和 NuminaTest 上的平均性能）的表现。每条陈述对应的证明均由 Goedel-Prover-SFT 生成。我们观察到，随着陈述集规模的增加，模型性能持续提升，这凸显了规模化训练对构建高效证明器的重要性。

增加形式化风格的多样性具有益处。表 3 展示了在不同形式化风格的陈述上训练的 iter-8 证明器的性能（其证明由 iter-7 证明器生成）。我们发现，在混合风格（即同时使用形式化器 A 和 B 生成的陈述）的模型，优于仅使用单一形式化风格训练的模型。这一结果表明，接触多样化的形式化模式有助于提升模型的泛化能力和推理能力。

数据集间的相关性。我们在不同训练轮次和超参数设置下评估模型性能，并计算多个数据集间性能的相关性（见图 6）。我们观察到，模型在 ProofNet 上的性能与在 miniF2F、Lean Workbook 和 NuminaTest 上的性能呈负相关。此外，我们研究了在训练数据中加入 Mathlib4 的影响。如表 4 所示，引入 Mathlib4 提升了 ProofNet 上的性能，却导致 miniF2F 上性能下降。这些发现表明，ProofNet/Mathlib4 与其他数据集之间存在分布偏移。具体而言，Mathlib4 和 ProofNet 更侧重于数学概念的操作，而 miniF2F、Lean Workbook 和 NuminaTest 等数据集则包含更多奥赛风格问题，强调复杂推理而非形式化数学内容。附录 C 提供了示例说明。尽管存在这种分布偏移，我们仍从第六轮迭代起将 Mathlib4 纳入训练集，遵循 DeepSeek-Prover-V1.5-RL（Xin 等，2024b）和 TheoremLamma（Wang 等，2024）的做法，旨在提升模型在更广泛数学领域的通用能力。更多训练细节见附录 B。

替代的数据合成方法。除了自动形式化陈述并由证明器提供证明外，我们还探索了其他构建训练数据集的策略，重点是通过分治策略（divide-and-conquer）解决难题。受 Jiang 等（2022）启发，我们实现了以下流程：(1) 使用 OpenAI 的 o1-preview 模型为形式化陈述生成证明；(2) 提取该证明的高层“草图”；(3) 利用 DeepSeek-Prover-V1.5-RL 证明草图所提供的子目标。若所有子目标均被成功证明，则获得原问题的有效证明。附录 D 提供了实现细节。然而，该流程在实践中效果不佳：在 miniF2F 验证集（244 题）上仅成功解决 76 题，远少于 DeepSeek-Prover-V1.5-RL 单独解决的 158 题。而且，在这 76 题中，仅有 1 题是 DeepSeek-Prover-V1.5-RL 未能解决的，表明该流程带来的边际收益极为有限。

探索 DPO 与 RL 训练。我们在 Goedel-Prover-SFT 基础上进一步探索了 DPO 和 RL 训练。我们实现了离线的直接偏好优化（DPO）（Rafailov 等，2023）和在线的组相对策略优化（GRPO）（Shao 等，2024），实现细节见附录 E。表 5 显示，尽管 DPO 和 GRPO 提升了模型的 Pass@32 性能，但平均证明长度显著增加，且某些模式的出现频率急剧上升。这一现象表明模型正在过拟合某些语法模式或“捷径”，类似于“奖励黑客”（reward hacking）（Chen 等，2024）。例如，Lean 中的 try 战术会尝试执行一个战术，无论成功与否都继续执行。虽然通常无害，偶尔有用，但过度使用会导致无效证明并大幅增加验证成本。经 RL 训练的模型开始过度偏好此类模式，最终损害其推理与泛化能力。

进一步实验表明，在 DPO 训练中加入长度惩罚有助于缓解这种过拟合。但我们观察到，与 SFT 模型相比，经 GRPO 或带长度惩罚的 DPO 微调的模型在增加推理时计算资源时收益显著更小。如表 5 所示，这些模型在 Pass@32 上比 Goedel-Prover-SFT 提升约 3%，但当增加推理预算（例如 Pass@3200）时，这一优势迅速减弱。这表明 RL 训练可能降低了输出多样性，导致推理时扩展效率降低。

6 讨论

在附录F中提供了对Goedel-Prover-SFT生成证明的特征的进一步讨论以及潜在的改进领域。

原文链接：https://arxiv.org/pdf/2502.07640