DeepSeek「五一禮包」來了！新開源模型數學推理能力大提升｜附實測細節

趕在五一假期前夕，DeepSeek 給我們送出一份驚喜大禮。

延續一貫的開源節奏，DeepSeek 在 Hugging Face 正式釋出 DeepSeek-Prover-V2，並同步上線模型卡及示例程式碼。此次共推出兩個版本：

DeepSeek-Prover-V2-7B：基於上一代 V1.5 模型，支援最長 32K 上下文輸入；

DeepSeek-Prover-V2-671B：在 DeepSeek-V3-Base 基礎上訓練，推理效能最強。

*核心貢獻者 †在 DeepSeek-AI 實習期間完成的工作，掃描文末二維碼，進社群獲取完整報告

據官方論文披露，DeepSeek-Prover-V2 的訓練核心是「遞迴+強化學習」的組合：即先由 DeepSeek-V3 拆解複雜定理，生成一系列子目標和推理思路；再透過 GRPO 演算法，從多種候選方案中自動學習如何選出最優解。

模型特別引入了兩種互補的「解題風格」：

快速模式（non-CoT）：專注於速度，像是一位熟練工匠，直接生成精煉的 Lean 程式碼答案，不展示思考過程，適合處理大量題目。

邏輯模式（CoT）：更像一個耐心的數學老師，會詳細列出每一步推理過程，確保邏輯清晰、思路透明。

訓練過程分為兩階段，在第一階段，研究人員主要訓練快速模式，採用「專家迭代」方法：模型先嚐試解決難題，成功的答案再作為新資料反哺模型，不斷打磨自己的能力。

待快速模式趨於穩定後，研究人員進入第二階段，開始訓練更復雜的邏輯推理能力。他們將 DeepSeek-V3 的數學知識遷移到新模型中，並結合形式化資料，引入「冷啟動」機制，構建起更復雜的推理路徑。

為了進一步提升推理能力，研究人員引入了 GRPO 的強化學習演算法，不同於傳統的 PPO，它直接在多個候選答案中比較優劣，引導模型自主學會選擇最優解。

具體做法是：每次輸入一個定理，系統會生成 32 個不同的證明方案，然後只保留被 Lean 驗證系統判定為「正確」的答案（獎勵 1 分，否則 0 分），這樣模型就能在高質量反饋中不斷進化。

在開發出效能強大的 671B 模型後，DeepSeek 研究團隊又嘗試把這些能力「蒸餾」到更小的 7B 模型中，而整個過程就像是師傅教徒弟:

先用大模型生成解題過程，再教會小模型理解並復現；同時將小模型輸入長度擴充套件至與大模型一致，並經歷相同的強化訓練。

這樣，即便在資源有限的裝置上，使用者也能使用小體積模型獲得接近大模型的數學推理能力，並根據需求選擇快速或詳細解題風格。

整個體系中，DeepSeek-V3 負責拆解複雜定理，生成自然語言的推理草圖，同步轉譯為 Lean 語言表示的一系列子目標，並生成「思路鏈」作為中間引導。

7B 模型再一步步完成子證明，最終拼接成完整推理。這種「模糊思考 + 精確證明」的訓練機制，有效提升了小模型的數學理解深度。

在最終效能評估中，DeepSeek-Prover-V2-671B 在 MiniF2F 測試中實現了 88.9% 的透過率，成功解出 PutnamBench 資料集中的 49 道難題。

與此同時，DeepSeek 還同步推出了一個全新的數學形式化資料集 ProverBench，共包含 325 道問題題目。涵蓋：

AIME 競賽題（15 題）

數論、代數、線性代數、微積分、實分析等多個方向

這一資料集不僅包含真實的高中競賽題目，還涵蓋從基礎代數、實變分析到機率論等多個本科階段知識點，能夠系統評估模型在不同數學領域的推理能力。

結果顯示，在 15 道 AIME 競賽題中，DeepSeek-Prover-V2 成功解出其中 6 道，而 DeepSeek-V3 使用多數投票方式（majority voting）則解決了 8 道。

按照官方的說法，這組對比凸顯出一個重要趨勢：大型語言模型在「非正式數學推理」和「正式數學推理」之間的表現差距正在明顯縮小。

非正式數學推理：指模型像人類一樣用自然語言思考、理解並解答數學題，比如我們日常說「這道題怎麼算？」的方式。它更靈活、不需要嚴格的邏輯形式。

正式數學推理：指模型能用像 Lean 這樣的形式語言，寫出符合數學邏輯、可被驗證器檢驗的嚴謹證明。它像數學論文中的證明，強調每一步推理都必須嚴格準確。

換句話說，過去模型更像是「會算但不會寫出嚴謹證明」。而現在，在模型結構和訓練策略不斷演進下，語言模型也逐步學會了寫出規範、可驗證的數學證明。

此外，DeepSeek 宣佈新模型的使用將遵循其公開許可證。

🔗 https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/LICENSE-MODEL

目前，Prover-V2 系列已可透過 Hugging Face 平臺免費下載，並支援 Transformers 介面部署。Novita AI 是首批上線 Prover-V2-671B 推理服務的第三方提供商，我們也藉此測試了一些問題。

經典的「一根 5.5 米長的竹竿可以透過高 4 米寬 3 米的門嗎？」很遺憾，結果它沒答對。

對於這道抽象代數，它的回答不僅正確，還能從基本定義出發，解釋了什麼是群同態、Z₁₂ 和 Z₄ 的含義，以及同態的運算規則，顯然，這對於初學者很友好。

從論文所透露的方向來看，DeepSeek-Prover-V2 給出的不僅是數學答案，更指明瞭語言模型下一階段的可能路徑。

如果說過去我們關心的是大模型「能說什麼」，那麼在 Prover-V2 身上，我們得需要關注它「能證明什麼」。

數學只是切入口，推理才是 DeepSeek 這次真正下注的方向。

從生成內容邁向生成結構化邏輯，這條路線不夠性感，也不容易講故事，卻可能最早觸碰通用人工智慧的底層結構。

畢竟，AI 可以不懂人情世故，但它必須學會推理，因為任何知識系統的邊界，歸根結底都是邏輯能否閉環、以及推理能否成立。

最後附上相關地址：

1️⃣ DeepSeek-Prover-V2-7B HuggingFace 地址：

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

2️⃣ DeepSeek-Prover-V2-671B HuggingFace 地址：

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

3️⃣ DeepSeek-ProverBench HuggingFace 地址：

https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

4️⃣

DeepSeek-Prover-V2

GitHub 地址：

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

文 | Prover