剛剛，DeepSeek開源新模型，拿下奧數證明題冠軍

智東西
作者 李水青
編輯 心緣

智東西11月17 日報道，今日，DeepSeek開源了“奧數金牌級”模型DeepSeekMath-V2，該模型具備強大的定理證明能力。

DeepSeekMath-V2在2025年國際數學奧林匹克競賽（IMO 2025）和2024年中國數學奧林匹克競賽（CMO 2024）上取得了金牌水平的成績；并在2024年普特南大學生數學競賽（Putnam 2024）上取得了接近滿分（118/120分）的成績，超過人類最高的90分成績。

如下圖所示，DeepSeekMath-V2以10%的優勢擊敗谷歌的IMO金獎得主DeepThink模型。

▲DeepSeekMath-V2在數學競賽中的成績表現

▲DeepSeekMath-V2在IMO-ProofBench的測評結果

上述結果表明，自驗證數學推理是一個可行的研究方向，可能有助于開發更強大的數學AI系統。

Hugging Face地址：
https://huggingface.co/deepseek-ai/DeepSeek-Math-V2
論文地址：
https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf

按慣例，DeepSeek往往會將新開源的模型直接上線DeepSeek，我們第一時間嘗試進行了體驗。

首先讓DeepSeek證明一道較簡單的題目“證明根號2為無理數”，DeepSeek快速給出了正確答案。

當智東西輸入“證明奇數和整數哪個多？”這一證明題，DeepSeek也給出了正確證明過程和答案，這一證明過程大部分人應該可以看懂。當然，奧數級證明題會更加復雜，如果有能夠看懂理解這類題目的讀者，可以再進一步進行體驗測試。

回到模型背后的研發問題，我們來具體看看論文內容，從已有的研究來看，在數學推理領域，強化學習（RL）傳統方法足以讓大模型在主要評估最終答案的數學競賽（如AIME和HMMT）中達到很高的水平。然而這種獎勵機制存在兩個根本性的局限性：

首先，傳統方法不能可靠地代表推理的正確性，模型可能通過有缺陷的邏輯或僥幸的錯誤得出正確答案。

其次，它不適用于定理證明任務，在這類任務中，問題可能不需要生成數值形式的最終答案，而嚴謹的推導才是主要目標。

為此，DeepSeek建議在大型語言模型中開發證明驗證能力，基于DeepSeek-V3.2-Exp-Base開發了DeepSeekMath-V2。他們讓模型明確了解其獎勵函數，并使其能夠通過有意識的推理而非盲目的試錯來最大化這一獎勵。

DeepSeek制定了用于證明評估的高級評分標準，目的是訓練一個驗證器，使其能根據這些評分標準對證明進行評估，模擬數學專家的評估過程。以DeepSeek-V3.2-Exp-SFT的一個版本為基礎，通過強化學習訓練模型生成證明分析，訓練過程使用了兩個獎勵組件：格式獎勵和分數獎勵。

然后是構建強化學習數據集。DeepSeek基于17503道競賽題目、DeepSeek-V3.2-Exp-Thinking生成的候選證明、帶專家評分的隨機抽取的證明樣本，構建了初始強化學習訓練數據集。

緊接著，其設置了強化學習目標和訓練驗證器的強化學習目標。具體是以DeepSeek-V3.2-Exp-SFT的一個版本為基礎，通過強化學習訓練模型生成證明分析，訓練過程使用了兩個獎勵組件：格式獎勵和分數獎勵。而后通過下列函數完成訓練驗證器的強化學習目標。

為了解決訓練過程中“驗證器可能通過預測正確分數同時虛構不存在的問題來獲得全部獎勵”這一漏洞，DeepSeek引入了一個二次評估過程——元驗證（meta-verification），從而提高驗證器識別問題的忠實度。

在證明生成階段，DeepSeek進行了證明生成器的訓練，并通過自我驗證增強推理能力，解決模型被要求一次性生成并分析自己的證明時“生成器不顧外部驗證器判錯而宣稱證明是正確的”。

最后，DeepSeek證明驗證器和生成器形成了一個協同循環：驗證器改進生成器，而隨著生成器的改進，它會生成新的證明，這些證明對驗證器當前的能力構成挑戰，這些挑戰也成為增強驗證器自身的寶貴訓練數據。

簡單來說，DeepSeekMath-V2模型中的驗證器能完成逐步檢查證明過程，而生成器則會修正自身的錯誤。

從實驗結果來看，在單步生成結果評估中，如圖1所示，在CNML級別的所有問題類別（代數、幾何、數論、組合數學和不等式）中，DeepSeekMath-V2始終優于GPT-5-Thinking-High和Gemini 2.5-Pro，展現出在各領域更卓越的定理證明能力。

在帶自我驗證的順序優化中，其對2024 IMO備選題進行連續優化后，證明質量提升。自選的最佳證明比線程平均值獲得了顯著更高的驗證分數，這表明生成器能夠準確評估證明質量。這些結果證實，其生成器能夠可靠地區分高質量證明和有缺陷的證明，并利用這種自我認知系統地改進其數學推理能力。

在高計算量探索中，DeepSeek擴大了驗證和生成計算的規模，他們的方法解決了2025 IMO的6道題中的5道，以及2024 CMO的4道題，另外1道題獲得部分分數，在這兩項頂尖高中競賽中均達到金牌水平，在基礎集上優于DeepMind的DeepThink（IMO金牌水平），在高級集上保持競爭力，同時大幅優于所有其他基線模型。

但DeepSeek發現，最困難的IMO級別問題對其模型來說仍然具有挑戰性。

值得注意的是，對于未完全解決的問題，DeepSeek的生成器通常能在其證明過程中識別出真正的問題，而完全解決的問題則能通過所有64次驗證嘗試。這表明，我們能夠成功訓練基于大語言模型的驗證器，以評估那些此前被認為難以自動驗證的證明。通過在驗證器的指導下增加測試時的計算量，DeepSeek的模型能夠解決那些需要人類競爭者花費數小時才能解決的問題。

結語：可自我驗證的AI系統，離解決研究級數學問題更進一步

總的來說，DeepSeek提出了一個既能生成又能驗證數學證明的模型。團隊突破了基于最終答案的獎勵機制的局限性，邁向了可自我驗證的數學推理。

這項工作證實，大語言模型能夠培養出針對復雜推理任務的有意義的自我評估能力。盡管仍存在重大挑戰，這一研究方向有望為創建可自我驗證的AI系統解決研究級數學問題這一目標做出貢獻。