继V1.5之后，幻方又发布了 DeepSeek-Prover-V2-671B，参数提升100倍
我们介绍了 DeepSeek-Prover-V2，这是一个开源的大型语言模型，专为精益 4 中的形式定理证明而设计，其初始化数据是通过 DeepSeek-V3 支持的递归定理证明流水线收集的。冷启动训练程序首先会提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决的子目标的证明被合成为一个思维链过程，与 DeepSeek-V3 的逐步推理相结合，为强化学习创建一个初始冷启动。这一过程使我们能够将非正式和正式的数学推理整合到一个统一的模型中。
通过递归证明搜索合成冷启动推理数据
-
为了构建冷启动数据集，我们利用 DeepSeek-V3 作为子目标分解和形式化的统一工具，开发了一个简单而有效的递归定理证明流水线。我们促使DeepSeek-V3将定理分解为高级证明草图，同时在Lean 4中将这些证明步骤形式化，从而形成子目标序列。
-
我们使用较小的 7B 模型来处理每个子目标的证明搜索，从而减少相关的计算负担。一旦挑战性问题的分解步骤得到解决，我们就会将完整的分步形式化证明与 DeepSeek-V3 中相应的思维链配对，从而创建冷启动推理数据。
使用合成冷启动数据进行强化学习
-
我们将 7B 验证器模型仍未以端到端方式解决，但所有分解子目标都已成功解决的挑战性问题子集整理出来。通过组合所有子目标的证明，我们为原始问题构建了一个完整的形式化证明。然后，这个证明会被附加到 DeepSeek-V3 的思维链中，而 DeepSeek-V3 的思维链会概述相应的 Lemma 分解，从而产生一个非正式推理和后续形式化的内聚综合体。
-
在合成冷启动数据上对证明者模型进行微调后，我们执行了强化学习阶段，以进一步增强其连接非正式推理和正式证明构建的能力。按照推理模型的标准训练目标，我们使用二进制正确或不正确反馈作为奖励监督的主要形式。
-
由此产生的 DeepSeek-Prover-V2-671B 模型在神经定理证明方面达到了最先进的性能，在 MiniF2F 测试中达到 88.9 88.9 88.9MiniF2F测试的通过率为100%，解决了PutnamBench 658个问题中的49个。DeepSeek-Prover-V2 针对 miniF2F 数据集生成的证明以 ZIP 压缩包的形式提供下载。
ProverBench: AIME 的形式化和教科书问题
我们介绍 ProverBench，这是一个由 325 个问题组成的基准数据集。其中，15 个问题是根据最近的 AIME 竞赛（AIME 24 和 25）中的数论和代数问题形式化的，提供了真实的高中竞赛级挑战。其余的 310 个问题来自课本例题和教学教程，是一个形式化数学问题的多样化和教学化集合。该基准旨在对高中竞赛问题和本科生数学水平进行更全面的评估。
| Area | Count |
|---|---|
| AIME 24&25 | 15 |
| Number Theory | 40 |
| Elementary Algebra | 30 |
| Linear Algebra | 50 |
| Abstract Algebra | 40 |
| Calculus | 90 |
| Real Analysis | 30 |
| Complex Analysis | 10 |
| Functional Analysis | 10 |
| Probability | 10 |
| Total | 325 |
模型和数据集下载
我们发布了两种规模的 DeepSeek-Prover-V2 模型：7B和671B参数。DeepSeek-Prover-V2-671B是在DeepSeek-V3-Base基础上训练的。DeepSeek-Prover-V2-7B是在DeepSeek-Prover-V1.5-Base基础上构建的，其特点是上下文长度可扩展至32K token。
| 模型 | 下载 |
|---|---|
| DeepSeek-Prover-V2-7B | 🤗 HuggingFace |
| DeepSeek-Prover-V2-671B | 🤗 HuggingFace |
| 模型 | 下载 |
|---|---|
| DeepSeek-ProverBench | 🤗 HuggingFace |
快速启动
您可以直接使用Huggingface’s Transformers进行模型推理。DeepSeek-Prover-V2-671B与DeepSeek-V3采用相同的架构。有关详细信息和支持的功能，请参阅Hugging Face 上的 DeepSeek-V3 文档。
下面是一个从 miniF2F 数据集生成问题证明的基本示例：
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)