DeepSeek ai 于 2025 年 4 月 30 日發布DeepSeek-Prover-V2-671B，這是一款基于 6710 億參數MoE架構的下一代自動定理證明模型，在 Lean 4 框架內生成和驗證證明。其優勢包括將形式數學提升到 “GPT-4 級別” 規模、MoE 帶來的效率提升、開源且允許商業使用。相比 V1.5 版本，它在參數數量、上下文長度、通過率等方面有顯著提升。預計在 miniF2F 等基準測試中表現優異，可用于形式驗證、加速數學研究等領域，使用時需從 Hugging Face 下載權重并完成相關設置。

技術特點

• 參數量與架構：模型總參數量為6710億，采用MoE架構，每token激活約370億參數。這種架構在保持強大推理能力的同時，顯著降低了內存需求。

• 上下文長度：支持超長上下文，最大位置嵌入達163840，能夠處理復雜的數學證明。

• 計算精度：支持BF16、FP8、F32等多種計算精度，方便模型更快、更省資源地訓練和部署。

• 文件格式：使用更高效的safetensors文件格式。

• 量化技術：采用FP8量化，通過量化技術減小模型大小，提高推理效率。

關鍵優勢

• 規模與復雜性：巨大的參數量和長上下文窗口（約128k tokens），能夠處理更長、更復雜的數學證明邏輯鏈。

• 效率優化：采用MoE架構，相比全連接的6710億參數模型，顯著降低了內存需求并提升了推理速度。

• 開源與許可：模型開源，權重可在Hugging Face上獲取，且預計允許商業使用。

應用場景

• 形式化驗證：在密碼學安全性證明或芯片設計正確性證明中進行嚴格檢查。

• 加速數學研究：幫助數學家形式化現有定理、探索新猜想，并解決奧林匹克級別的數學問題。

• 高級教育工具：創建交互式輔導系統，指導學生完成形式化證明。

• 安全關鍵系統：在代碼部署前，通過Lean集成驗證關鍵軟件屬性和不變量。

快速入門步驟

1. 獲取模型：從Hugging Face下載權重：deepseek-ai/DeepSeek-Prover-V2-671B。

2. 設置Lean：安裝Lean 4（建議≥4.5版本）和mathlib4庫。

3. 驗證硬件：確保硬件配置滿足最低要求（建議使用高性能配置）。

4. 安裝推理引擎：設置如vLLM或其他兼容MoE的框架。

5. 探索示例：檢查模型倉庫中的評估腳本或示例筆記本。

常見問題

是否開源？是否可用于商業用途？

是的，DeepSeek-Prover-V2-671B是開源的（可在Hugging Face上獲取權重），并且預計其許可協議允許學術和商業用途。

能否在NVIDIA 4090上運行？

初步報告稱，由于采用了MoE、MLA和量化等優化技術，該模型可以在單個NVIDIA 4090 GPU上運行，尤其是搭配足夠的RAM和快速NVMe SSD進行動態加載時。性能會因具體配置而異。

相關鏈接

Hugging Face：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Github：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

詳細介紹：https://deepseeksai.com/prover-v2-671b/

論文：https://arxiv.org/pdf/2408.08152