開源自動化的前沿模型定理證明：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）。

• 我們開源了代碼2、模型3???、數據集??，以及在 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-RL12 為每條陳述生成 16 個證明候選，然后通過 Lean 編譯器驗證這些證明。若至少有一個證明能成功解決該陳述，我們就為該陳述保留一個證明；當存在多個有效證明時，隨機采樣其中一個。這些收集到的證明被用于在 DeepSeek-Prover-V1.5-Base13 基礎上進行監督微調（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