
一個能夠自我驗證的 AI 系統,正離攻克研究級數學問題更近一步。
11 月 27 日,DeepSeek 正式開源了其全新模型 DeepSeekMath-V2,這是一款具備“奧數金牌級”定理證明能力的 AI 系統。
DeepSeekMath-V2 在 2025 國際數學奧林匹克(IMO 2025)和 2024 中國數學奧林匹克(CMO 2024)中展現了金牌水準的表現。更令人矚目的是,它在 2024 普特南數學競賽中取得了 118/120 的幾乎滿分成績,遠遠超過目前已知的人類最高分 90 分。
從效能評測來看,DeepSeekMath-V2 在 IMO-ProofBench 等關鍵證明測試中,以 10% 的明顯優勢擊敗了谷歌的 IMO 金獎模型 DeepThink。
這些成果揭示了一個突破性的結論:自我可驗證的數學推理不僅是可能的,而且可能是打造更強數學 AI 系統的關鍵道路。
按照 DeepSeek 一貫做法,該模型在釋出後立即上線可用。在初步測試中,DeepSeekMath-V2 能迅速給出經典題目的正確證明,例如“證明 √2 是無理數”。當輸入“奇數和偶數哪個更多?”時,它也給出了嚴謹且結構清晰的證明過程,即使非專業人士也能理解。當然,奧數級的證明題要複雜得多,高水平數學讀者可以自行嘗試更深入的體驗。
回顧模型背後的研究思路,傳統強化學習(RL)在只需要最終答案的競賽(如 AIME 或 HMMT)中可以獲得高分,但 DeepSeek 指出這種方法天然存在兩個關鍵侷限:
首先,僅憑最終答案不能可靠反映推理正確性。模型可能通過邏輯漏洞或僥倖路徑獲得正確結果。
其次,它不適用於定理證明場景,因為此類問題考察的核心不是最後答案,而是嚴謹的推導過程本身。
為解決這個問題,DeepSeek 專注於在大語言模型中建立顯式證明驗證能力。基於 DeepSeek-V3.2-Exp-Base,DeepSeekMath-V2 被訓練為理解獎勵機制,並通過有意識的推理而非盲目試錯來最佳化證明質量。
DeepSeek 為證明評估建立了一套高階評分標準,使模型能夠模擬數學專家的判斷方式。以 DeepSeek-V3.2-Exp-SFT 為基礎版本,通過強化學習訓練模型生成證明分析,並採用格式獎勵和評分獎勵兩種核心機制。
訓練資料集包括 17503 道數學競賽題目、模型生成的候選證明,以及人工專家評分的證明樣本,形成了極大的強化學習訓練語料庫。DeepSeek 隨後為生成器和驗證器分別定義了強化學習目標。雖然這一機制讓分析能力更強,但研究人員發現了一個潛在漏洞:驗證器可能通過生成看似合理的分數來“操縱系統”,而並未真正理解證明問題。
為修復這一點,DeepSeek 引入了“元驗證”(meta-verification)機制,通過第二層分析模型,大幅提高判斷證明質量的可信度。
在證明生成階段,模型被訓練為循序檢查推理過程,而不是直接宣稱證明正確。這樣可以防止模型在驗證器指出錯誤後仍堅持自己沒有錯誤。
最終,DeepSeek 的驗證器與生成器形成了一個協同迴圈:驗證器幫助生成器改進,而生成器不斷產生新的證明挑戰驗證器;這些挑戰又成為訓練驗證器的寶貴資料。簡單來說:驗證器逐步檢查推理,生成器從錯誤中自我修正。
實驗結果表明,在 CNML 的所有數學類別(代數、幾何、數論、組合數學、不等式)中,DeepSeekMath-V2 始終優於 GPT-5-Thinking-High 和 Gemini 2.5-Pro,展現出更卓越的定理證明能力。
在帶自我驗證的順序最佳化中,DeepSeekMath-V2 在 2024 IMO 備選題上的證明質量顯著提升,並顯示其能夠準確區分高質量與有缺陷的證明,並自主最佳化推理。
在高計算量推理實驗中,該系統成功解決了 IMO 2025 中 6 題中的 5 題,以及 CMO 2024 中 4 題 + 1 題部分分數的解答,取得了金牌水準成績。不僅在基礎測試集上超過了 DeepMind 的 DeepThink,而且在高階測試集上依然保持競爭力。
不過 DeepSeek 也指出,最難的 IMO 級題目仍對模型構成挑戰。
值得注意的是,對於未完全解決的問題,DeepSeekMath-V2 通常能在自己的證明中識別出真正的推理障礙;而對完全解決的問題,其證明能通過 64 輪驗證嘗試而無衝突。這表明驗證器已經能夠評估那些此前被認為幾乎不可能自動驗證的證明。
通過在推理階段提升計算投入,DeepSeek 的模型能夠解決那些需要人類耗費數小時才能完成的題目。
結論:一個能夠自我驗證的 AI 架構,可能是攻克研究級數學的核心突破。
總的來說,DeepSeek 打造了一個既能生成又能審查數學證明的模型。團隊突破了基於最終答案的獎勵機制侷限,邁向了真正的自我驗證數學推理時代。
這一成果表明,大語言模型能夠發展出適用於複雜推理任務的元認知能力。儘管仍有挑戰,但這一研究方向已經讓 AI 更接近目標:構建真正能夠自我驗證的 AI 系統,解決研究級數學問題。