DeepSeek 發表 Prover-V2：671B 參數的數學定理證明模型

DeepSeek 於 2025 年 4 月 30 日發表 DeepSeek-Prover-V2-671B，一款鎖定「數學定理證明」的專用模型。它建構於支撐 DeepSeek-V3 的 671B 參數混合專家（MoE）架構之上，任務聚焦在 Lean 4 這套形式化證明輔助工具框架中，自動生成並驗證數學證明的正確性。官方公布的基準測試顯示，該模型在 MiniF2F-test 測試集上達到 88.9% 的通過率，並在難度更高的 PutnamBench 題庫（收錄美國大學生數學競賽 Putnam 的題目）658 題中解出 49 題。模型以開源形式釋出於 Hugging Face，並附上允許商業使用的授權條款。

技術意義：MoE 架構把「推理成本」壓下來

模型總參數量高達 671B，但採用 MoE 設計，每次生成一個 token 時只實際啟用約 370 億參數，其餘專家模組保持休眠。這種「按需喚醒」機制讓 DeepSeek 得以維持大規模知識容量，同時把單次推理成本壓低到接近中型模型的水準。對形式化證明這種需要反覆嘗試、驗證、回溯的任務而言，推理效率直接決定模型能在有限時間內探索多少條證明路徑，這也是 Prover-V2 敢於挑戰 Putnam 級別題目的底氣所在。

與前代及同類模型的比較

形式化定理證明是相對窄但技術門檻極高的 AI 應用領域，此前形式化證明領域的先進成果多集中在少數頂尖實驗室。DeepSeek 此次選擇以開源、可商用授權的方式釋出 Prover-V2，等於是把原本集中在少數實驗室的能力，以低成本方式開放給全球研究者與企業使用。這延續了 DeepSeek 自 R1 以來一貫的策略：用開源模型快速搶佔特定垂直技術領域的話語權，而非只做通用對話模型的軍備競賽。

業界反應：開源策略持續施壓

Prover-V2 發布的時間點，正好落在 DeepSeek 醞釀下一代旗艦模型「R2」之前，被外界解讀為技術實力的預熱動作。對其他 AI 廠商而言，DeepSeek 一再以開源、免費商用的形式釋出高規格模型，持續壓縮閉源模型廠商的定價與差異化空間，也讓「數學推理能力」成為繼程式碼生成之後，另一個開源陣營急起直追的戰場。

對管理者的意義

Prover-V2 本身是高度學術化的工具，多數管理者不會直接使用，但它反映的趨勢值得留意：AI 在「需要嚴謹邏輯、可驗證正確性」的任務上正快速進步，未來財務模型稽核、合約條款一致性檢查、工程規格驗算等講求「零錯誤」的管理場景，都可能出現對應的 AI 輔助工具，值得持續關注同類技術何時走向企業應用。