整理｜華衛、核子可樂

昨晚，DeepSeek 在 Hugging Face 上開源了一個新模型。這次他們發布的，是名為 DeepSeek-Prover-V2 的數學推理模型，提供 7B 和 671B 兩種參數規模。

開源項目鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main

該模型專為在數學驗證工具 Lean 4 中進行形式化定理證明而設計。Lean 是一種函數式編程語言，可以作為定理證明時的輔助證明工具，在數學界應用甚廣，目前已發展到第四代，即 Lean 4。此前，陶哲軒曾借助 Lean 4 成功完成 PFR 猜想的證明。

在多個標準基準測試中，DeepSeek-Prover-V2-671B 都取得了神經定理證明領域的最先進性能水平。并且，面對從著名的 AIME 競賽（2024 - 2025 年）中挑選的 15 個問題，該模型成功解出了其中的 6 個。相比之下，DeepSeek-V3 通過多數投票解決了其中 8 個問題。DeepSeek 團隊表示，這一對比突出表明大語言模型中形式化和非形式化數學推理之間的差距正在大幅縮小。

并且，相比 Numina 和 Kimi 團隊前段時間聯合推出的數學定理證明模型 Kimina-Prover ，DeepSeek-Prover-V2-7B 在 MiniF2F 測試中的通過率更高。在 pass@8192 的采樣預算下，Kimina-Prover 的通過率為 80.7%，而 DeepSeek-Prover-V2-7B 達到了 82.0%。

該模型一發布，就有數學奧賽學生迫不及待地去試用了。據稱，DeepSeek-Prover-V2 的效果讓他印象深刻，“我甚至還嘗試了一道題，結果它完全搞定了。它真的太棒了?！焙Ｍ獾木W友大呼：“人工智能的更新速度比光速還要快！”“中國正在崛起?！?/p>

還有網友直接給出這樣的高評價：“DeepSeek-Prover-V2-671B 旨在實現所有數學運算的自動化。”“DeepSeek 這篇在 reasoning 的追求上，到了一個讓普通老百姓不能理解的程度?！?/p>

據介紹，DeepSeek-Prover-V2 通過強化學習推進子目標分解的形式數學推理，其初始化數據通過由 DeepSeek-V3 驅動的遞歸定理證明流程收集得到。冷啟動訓練過程首先會促使 DeepSeek-V3 將復雜問題分解為一系列子目標，已解決子目標的證明被合成為一個思維鏈過程，并結合 DeepSeek-V3 的逐步推理，為強化學習創建初始冷啟動條件，這一過程能夠將非正式和形式化的數學推理整合到一個統一的模型中。

從隨后放出的技術報告里，我們看到了有關 DeepSeek-Prover-V2 的完整訓練方案及更多技術細節。

兩步走的訓練方案

將復雜定理的證明分解為一系列較小的引理，作為證明的墊腳石，這是人類數學家常用的有效策略。DeepSeek-Prover-V2 本質上就是一種用于子目標分解的推理模型，利用一系列合成冷啟動數據和大規模強化學習來提高其性能。

遞歸證明搜索合成形式化推理數據

為構建冷啟動數據集，DeepSeek 團隊開發了一個簡單而有效的遞歸定理證明流程，利用 DeepSeek-V3 作為子目標分解和形式化的統一工具，最終的思維鏈以一個由一系列 have 語句組成的 Lean 定理結束，每個 have 語句都以 sorry 占位符結尾，表示有待解決的子目標。

過程中，DeepSeek-V3 首先用自然語言分析數學問題，然后將證明分解為更小的步驟，并將每個步驟轉換為相應的 Lean 形式化陳述；由于通用模型在生成完整的 Lean 證明方面存在困難，僅指示 DeepSeek-V3 生成省略細節的高級證明草圖。這種方法模仿了人類構建證明的方式，即將復雜定理逐步簡化為一系列更易于處理的引理。

利用 DeepSeek-V3 生成的子目標，DeepSeek-Prover-V2 采用遞歸求解策略來系統地解決每個中間證明步驟：從 have 語句中提取子目標表達式，用它們替換給定問題中的原始目標，然后將前面的子目標作為前提條件。這種構建方式使得后續子目標可以利用前面步驟的中間結果來解決，從而促進更局部化的依賴結構，并有助于開發更簡單的引理。

接下來，為了減少廣泛證明搜索的計算開銷，DeepSeek 團隊使用一個專門優化用于處理分解后引理的較小的 70 億參數證明模型，可以在所有分解步驟都成功解決后，自動推導出原始定理的完整證明。

