DeepSeek AI 團隊於 2025 年 4 月 30 日正式發佈 DeepSeek-Prover-V2-671B，一款專為數學定理證明打造的超大規模開源人工智能模型。該模型在運算效率與邏輯推理能力上均實現重大突破，甚至可在單張 NVIDIA 4090 顯卡上實現流暢運行，為科研與工程領域提供嶄新的自動化證明工具。
數學定理的 AI 專家
DeepSeek-Prover-V2-671B 擁有高達 6710 億參數的龐大架構，定位為形式化數學領域的專家級人工智能系統。透過混合專家（Mixture of Experts, MoE）架構與多任務注意力機制，該模型能根據問題領域動態啟用對應“數學專家模組”，有效處理高階抽象邏輯與演繹推理。其設計也可能結合了檢索增強生成（RAG）技術，以整合外部數學知識庫如 Lean 4、Isabelle 等形式化資料來源。
精準又高效的推理性能
與通用大型模型如 DeepSeek 70B 相比，DeepSeek 671B 在數學推理任務中的表現更加出色。其推理結果不僅準確，還能滿足形式化驗證需求，特別是在抽象代數、拓撲學等高深數學問題中表現尤為穩定。同時，該模型推測具備長文本處理能力，可支持最高 128K token 的上下文長度，能應對證明任務中冗長的邏輯鏈與前提描述。
應用橫跨學術與產業
DeepSeek 671B 的應用潛力廣泛。對科研工作者而言，它能協助完成猜想驗證與理論發現；在教育場域，則能用於生成教學案例或自動檢查學生證明過程的邏輯嚴謹性；於產業界，如晶片設計與密碼學等領域，則可輔助形式化驗證流程，降低錯誤率、提升開發安全性。
部署門檻大幅降低
該模型已於 Hugging Face 正式開源，並支援學術與商業用途。最令人矚目的是其部署效率：透過清華大學開發的 kTransformers 框架與 CPU-GPU 混合架構，開發者僅需單張 NVIDIA 4090 顯卡即可運行，無需昂貴的多卡 H100 集群，記憶體使用率降低 93.3%，吞吐量提升達 5.76 倍，為各類規模的團隊提供更靈活的部署選擇。
技術創新再下一城
DeepSeek 671B 的高效運作亦得益於多項底層創新，包括多頭潛在注意力（MLA）機制以壓縮鍵值緩存空間，與利用 GRPO 強化學習演算法對齊人類推理偏好。此外，其訓練數據涵蓋高品質的形式化數學資料庫，進一步提升模型對專業證明邏輯的理解與表達能力。
