趕在五一假期前夕，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-V2GitHub 地址：
https://github.com/deepseek-ai/DeepSeek-Prover-V2

文 | Prover

我們正在招募伙伴

簡歷投遞郵箱hr@ifanr.com

?? 郵件標題「姓名+崗位名稱」（請隨簡歷附上項目/作品或相關鏈接）