證明模型的訓練需要大量的形式語言問題集，這些問題集通常通過對現有的自然語言數學語料庫進行形式化得到。為此，該團隊在 DeepSeek-Prover-V2 中引入了一個課程學習框架，利用分解后的子目標生成推測性定理，逐步增加訓練任務的難度，以更好地指導模型的學習過程。一旦具有挑戰性的問題的分解步驟得到解決，就將完整的逐步形式化證明與 DeepSeek-V3 相應的思維鏈配對，創建冷啟動推理數據。

上述算法框架分兩個階段運行，利用兩個互補的模型：DeepSeek-V3 用于引理分解，70 億參數證明模型用于完成相應的形式化證明細節。這個流程提供了一種自然且可擴展的機制，將大語言模型的高級推理與精確的形式驗證相結合，合成形式化推理數據。通過這種方式，DeepSeek 團隊在單個模型中統一了非形式化數學推理和證明形式化的能力。

執行強化學習階段

在冷啟動的基礎上，DeepSeek 團隊應用后續的強化學習階段，進一步加強非形式化數學推理與形式化證明構建之間的聯系。實驗表明，從任務分解中的非形式化推理冷啟動開始的強化學習，顯著提高了模型在形式化定理證明方面的能力。

據介紹，他們整理了一組 70 億參數證明模型無法端到端解決，但所有分解后的子目標都已成功解決的具有挑戰性問題子集。通過組合所有子目標的證明，為原始問題構建了一個完整的形式化證明，然后將該證明附加到 DeepSeek-V3 的思路鏈中。這一思路鏈概述了相應的引理分解，從而將非形式化推理與后續形式化過程緊密結合。

在對證明模型進行合成冷啟動數據的微調后，該團隊開始執行強化學習階段，以進一步提高其將非形式化推理與形式化證明構建聯系起來的能力。遵循推理模型的標準訓練目標，它們使用二元正確或錯誤反饋作為主要的獎勵監督形式。

由于在訓練過程中觀察到生成的證明結構經常與思維鏈指導提供的引理分解不同，他們在訓練的早期步驟中納入了一致性獎勵，對結構不一致進行懲罰，明確要求最終證明中包含所有分解的 have 結構引理。在實踐中，強制執行這種一致性提高了證明的準確性，特別是在需要多步推理的復雜定理上。

提供兩種推理證明模式

簡單來說，DeepSeek-Prover-V2 通過兩階段訓練流程開發，建立了兩種互補的證明生成模式：

1. 高效非思維鏈（non-CoT）模式：此模式針對快速生成形式化 Lean 證明代碼進行了優化，專注于在不顯示中間推理步驟的情況下生成簡潔的證明。

2. 高精度思維鏈（CoT）模式：此模式在構建最終形式化證明之前，系統地闡述中間推理步驟，強調透明度和邏輯進展。

與 DeepSeek-Prover-V1.5 一致，DeepSeek-Prover-V2 的兩種生成模式由兩個不同的引導提示控制。在第一階段，DeepSeek 團隊在課程學習框架內使用專家迭代范式來訓練非思維鏈證明模型，同時通過基于子目標的遞歸證明為難題合成證明。選擇非思維鏈生成模式是為了加速迭代訓練和數據收集過程，因為它提供了明顯更快的推理和驗證周期。

在此基礎上，第二階段利用了通過將 DeepSeek-V3 復雜的數學推理模式與合成形式證明相結合而生成的冷啟動鏈式思維鏈數據。CoT 模式通過進一步的強化學習階段得到增強，遵循推理模型常用的標準訓練流程。

據介紹，該團隊使用恒定的學習率 5e-6，在 16384 個 token 的上下文窗口內，對 DeepSeek-V3-Base-671B 進行監督微調。訓練語料庫由兩個互補來源組成：（1）通過專家迭代收集的非思維鏈數據，這些數據生成的 Lean 代碼沒有中間推理步驟；（2）冷啟動思維鏈數據，這些數據將 DeepSeek-V3 先進的數學推理過程提煉為結構化的證明路徑。非思維鏈組件強調 Lean 定理證明生態系統中的形式驗證技能，而思維鏈示例則明確模擬了將數學直覺轉化為形式化證明結構的認知過程。

DeepSeek-Prover-V2 所采用的強化學習算法是組相對策略優化（GRPO），該算法在推理任務中已證明具有卓越的有效性和效率。與近端策略優化（PPO）不同，GRPO 通過為每個定理提示采樣一組候選證明，并根據它們的相對獎勵優化策略，消除了對單獨批評模型的需求。訓練使用二元獎勵，即每個生成的 Lean 證明如果被驗證正確則獲得 1 的獎勵，否則為 0。

為確保有效學習，DeepSeek 團隊精心挑選了訓練提示，僅包括那些具有足夠挑戰性但可由監督微調模型解決的問題。在每次迭代中，DeepSeek-Prover-V2 會采樣 256 個不同的問題，為每個定理生成 32 個候選證明，最大序列長度為 32768 個 token。

