DeepSeek-ProverBench

**Synthesize Cold-Start Reasoning Data through Recursive Proof Search**

- To construct the cold-start dataset, we develop a simple yet effective pipeline for recursive theorem proving, utilizing DeepSeek-V3 as a unified tool for both subgoal decomposition and formalization. We prompt DeepSeek-V3 to decompose theorems into high-level proof sketches while simultaneously formalizing these proof steps in Lean 4, resulting in a sequence of subgoals.

- We use a smaller 7B model to handle the proof search for each subgoal, thereby reducing the associated computational burden. Once the decomposed steps of a challenging problem are resolved, we pair the complete step-by-step formal proof with the corresponding chain-of-thought from DeepSeek-V3 to create cold-start reasoning data.

---

**Reinforcement Learning with Synthetic Cold-Start Data**

- We curate a subset of challenging problems that remain unsolved by the 7B prover model in an end-to-end manner, but for which all decomposed subgoals have been successfully resolved. By composing the proofs of all subgoals, we construct a complete formal proof for the original problem. This proof is then appended to DeepSeek-V3's chain-of-thought, which outlines the corresponding lemma decomposition, thereby producing a cohesive synthesis of informal reasoning and subsequent formalization.

- After fine-tuning the prover model on the synthetic cold-start data, we perform a reinforcement learning stage to further enhance its ability to bridge informal reasoning with formal proof construction. Following the standard training objective for reasoning models, we use binary correct-or-incorrect feedback as the primary form of reward supervision.
- The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching $88.9$% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. The proofs generated by DeepSeek-Prover-V2 for the miniF2F dataset are available for download as a [ZIP archive](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip).

---

## 3. ProverBench: Formalization of AIME and Textbook Problems

we introduce ProverBench, a benchmark dataset comprising 325 problems. Of these, 15 are formalized from number theory and algebra questions featured in the recent AIME competitions (AIME 24 and 25), offering authentic high-school competition-level challenges. The remaining 310 problems are drawn from curated textbook examples and educational tutorials, contributing a diverse and pedagogically grounded collection of formalized mathematical problems. This benchmark is designed to enable more comprehensive evaluation across both high-school competition problems and undergraduate-level mathematics.

<div align="center">

| 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 |

</div>

## 4. Model & Dataset Downloads

We release DeepSeek-Prover-V2 in two model sizes: 7B and 671B parameters. DeepSeek-Prover-V2-671B is trained on top of DeepSeek-V3-Base. DeepSeek-Prover-V2-7B is built upon DeepSeek-Prover-V1.5-Base and features an extended context length of up to 32K tokens.

<div align="center">

| **Model** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-Prover-V2-7B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |
| DeepSeek-Prover-V2-671B | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |

</div>

<div align="center">

| **Dataset** | **Download** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |

</div>

## 5. Quick Start

