繼昨日放出新開源模型 Prover V2 之后，DeepSeek 在今天又公布了它的技術報告。

這份報告長達 34 頁，披露了更多該模型的重要技術細節和基準測試表現，讓我們有機會進一步了解它的創新之處。

DeepSeek Prover V2 系列模型有兩個尺寸：7B 和 671B 參數。

DeepSeek-Prover-V2-671B 在 DeepSeek-V3-Base 基礎上進行訓練，推理性能更強。

DeepSeek-Prover-V2-7B 則基于 DeepSeek-Prover-V1.5-Base 構建，上下文長度得到了擴展，最高可達 32K token。

其中，DeepSeek-Prover-V2-671B 在神經定理證明（neural theorem proving）領域超越了之前的模型：MiniF2F 測試集在 Pass@32 下達到了 82.4% 的準確率。

（來源：DeepSeek）

兩個模型都已經開源，可以在開源社區 Hugging Face 上找到。技術論文則是在 GitHub 上（模型和論文鏈接在文末）。

據論文介紹，DeepSeek Prover V2 是一個專為 Lean 4 形式定理證明設計的開源大型語言模型。其最大創新點在于，能將非形式化的數學推理能力與嚴格的形式化證明過程結合在一起，實現了兩種思維模式的有效融合。

你可以想象一下，當我們要解決一道數學題時，腦海中往往先有一個大致的思路，然后再一步步填充細節。這種從整體到局部、從思路到步驟的過程，對人類來說很自然，但對AI卻是一項艱巨的挑戰。

在 AI 發展歷程中，GPT 和 Claude 等大語言模型（LLM，Large Language Model）已經展示出令人印象深刻的數學問題求解能力。它們能夠通過“思維鏈”（CoT，Chain-of-Thought）方法，像人類一樣逐步思考問題，甚至能解決一些競賽級別的難題。

圖丨獲得美國普林斯頓大學副教授王夢迪點贊（來源：X）

然而，在更為嚴格的數學領域——形式化定理證明方面，AI 的表現卻相對遜色。

原因在于兩種思維模式的本質差異：自然語言推理是靈活的、啟發式的，允許一定程度的模糊性和跳躍性思維；而形式化證明則要求百分百的精確性和嚴謹性，每一個推理步驟都必須經過嚴格驗證，不允許任何隱含假設和細節省略。

就像兩種不同的語言，雖然表達的是同一個數學世界，但規則和要求卻大相徑庭。

為了解決這一挑戰，DeepSeek-Prover-V2 采用了一種創新的“遞歸定理證明流程”，這一流程的靈感源自人類數學家解決復雜問題的方法——將困難問題分解為一系列更容易解決的子問題。

圖 | 遞歸定理證明流程概括（來源：DeepSeek）

首先，研究團隊利用 DeepSeek-V3 模型擔任“分解專家”的角色，構建定理證明系統的基礎框架。

當面對一個復雜的數學定理時，DeepSeek-V3 會用自然語言分析和理解問題，提出高層次的證明思路，將整個證明分解為一系列較小的子目標，最后將每個子目標翻譯成嚴格的 Lean 4 形式語言表達，由 have…sorry 語句組成，也就是需要解決的子目標。

這種方法也是人類所用的證明構建方式，即將復雜定理逐步簡化為一系列更易管理的引理。

一旦復雜問題被分解為多個子目標，研究團隊就會使用更小的 7B 參數模型作為解題專家，逐一攻克這些子目標。這種方法不僅提高了效率，還大幅降低了計算資源的消耗。

DeepSeek 采用遞歸求解策略系統地解決每個中間證明步驟。他們從 have 語句中提取子目標表達式，用它們替代原始問題中的目標，并將前面的子目標作為前提條件。

這種構建使后續子目標能夠利用早期步驟的中間結果，從而促進更局部化的依賴結構，有助于開發更簡單的引理。

為了減少大量證明搜索的計算開銷，使用專門優化的小型 7B 證明模型處理分解后的引理。成功解決所有分解步驟后，原始定理的完整證明就可以自動推導出來。

（來源：DeepSeek）

在這個過程中，證明模型的訓練需要大型形式語言問題集，但從人類編寫文本形式化獲得的訓練信號通常較為稀疏，因為大部分計算嘗試都不會產生成功的證明，因此不提供積極的獎勵信號。

為了產生更密集的訓練信號，DeepSeek 利用子目標擴展用于模型訓練的形式語句范圍，生成兩類子目標定理：一類將前面的子目標作為前提條件，另一類則不包含前提條件。

