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 宣布新模型的使用將遵循其公開授權。
目前，Prover-V2系列已可透過Hugging Face平台免費下載，並支援Transformers介面部署。 Novita AI是首批上線Prover-V2-671B推理服務的第三方供應商，我們也藉此測試了一些問題。
經典的「一根5.5 公尺長的竹竿可以通過高4 公尺寬3 公尺的門嗎？」很遺憾，結果它沒答對。
對於這道抽象代數，它的回答不僅正確，還能從基本定義出發，解釋了什麼是群同態、Z₁₂和Z₄的含義，以及同態的運算規則，顯然，這對於初學者很友好。
從論文所透露的方向來看，DeepSeek-Prover-V2給出的不僅是數學答案，更指明了語言模型下一階段的可能路徑。
如果說過去我們關心的是大模型“能說什麼”，那麼在Prover-V2身上，我們得需要關注它“能證明什麼”。
數學只是切入口，推理才是DeepSeek這次真正下注的方向。
從生成內容邁向生成結構化邏輯，這條路線不夠性感，也不容易說故事，卻可能最早觸碰通用人工智慧的底層結構。
畢竟，AI可以不懂人情世故，但它必須學會推理，因為任何知識系統的邊界，歸根究底都是邏輯能否閉環、以及推理能否成立。