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

該模型專為在數學驗證工具 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 的效果讓他印象深刻，“我甚至還嘗試了一道題，結果它完全搞定了。它真的太棒了。”海外的網友大呼：“人工智慧的更新速度比光速還要快！”“中國正在崛起。”

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

據介紹，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 透過兩階段訓練流程開發，建立了兩種互補的證明生成模式：

與 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 道問題則來自精心挑選的高中競賽和大學課程教材示例，為形式化數學問題提供了多樣且以教材為基礎的集合。此基準測試旨在對高中競賽問題和大學數學問題解答能力做出更為全面評估。