DeepSeek再破谷歌OpenAI壟斷：開源IMO數學金牌大模型

henry 發自 凹非寺
量子位 | 公眾號

AI界掌管開源的神——DeepSeek回來了！

剛剛，DeepSeek開源了全新的數學模型DeepSeekMath-V2，專注于可自驗證的數學推理。

DeepSeekMath-V2不僅在IMO 2025和CMO 2024中取得金牌級分數，而且還在Putnam 2024中，得分118/120，超過了人類最高分90。

與此同時，DeepSeekMath-V2在所有CNML級別問題類別（代數、幾何、數論、組合學、不等式）上均優于GPT-5-Thinking-High和Gemini 2.5-Pro。

不僅性能無敵，網友表示這還是第一個開源的IMO金牌模型。

這下，谷歌和OpenAI要坐不住了！

特別是OpenAI，本來就打算放出IMO金牌模型來應對谷歌Gemini 3 Pro的沖擊，現在被DeepSeek搶先一步。

（鯨魚回來了！）

值得一提是，這篇論文的一作邵智宏也是之前DeepSeekMath 7B的一作，在那篇論文中，他們提出了著名的GRPO

最強開源IMO金牌模型

總的來說，DeepSeekMath-V2是一個旨在實現自驗證數學推理（Self-verification）的大型語言模型（685B）。

它的核心在于開發和利用強大的證明驗證能力來指導和優化證明生成，從而克服傳統上依賴最終答案作為獎勵的強化學習（RL）方法的局限性。

傳統用于數學推理的強化學習（RL）方法存在根本性限制：

• 最終答案獎勵的不可靠性：將LLM獎勵基于最終答案的正確性，并不能保證推理過程的正確性或邏輯的嚴謹性，模型可能通過錯誤的邏輯得出正確答案 。
• 對定理證明任務的局限性：許多數學任務（如定理證明）不要求數值答案，而是需要嚴格的步驟推導和邏輯嚴謹性，使得基于最終答案的獎勵機制不適用。
• 缺乏內部驗證能力：經過傳統方法訓練的LLMs缺乏驗證自身證明有效性的能力，經常表現出高假陽性率（即認為錯誤的證明是有效的)。

DeepSeekMath-V2采用迭代的強化學習循環，交替優化證明驗證器和證明生成器，以實現可自驗證的數學推理。

證明驗證

訓練驗證器

研究首先訓練一個準確且忠實的LLM-based驗證器，使其能夠根據人類專家的標準識別證明中的問題并評分。

具體來說，驗證器針對給定的數學問題與證明，輸出一個證明分析，該分析首先總結識別出的問題（如果有），然后基于三個級別分配一個分數：

1：完全正確、嚴謹且邏輯清晰的證明。0.5：總體邏輯合理，但有微小錯誤或細節遺漏的證明。0：包含致命邏輯錯誤或關鍵漏洞的根本性錯誤的證明。

驗證器的訓練分為數據構建（冷啟動）和模型強化學習目標兩個關鍵階段。

在數據構建階段，研究首先從AoPS競賽中收集了1.75萬個要求證明的奧賽級別數學問題。

隨后，利用現有模型（DeepSeek-V3.2-Exp-Thinking）生成大量的候選證明，并通過多輪迭代來提升證明的嚴謹性，最終請數學專家人工對這些證明進行評分，分數分為1、0.5和0三個級別，從而創建了初始的RL驗證數據集。

進入強化學習目標階段，研究使用上述數據集對基礎模型（DeepSeek-V3.2-Exp-SFT）進行訓練，使其能夠輸出證明分析總結和最終分數。

獎勵函數一方面通過格式獎勵強制模型輸出格式包含問題總結和分數，另一方面通過分數獎勵激勵模型預測的分數與專家標注的分數高度一致，從而使驗證器具備模仿人類專家評估嚴謹性的能力。

引入元驗證 (Meta-Verification)

為解決初步訓練的驗證器可能因幻覺（hallucinating）不存在的問題而獲得正確低分，從而損害其對錯誤識別的忠實性（faithfulness）的問題，研究團隊引入了元驗證（Meta-Verification）機制。

元驗證作為一個二級評估過程，旨在審查驗證器生成的證明分析（Proof Analysis），評估其中識別出的問題是否真實存在，以及這些問題是否在邏輯上合理地支持了其預測的證明分數。

為了訓練元驗證器，研究首先讓數學專家根據專門的元驗證標準對驗證器輸出的分析質量進行評分，創建了元驗證數據集。

隨后，研究訓練了一個專門的元驗證器，該元驗證器生成對驗證分析本身的問題總結，并分配一個質量分數，以衡量原驗證器分析的準確性和合理性。

元驗證器的強化學習目標結構與驗證器訓練類似，同樣包含格式獎勵和分數獎勵。

