團隊趕放假，DeepSeek-Prover V2 671B開源發佈

來源——AMP實驗室

幻方量化又做空了

DeepSeek 昨日下午，在 AI 開源社區 Hugging Face 發佈了一個名爲 DeepSeek-Prover-V2-671B 的新模型。

DeepSeek-Prover-V2-671B 使用了更高效的 safetensors 文件格式，並支持 BF16、FP8、F32 等多種計算精度，方便模型更快、更省資源地訓練和部署。

從命名上看，這款參數高達 6710 億的模型可能是去年發佈的數學 AI 模型 Prover-V1.5 的升級版。

DeepSeek-Prover 是由 DeepSeek 團隊開發的開源數學大模型系列，其核心功能是專注於形式化數學定理的自動證明與驗證，尤其是在數學推理的嚴謹性和邏輯性上具有顯著優勢。相較之下，通用模型（如 GPT-4）雖在廣泛任務中表現優異，但缺乏內置驗證機制，難以保證數學證明的精確性。

最新的V2-671B版本則在多個方面實現了突破，其參數量躍升至 6710 億，採用混合專家架構（MoE），每層包含 256 個路由專家和 1 個共享專家，支持動態分配計算資源，顯著提升複雜邏輯的解析效率。

此外，V2-671B引入多頭潛注意力（MLA）架構壓縮鍵值緩存（KV Cache），降低推理內存佔用，結合 FP8 量化技術提升計算效率超 40%，並擴展上下文窗口至 163,840 tokens，覆蓋長證明流程。

最後是算法升級，新V2強化 RMaxTS 算法驅動探索多樣性證明路徑，優化截斷-恢復機制平衡生成與驗證效率，並通過三階段訓練（預訓練、監督微調、強化學習）增強領域適配性，尤其在形式化語言（如 Lean 4）的生成穩定性上表現突出。這些改進使其在學術研究、工業驗證等場景中展現出更強的專業性與實用性。