剛剛，DeepSeek 開源了全新的數學模型 DeepSeekMath-V2，專注可自驗證的數學推理框架。
DeepSeek-Math-V2 在 IMO-ProofBench 和 IMO 2025（6 道題中的 5 道）和 Putnam 2024（接近完美的 118/120 分）等比賽中表現出色。
新模型可以通過驗證器-生成器循環進行自驗證推理，代表自主數學發展取得重大飛躍。
邵智宏為此篇論文一作，也是之前提出 GRPO 的 DeepSeekMath 7B 一作。
自驗證模型
實驗表明，正確的答案并不能保證推理過程的正確性。此外，許多數學任務需要嚴謹的逐步推導，這使得最終答案獎勵不再適用。
為了突破深度推理的極限，DeepSeek 認為有必要驗證數學推理的全面性和嚴謹性。自驗證對于擴展測試時間計算能力尤為重要，特別是對于那些尚無已知解決方案的開放性問題。
為了實現可自驗證的數學推理，團隊研究了如何訓練一個基于大型語言模型的定理證明驗證器，再以驗證器為獎勵模型訓練一個證明生成器，并激勵生成器在最終定稿前盡可能多地識別和解決自身證明中的問題。
為了在生成器性能提升的同時保持生成與驗證之間的差距，DeepSeek 團隊提出擴展驗證計算能力，以自動標記新的難以驗證的證明，從而創建訓練數據以進一步改進驗證器。
DeepSeekMath-V2 展現了強大的定理證明能力，在 IMO 2025 和 CMO 2024 上取得了金牌水平的成績，并在 Putnam 2024 上取得了接近完美的 118/120 分（測試時間計算量已擴展）。
這些結果表明，可自我驗證的數學推理是一個可行的研究方向，可能有助于開發更強大的數學人工智能系統。
驗證方法
團隊還引入了元驗證：這是一個輔助評估過程，用于評估驗證者識別出的問題是否確實存在，以及這些問題是否根據評估標準在邏輯上證明了預測的證明分數。
該元驗證器會生成一份分析中發現問題的摘要，并給出一個質量評分，用于衡量驗證器分析的準確性和合理性。
利用訓練好的元驗證器 ??，研究人員通過將元驗證反饋整合到獎勵函數中來增強驗證器的訓練。
證明驗證器和生成器形成了一個協同循環：驗證器改進生成器，而隨著生成器的改進，它會生成新的證明，從而挑戰驗證器當前的性能。
為了提高標注效率，研究人員對每個證明生成多個驗證器分析，以便發現潛在問題供人工審核。
通過人工智能輔助標注過程，團隊發現了兩個事實：
擴大驗證器樣本規模可以提高發現有缺陷證明中真正問題的概率；
審查驗證者發現的問題實際上就是元驗證，對于語言學習來說，掌握元驗證也更節省樣本成本。
這兩個發現使得進一步提高自動化程度成為可能。
實驗結果
在所有 CNML 級別問題類別（代數、幾何、數論、組合數學和不等式）中，DeepSeekMath-V2 的性能始終優于 GPT-5-Thinking-High 和 Gemini 2.5-Pro ，展現了其在各個領域卓越的定理證明能力。
通過對 IMO 2024 短名單題目進行順序精煉，模型可以提升證明質量的過程。每個題目有 32 個獨立的精煉線程。用戶自行選出的最佳證明的驗證得分顯著高于線程平均水平，這表明生成器能夠準確評估證明質量。
自驗證能夠有效地指導迭代改進。生成器能夠區分高質量證明和有缺陷的證明，并利用這種自我感知能力系統地改進其數學推理能力。
模型解決了 IMO 2025 的 6 道題中的 5 道，以及 CMO 2024 的 4 道題，并在另一道題上獲得了部分分數，在這兩項頂尖高中數學競賽中均取得了金牌成績。
在 Putnam 2024（頂尖的本科生數學競賽）中，模型完全解決了 12 道題中的 11 道，剩余的 1 道題也僅有少量錯誤，最終得分 118/120，超過了人類最高分 90 分。
模型的方法在基礎數據集上優于 DeepMind 的 DeepThink（IMO 金牌得主），在高級數據集上也保持競爭力，同時顯著優于所有其他基線模型。但是，IMO 級別最難的問題仍然具有挑戰性。
值得注意的是，對于尚未完全解決的問題，生成器通常能夠識別出其證明中存在的真實問題，而完全解決的問題則通過了全部 64 次驗證嘗試。這表明基于 LLM 的驗證器能夠自動評估以前被認為難以驗證的證明。
參考資料：
https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf
分享
