🚀 DeepSeek-Prover-V2

DeepSeek-Prover-V2 是一个用于 Lean 4 形式定理证明的开源大语言模型。它借助由 DeepSeek-V3 驱动的递归定理证明管道收集初始化数据，将非正式和正式的数学推理集成到统一模型中，在神经定理证明领域取得了卓越的性能。

🚀 快速开始

你可以直接使用 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)

## ✨ 主要特性
### 合成冷启动推理数据
- **递归证明搜索管道**：为构建冷启动数据集，开发了一个简单而有效的递归定理证明管道，利用 DeepSeek-V3 作为子目标分解和形式化的统一工具。通过提示 DeepSeek-V3 将定理分解为高级证明草图，并同时在 Lean 4 中形式化这些证明步骤，得到一系列子目标。
- **减轻计算负担**：使用较小的 7B 模型处理每个子目标的证明搜索，降低了计算负担。当一个具有挑战性的问题的分解步骤得到解决后，将完整的逐步形式证明与 DeepSeek-V3 对应的思维链配对，创建冷启动推理数据。

### 合成冷启动数据的强化学习
- **构建完整证明**：精心挑选了一组具有挑战性的问题，这些问题无法由 7B 证明器模型以端到端的方式解决，但所有分解的子目标都已成功解决。通过组合所有子目标的证明，为原始问题构建一个完整的形式证明。然后将此证明附加到 DeepSeek-V3 的思维链上，该思维链概述了相应的引理分解，从而产生非正式推理和后续形式化的连贯合成。
- **强化学习提升性能**：在合成冷启动数据上微调证明器模型后，进行强化学习阶段，以进一步增强其将非正式推理与形式证明构建相衔接的能力。遵循推理模型的标准训练目标，使用二元正确或错误反馈作为主要的奖励监督形式。
- **卓越的性能表现**：最终得到的模型 DeepSeek-Prover-V2-671B 在神经定理证明中达到了最先进的性能，在 MiniF2F 测试中达到了 $88.9$% 的通过率，并解决了 PutnamBench 中 658 个问题中的 49 个。DeepSeek-Prover-V2 为 miniF2F 数据集生成的证明可以作为 [ZIP 存档](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip) 下载。

## 📦 安装指南
文档未提及安装步骤，故跳过此章节。

## 💻 使用示例
### 基础用法
```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)

### 高级用法
文档未提及高级用法相关代码示例，故跳过此部分。

## 📚 详细文档
### ProverBench：AIME 和教科书问题的形式化
我们引入了 ProverBench，这是一个包含 325 个问题的基准数据集。其中，15 个问题是从最近的 AIME 竞赛（AIME 24 和 25）中的数论和代数问题形式化而来，提供了真实的高中竞赛级别的挑战。其余 310 个问题来自精心挑选的教科书示例和教育教程，构成了一个多样化且具有教学基础的形式化数学问题集合。这个基准旨在能够对高中竞赛问题和本科水平的数学进行更全面的评估。

<div align="center">

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

</div>

### 模型与数据集下载
我们发布了两种模型大小的 DeepSeek-Prover-V2：7B 和 671B 参数。DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 上进行训练的。DeepSeek-Prover-V2-7B 基于 DeepSeek-Prover-V1.5-Base 构建，并具有长达 32K 标记的扩展上下文长度。

<div align="center">

| **模型** | **下载地址** |
| ---- | ---- |
| 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">

| **数据集** | **下载地址** |
| ---- | ---- |
| DeepSeek-ProverBench | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |

</div>

## 🔧 技术细节
文档未提及技术实现细节相关内容，故跳过此章节。

## 📄 许可证
使用 DeepSeek-Prover-V2 模型需遵循 [模型许可证](LICENSE-MODEL)。

## 📞 联系我们
如果您有任何问题，请提出问题或通过 [service@deepseek.com](mailto:service@deepseek.com) 与我们联系。