当前位置：首页 > ai >正文

最新DeepSeek-Prover-V2-671B模型简介、下载、体验、微调、数据集：专为数学定理自动证明设计的超大垂直领域语言模型（在线体验地址）

ai 2025/5/3 16:26:47

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

四、数据集资源

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)