DeepSeek-Prover-V2-671B模型 簡介、下載、體驗、微調、數據集：專為數學定理自動證明設計的超大垂直領域語言模型（在線體驗地址）
體驗地址：[Hugging Face 在線體驗]https://huggingface.co/playground?modelId=deepseek-ai/DeepSeek-Prover-V2-671B&provider=novita
推薦入口：[Novita 平臺直達鏈接（含邀請碼）]https://novita.ai/referral?invited_code=A43LMN
一、模型簡介
DeepSeek-Prover-V2-671B 是 DeepSeek 團隊于 2025 年發布的超大規模開源語言模型，專為 Lean 4 環境下的數學定理自動證明任務設計。該模型采用深度鏈式思維（Chain-of-Thought）結合形式化推理訓練，成功將“人類直覺式證明”與“嚴謹符號邏輯”結合，開啟了 AI 數學證明的新階段。
本模型構建在 DeepSeek-V3 架構基礎之上，支持超長上下文輸入，并在多個數學證明權威基準測試中創下 SOTA 表現。
二、模型亮點與技術創新
1. 冷啟動數據構建：遞歸證明生成流程
- 利用 DeepSeek-V3 將復雜定理拆分為子目標；
- 使用小模型（7B）依次完成子目標 Lean 4 證明；
- 將子目標整合為完整定理證明，并保留推理鏈（CoT）；
2. 強化學習：形式+非形式聯合訓練
- 將符號證明與自然語言推理串聯；
- 使用“正誤”反饋強化模型推理與形式化能力聯動；
- 顯著提升對競賽題、高階數學題的適應性；
3. SOTA 性能表現
- MiniF2F-Test 集：88.9% 通過率
- PutnamBench：解出 49/658 高難問題
三、模型下載與調用方式
模型文件（兩種規模）
| 模型版本 | 下載鏈接 |
|---|---|
| DeepSeek-Prover-V2-7B | https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B |
| DeepSeek-Prover-V2-671B | https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B |
Hugging Face 直接體驗入口
https://huggingface.co/playground?modelId=deepseek-ai/DeepSeek-Prover-V2-671B&provider=novita
推薦體驗平臺（Novita）
https://novita.ai/referral?invited_code=A43LMN
四、數據集資源
ProverBench：325題專業數學題集
該評測集包含來自 AIME 數學競賽、高校教材、分析代數等不同領域的題目，是目前最系統的數學推理模型評測集之一。
| 領域 | 數量 |
|---|---|
| AIME 24/25 | 15 |
| 微積分/實分析 | 120 |
| 數論/代數 | 110 |
| 概率/復分析 | 20 |
| 抽象代數/泛函分析 | 60 |
下載地址：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
五、使用示例：自動生成 Lean 4 證明代碼
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)model_id = "DeepSeek-Prover-V2-7B" # or DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)formal_statement = """
import Mathlib
import Aesopset_option maxHeartbeats 0open BigOperators Real Nat Topology Rat/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ?) / 100 * 30 - 130 / 100 * 20) = 10 := bysorry
""".strip()prompt = """
Complete the following Lean 4 code:```lean4
{}
/```Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()chat = [{"role": "user", "content": prompt.format(formal_statement)},
]model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)六、模型微調說明（高級用戶）
- 基礎框架：與 DeepSeek-V3 結構兼容；
- 上下文長度支持：最大支持 163K tokens；
- 精度與效率平衡：支持 FP8/BF16 精度加速訓練；
- 推薦場景：Lean 4 高階訓練、大學數學 AI 助教、自動題解平臺等。
七、許可證信息
- 模型代碼：MIT License
- 模型權重：Model License（需遵循使用條款）
詳見：LICENSE-MODEL
八、聯系方式與支持
- GitHub 主頁：https://github.com/deepseek-ai
- 官方郵箱：service@deepseek.com
- 交流群組：Discord / WeChat / HuggingFace Spaces 頁面
如需將本模型部署為企業級數學引擎，或進行專業定制化訓練，請聯系 DeepSeek 團隊獲得商業合作通道。
