DeepSeek 壞得很，假前給大家送勞動節禮物來了，不過這次不是 DeepSeek-R2。
4 月 30 日，DeepSeek 正式推出 DeepSeek-Prover-V2-671B，標誌著 AI 數學推理能力邁入新紀元。
DeepSeek-Prover-V2-671B 是什麼？
作為 DeepSeek 開源模型系列的新一代自動定理證明專家，該模型基於與 DeepSeek-V3 相同的 6710 億引數混合專家（MoE）架構，專為 Lean 4 證明輔助框架中的證明生成與驗證而最佳化。
其 MoE 設計採用動態引數啟用機制，單次推理僅呼叫約 370 億引數（根據 DeepSeek 官方 MoE 架構報告推測，例如 V3 的技術方案），在保持強大推理能力的同時顯著提升計算效率。
核心突破價值
本次釋出具有三大里程碑意義：
-
實現形式化數學的「GPT-4 級」突破：憑藉超大規模引數量與約 128k tokens 的上下文視窗，可處理高階數學證明中特有的複雜長邏輯鏈。
-
MoE 架構效能優勢：相比稠密的 6710 億引數模型，大幅降低記憶體需求並提升運算速度。該技術可能延續了 DeepSeek-V2 的多頭潛在注意力機制（MLA），此前已實現 KV 快取壓縮與吞吐量突破。
-
開放商用許可：延續 DeepSeek Prover V1.5 等前代模型傳統，預計在 Hugging Face 開源權重並允許商業應用，為學術與工業界提供普惠化支援。
實際應用場景
該模型為多個領域帶來革新可能：
-
形式化驗證：在密碼學安全證明、晶片設計驗證等自動化流程中實現嚴格數學檢驗
-
數學研究加速：協助數學家完成定理形式化、新猜想探索，乃至奧賽級數學難題的證明推導
-
智慧教育工具：構建可驗證步驟的互動式教學系統，引導學生掌握嚴謹的數學證明方法
-
關鍵系統安全：透過Lean整合，在軟體部署前直接驗證核心程式碼邏輯的正確性與不變性
技術架構解析
根據 DeepSeek-V3 等前代模型技術脈絡，當前披露的核心規格如下：
網友評論
參考：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/discussions
https://deepseeksai.com/prover-v2-671b/