接下來是增強驗證器訓練，研究利用訓練好的元驗證器，將元驗證的質量分數集成到驗證器的獎勵函數中，以增強驗證器的忠實性。

最終，使用原驗證數據集和元驗證數據集共同訓練增強后的驗證器，使該模型能夠同時執行證明驗證和元驗證兩項任務。

在原驗證數據集的一個驗證子集上，經驗證器評估的證明分析的平均質量分數從 0.85 提升到了0.96，同時保持了證明分數預測的準確性不變，有力證明了元驗證機制能有效提高驗證器識別問題的忠實度。

證明生成

接下來，研究用訓練好的驗證器作為獎勵模型來訓練證明生成器，并進一步通過“自驗證”機制，讓生成器學會嚴格地自我審查和修正，從而提高證明質量。

具體來說，研究訓練生成器以最大化驗證器賦給其生成的證明的分數。

在訓練中，生成器被要求在生成證明后，緊跟著進行自我分析。獎勵函數激勵準確的自我評估和正確性。

最終獎勵是對證明質量和自我評估質量的加權組合。

由此，自我評估獎勵不僅獎勵自評分的準確性，還獎勵自我分析的忠實性。

這種獎勵結構激勵生成器：忠實地承認錯誤（而非盲目自信）。獲得高獎勵的最佳策略是在最終輸出前，積極識別并解決自身證明中存在的問題，從而實現自我迭代完善。

證明驗證與生成之間的協同作用

接下來，研究利用驗證器和生成器的協同作用，通過規模化的計算和元驗證機制，建立了一個完全自動化的數據標注流程，從而持續提升驗證器的能力，并最終取代耗時的人工標注。

然而，隨著問題難度增加，人工標注耗時且效率低下。由此研究提出了一套自動化標注的方法：

首先，通過生成n個獨立的驗證分析，提高在有缺陷證明中捕獲真實問題的概率。接下來，利用元驗證器生成m個評估，對報告問題的分析進行有效性確認，確保識別出的問題是真實的（元驗證比從零識別問題更高效）。

具體的標注流程如下：

• 分數判定：檢查所有分析中分配的最低分數。只有當至少有k個分析被元驗證確認為有效時，該最低分才被賦給該證明；否則標記為1分（無合法缺陷）。
• 取代人工： 最終，這種完全自動化的流程在后續訓練迭代中徹底取代了人工標注，并且質量檢查證實其標注結果與專家判斷高度一致。

由此，上述流程在最終的訓練迭代中徹底取代了耗時的人力標注，實現了驗證和生成的協同循環，保證了模型能力的持續突破。

實驗結果

研究采用GRPO進行強化學習，迭代地優化證明驗證和生成能力。

在每次迭代中，研究首先優化證明驗證。然后，證明生成器會從驗證器的checkpoint初始化，并針對證明生成進行優化。

從第二次迭代開始，證明驗證器會使用一個檢查點進行初始化，該檢查點通過拒絕微調（rejection fine-tuning）鞏固了前一次迭代中的驗證和生成能力。

研究首先評估了模型未經迭代完善的單次生成正確證明的能力。

實驗結果表明，在所有CNML級別問題類別中——包括代數、幾何、數論、組合學和不等式——DeepSeekMath-V2 持續優于 GPT-5-Thinking-High和Gemini 2.5-Pro。

為了探究擴展上下文和自驗證如何提高證明質量，研究又評估了帶有自驗證的順序精煉方法。

研究表明，自選的最佳證明比線程平均得分獲得了顯著更高的驗證分數，這證明生成器具備準確評估證明質量的能力。

此外，隨著最大順序嘗試次數的增加，Pass@1大幅提升，表明自驗證有效地指導了迭代改進。

這些結果表明，生成器能夠可靠地區分高質量和有缺陷的證明，并利用這種自我意識系統地改進其數學推理。

最后，為了解決最具備挑戰性的問題，研究采用了高計算量搜索策略，該策略通過并行生成探索多樣化的證明路徑，并結合規模化的（64 次）驗證來精確識別細微錯誤。

模型迭代地從包含問題分析的候選證明池中精煉出最優證明，直到證明通過所有驗證。

最終，這種方法使其在Putnam競賽中以118/120的分數超越人類最高分90分，展現了在驗證器指導下，AI解決復雜問題的強大能力。

One more thing

如開頭所說，這篇論文的一作邵智宏也是DeepSeek之前數學模型DeepSeekMath 7B的一作。

值得一提的是，也就是在DeepSeekMath 7B的論文中，他和團隊提出了經典的GRPO（Group Relative Policy Optimization ）。同樣的，他也是DeepSeek-R1的核心貢獻者。

邵智宏目前是DeepSeek從事大模型推理研究的研究員，他本科畢業于北京航空航天大學，博士畢業于清華，師從黃民烈教授。

[1] https://huggingface.co/deepseek-ai/DeepSeek-Math-V2

[2]https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf

[3]https://zhihongshao.github.io/