這兩類子目標被整合到專家迭代階段，建立一個課程（curriculum），逐步引導證明模型系統地解決精心策劃的一系列挑戰性問題。

隨后，研究團隊挑選了一些 7B 證明模型無法“端到端（完全）解決”，但“所有子目標均已成功解決”的挑戰性問題。通過組合所有子目標的證明，他們構建了原始問題的完整形式證明。這個證明再與 DeepSeek-V3 的自然語言推理過程配對，創建了“冷啟動推理數據”。

“這使我們能夠收集數百個高質量的合成冷啟動數據，作為訓練 DeepSeek-Prover-V2 的基礎。”論文寫道。

這些冷啟動數據之所以珍貴，是因為它們同時包含了兩種形式的數學推理：直觀的自然語言思考鏈和嚴格的形式化證明步驟。就像是給 AI 提供了一本內容豐富的“雙語教材”，幫助它學習如何在兩種表達方式之間自如轉換。

有了冷啟動數據后，研究團隊通過面向推理的強化學習（Reasoning-oriented Reinforcement Learning）進一步優化模型性能。在這個階段，DeepSeek-Prover-V2 會學習如何更好地連接非形式推理與形式證明構建，特別注重保持證明結構與初始分解思路的一致性。

這個過程類似于學生在掌握基本思路后，通過不斷練習和反饋來提升解題能力，逐漸形成自己的解題風格和策略。

在訓練階段，DeepSeek-Prover-V2 采用了兩階段訓練策略，建立了兩種互補的證明生成模式：

• 高效非鏈式思維（non-CoT）模式：快速生成簡潔的形式 Lean 證明代碼，不包含明確的中間推理步驟。
• 高精度鏈式思維（CoT）模式：系統地闡述中間推理步驟，強調透明度和邏輯進展，構建最終形式證明。

訓練過程中，研究團隊使用“專家迭代”方法不斷提升模型能力。每次迭代中，用當前最佳模型（策略）嘗試解決之前未能解決的問題，成功的證明被添加到訓練數據中，用于改進模型。

這個迭代循環持續進行，使模型能夠逐步提高解決難題的能力。

此外，在強化學習階段，DeepSeek 使用了“群體相對策略優化”的算法，相比傳統 PPO 效果更好、效率更高。

性能方面，DeepSeek-Prover-V2 在多個主流基準測試中都取得了不錯的成績。

在評估 AI 形式證明能力的標準測試集 MiniF2F 中，DeepSeek-Prover-V2-671B 創造了新記錄。在嘗試 32 次（Pass@32）的情況下達到了 82.4% 的準確率，當增加到 8192 次（Pass@8192）時，表現提高到了 88.9%。

圖 | 在 MiniF2F 測試集上的表現（來源：DeepSeek）

即使是參數較少的 DeepSeek-Prover-V2-7B 也超越了以往所有開源定理證明模型。

在評估大學水平數學能力的 ProofNet 和 PutnamBench 測試中，DeepSeek-Prover-V2-671B 同樣表現出色。在 ProofNet 測試集上，它以 Pass@1024 指標達到了 37.1% 的解題率。在極具挑戰性的 PutnamBench 上成功解決了 658 個問題中的 49 個。

更加令人驚訝的是，研究團隊發現較小的 7B 模型在某些特定問題上甚至超越了 671B 的大模型，成功解決了 13 個大模型未能攻克的問題，將總解題數提升至 62 題。

在更全面的 CombiBench 測試中，DeepSeek-Prover-V2 在 77 個問題中解決了 12 個。雖然這一數字看似不高，但考慮到模型主要在數論和代數領域訓練，這一表現已經展示了其良好的跨領域泛化能力。

在 15 個來自 AIME 24 和 25 競賽的數學問題上，DeepSeek-Prover-V2-671B 成功解決了 6 個，而其通用語言模型 DeepSeek-V3 則解決了 8 個。

研究團隊認為這一對比結果很有趣，因為它表明形式數學證明與非形式數學推理之間的能力差距正在顯著縮小。

最后，DeepSeek 團隊計劃將創造 DeepSeek-Prover-V2-671B 的經驗擴展稱一個類似 AlphaProof 的系統，最終目標是挑戰國際數學奧林匹克級別的數學問題。

至于傳聞中的下一代 V4/R2 模型，說不定也會用上相關的技術進展。

參考資料：

https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main

論文鏈接：

https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf

模型鏈接：

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B

排版：劉雅坤