此外，該團隊將 DeepSeek-Prover-V1.5-Base-7B 的最大上下文長度從 4096 個 token 擴展到 32768 個，并使用在 DeepSeek-Prover-V2-671B 強化學習階段收集的滾動數據對這個擴展上下文模型進行微調。除了 CoT 模式，他們還納入了在專家迭代期間收集的非思維鏈證明數據，以實現一種成本效益高的證明選項，使用小型模型生成簡潔的形式化輸出。并且，7B 模型亦執行與 671B 模型相同的強化學習階段。

高中、本科、奧賽題“一網打盡”

在最后的性能評測環節，DeepSeek 團隊用各種形式定理證明的基準數據集對 DeepSeek-Prover-V2 進行了系統的評估，涵蓋高中競賽題目和本科階段數學知識。

結果表明，盡管訓練數據主要來自高中水平的數學問題，該模型仍能很好地泛化到更高級的大學水平問題，展現出其強大的形式化推理能力。

在 MiniF2F 測試中，DeepSeek-Prover-V2-671B 在使用 CoT 生成策略的情況下，僅需 32 次采樣即可達到前所未有的 82.4% 準確率，刷新了該基準測試的最新記錄，到 8192 次采樣時提高到 88.9%。值得注意的是，參數更少但效率更高的 DeepSeek-Prover-V2-7B 模型同樣表現出色，超越了所有現有的開源定理證明模型。

據了解，MiniF2F 基準測試包含 488 道形式數學問題陳述，這些問題來源于 AIME、AMC 和 IMO 等競賽以及 MATH 數據集，涵蓋代數、數論和歸納法等領域。

令人印象深刻的是，其子目標引導課程學習框架，結合通用模型 DeepSeek-V3 和輕量級專業 7B 定理證明器，DeepSeek-Prover-V2 在 miniF2F-valid 上取得了 90.2% 的成功率，幾乎與體量更大的 DeepSeek-Prover-V2-671B 持平。這一發現表明，最先進的通用 LLM 不僅可以擴展自然語言理解能力，還能有效支持復雜的形式推理任務。通過戰略性子目標分解，模型能夠將復雜問題拆解為一系列可處理的步驟，從而在非形式推理和形式證明之間建立起有效的橋梁。

在 ProofNet 和 PutnamBench 基準測試上，DeepSeek-Prover-V2-671B 也展示了超強的解題推理能力，且 CoT 模式下效果更優。這些結果進一步強調，CoT 推理方法在處理有挑戰性的大學水平數學問題方面更具有效性。

ProofNet 包含 371 道用 Lean 3 編寫的數學問題，這些問題來源于多部流行的本科純數學教材，涵蓋實分析、復分析、線性代數、抽象代數和拓撲學等領域。PutnamBench 是一項持續更新的基準測試，包含自 1962 年至 2023 年的普特南數學競賽題目。該競賽面向美國和加拿大的本科生，涵蓋分析、線性代數、抽象代數、組合數學、概率和集合論等多個領域。

一個意外發現是，DeepSeek-Prover-V2-7B 在非 CoT 生成模式下對 PutnamBench 數據集的表現更為出色，成功解決了 DeepSeek-Prover-V2-671B 無法解決的 13 道問題。通過對模型輸出的進一步分析，DeepSeek 團隊發現，其推理方法中存在一種顯著的模式：7B 模型經常使用 Cardinal.toNat 和 Cardinal.natCast_inj 來處理涉及有限基數的問題，這些手段似乎使模型能夠有效地解決需要精細操作基數值的一類問題，

而這樣的思路在 671B 版本的輸出中明顯缺失。

除了標準基準測試，DeepSeek 團隊還引入了在 ProverBench，這是一個包含 325 個形式化問題的集合，其中 15 道問題是基于近期 AIME 競賽中的數論和代數問題形式化而成，反映出真實的高中競賽水平挑戰，剩余的 310 道問題則來自精心挑選的高中競賽和大學課程教材示例，為形式化數學問題提供了多樣且以教材為基礎的集合。此基準測試旨在對高中競賽問題和大學數學問題解答能力做出更為全面評估。

https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf

聲明：本文為 InfoQ 翻譯整理，不代表平臺觀點，未經許可禁止轉載。

AICon 2025 強勢來襲，5 月上海站、6 月北京站，雙城聯動，全覽 AI 技術前沿和行業落地。大會聚焦技術與應用深度融合，匯聚 AI Agent、多模態、場景應用、大模型架構創新、智能數據基建、AI 產品設計和出海策略等話題。即刻掃碼購票，一同探索 AI 應用邊界！