You can directly use [Huggingface's Transformers](https://github.com/huggingface/transformers) for model inference. DeepSeek-Prover-V2-671B shares the same architecture as DeepSeek-V3. For detailed information and supported features, please refer to [the DeepSeek-V3 documentation on Hugging Face](https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md).

The following is a basic example of generating a proof for a problem from the miniF2F dataset:
````python
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. License
The use of DeepSeek-Prover-V2 models is subject to [the Model License](LICENSE-MODEL).

## 7. Contact

If you have any questions, please raise an issue or contact us at [[e-mail]](mailto:[e-mail]).

**通过递归证明搜索合成冷启动（cold-start）推理数据集**

- 为构建冷启动数据集，我们开发了一套简洁高效的递归定理证明（theorem proving）流水线，采用DeepSeek-V3作为统一工具，同时完成子目标分解（subgoal decomposition）与形式化（formalization）工作。我们通过提示DeepSeek-V3将定理拆解为高层级证明概要，同时在Lean 4中将这些证明步骤形式化，最终得到一系列子目标序列。
- 我们使用参数量更小的7B模型来处理每个子目标的证明搜索，从而降低计算开销。当一个复杂问题的分解步骤全部解决后，我们将完整的分步形式化证明与DeepSeek-V3生成的对应思维链（chain-of-thought）相结合，以此构建冷启动推理数据集。

---

**基于合成冷启动数据的强化学习（reinforcement learning）**
- 我们以端到端的方式筛选出一类具有挑战性的问题：这类问题无法被7B定理证明模型（prover model）直接解决，但所有分解后的子目标均已成功求解。通过组合所有子目标的证明，我们为原问题构建出完整的形式化证明。随后将该证明附加到DeepSeek-V3的思维链（即对应的引理分解流程）之后，由此得到非正式推理与形式化证明相结合的连贯合成数据。
- 在基于合成冷启动数据对定理证明模型完成微调后，我们进一步开展强化学习阶段，以提升模型连接非正式推理与形式化证明构建的能力。遵循推理模型的标准训练目标，我们采用二元对错反馈（binary correct-or-incorrect feedback）作为主要的奖励监督形式。
- 最终得到的模型DeepSeek-Prover-V2-671B在神经定理证明领域取得了当前最优（state-of-the-art）性能，在MiniF2F测试集上达到88.9%的通过率（pass ratio），并在普特南基准集（PutnamBench）的658道题目中解决了49道。DeepSeek-Prover-V2为miniF2F数据集生成的证明可通过[ZIP压缩包（ZIP archive）](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip)下载。

---

## 3. ProverBench：AIME与教科书问题的形式化基准
我们推出ProverBench基准数据集，共包含325道题目。其中15道题目来自近期美国数学邀请赛（AIME, American Invitational Mathematics Examination）2024与2025届的数论与代数题，具备真实的高中竞赛级难度。剩余310道题目取自精选的教科书例题与教学教程，形成了一套多样化且符合教育学逻辑的形式化数学问题集合。该基准旨在支持针对高中竞赛题与本科数学内容的更全面评估。

<div align="center">

| 领域 | 题量 |
| :---------------------: | :-------: |
| AIME 24&25 | 15 |
| 数论 | 40 |
| 初等代数 | 30 |
| 线性代数 | 50 |
| 抽象代数 | 40 |
| 微积分 | 90 |
| 实分析 | 30 |
| 复分析 | 10 |
| 泛函分析 | 10 |
| 概率论 | 10 |
| 总计 | 325 |

</div>

## 4. 模型与数据集下载
我们发布了两种参数量版本的DeepSeek-Prover-V2模型：7B与671B。DeepSeek-Prover-V2-671B基于DeepSeek-V3-Base训练得到；DeepSeek-Prover-V2-7B则以DeepSeek-Prover-V1.5-Base为基础，支持最高32K Token（Token）的扩展上下文长度（context length）。

<div align="center">

| **模型** | **下载链接** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-Prover-V2-7B | [🤗 Hugging Face（HuggingFace）](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |
| DeepSeek-Prover-V2-671B | [🤗 Hugging Face（HuggingFace）](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |

</div>

<div align="center">

| **数据集** | **下载链接** |
| :-----------------------------: | :----------------------------------------------------------: |
| DeepSeek-ProverBench | [🤗 Hugging Face（HuggingFace）](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |

</div>

## 5. 快速上手
您可以直接使用[Hugging Face的Transformers库（Transformers）](https://github.com/huggingface/transformers)进行模型推理。DeepSeek-Prover-V2-671B与DeepSeek-V3的架构完全一致。如需了解详细信息与支持功能，请参阅[Hugging Face上的DeepSeek-V3官方文档](https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md)。

以下是针对miniF2F数据集的题目生成证明的基础示例代码：
`python
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B" # 或 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

/-- 求120%的30与130%的20之间的正差值，并证明该差值为10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
sorry
""".strip()

prompt = """
请补全以下Lean 4代码：

lean4
{}

在生成正式的Lean 4形式化证明代码之前，请先提供详细的证明计划，概述主要证明步骤与策略。该计划应阐明核心思路、中间引理与证明结构，以指导最终形式化证明的构建。
""".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模型的使用需遵循[模型许可证（LICENSE-MODEL）](LICENSE-MODEL)。

## 7. 联系方式
如有任何疑问，请提交Issue或发送邮件至[[e-mail]](mailto:[e-mail]).