1. 简介

我们推出 DeepSeek-Prover-V2，这是一款专为 Lean 4 形式化定理证明设计的开源大语言模型，其初始数据通过由 DeepSeek-V3 驱动的递归定理证明流程收集。冷启动训练流程始于引导 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决的子目标证明被合成为思维链，结合 DeepSeek-V3 的逐步推理，为强化学习创建初始冷启动。这一过程使我们能够将非形式化与形式化的数学推理统一整合到单一模型中。

2. 模型概览

通过递归证明搜索合成冷启动推理数据

• 为构建冷启动数据集，我们开发了一个简单高效的递归定理证明流程，利用 DeepSeek-V3 作为子目标分解与形式化的统一工具。我们引导 DeepSeek-V3 将定理分解为高层证明框架，同时在 Lean 4 中形式化这些证明步骤，生成一系列子目标。

• 我们使用较小的 7B 模型处理每个子目标的证明搜索，从而降低计算负担。当复杂问题的分解步骤被解决后，我们将完整的逐步形式化证明与 DeepSeek-V3 的对应思维链配对，创建冷启动推理数据。

基于合成冷启动数据的强化学习

• 我们筛选出一批具有挑战性的问题，这些问题未被 7B 证明模型端到端解决，但其所有分解子目标均已成功验证。通过组合所有子目标的证明，我们为原始问题构建完整的形式化证明。该证明随后与 DeepSeek-V3 描述引理分解的思维链结合，形成非形式化推理与后续形式化的有机合成。

• 在冷启动数据上微调证明模型后，我们进行强化学习阶段以进一步提升其连接非形式化推理与形式化证明构建的能力。遵循推理模型的标准训练目标，我们使用二元正确/错误反馈作为主要的奖励监督形式。

• 最终模型 DeepSeek-Prover-V2-671B 在神经定理证明领域达到最先进性能，在 MiniF2F-test 上通过率达 88.9%，并解决 PutnamBench 658 道问题中的 49 道。DeepSeek-Prover-V2 为 miniF2F 数据集生成的证明可下载为 ZIP 压缩包。

3. ProverBench：AIME 与教材问题的形式化

我们推出 ProverBench 基准数据集，包含 325 道问题。其中 15 道来自近期 AIME 竞赛（AIME 24 和 25）的数论与代数题目，提供真实的高中竞赛级挑战。其余 310 道问题选自教材案例与教学教程，构成多样且具有教学基础的形式化数学问题集合。该基准旨在实现对高中竞赛题与本科数学问题的更全面评估。

4. 模型与数据集下载

我们发布两个参数规模的 DeepSeek-Prover-V2 模型：7B 和 671B。DeepSeek-Prover-V2-671B 基于 DeepSeek-V3-Base 训练。DeepSeek-Prover-V2-7B 基于 DeepSeek-Prover-V1.5-Base，并扩展上下文长度至 32K token。

5. 快速开始

您可以直接使用 Huggingface 的 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 Aesop

set_option maxHeartbeats 0

open 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 := by
  sorry
""".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)

6. 许可协议

DeepSeek-Prover-V2 模型的使用需遵守 模型许可协议。

7. 联系我们

如有任何疑问，请提交 issue 或通过邮件 service@deepseek.com 与我们联系。