Deepseek Prover V2 671B GGUF

🚀 DeepSeek-Prover-V2-671B

DeepSeek-Prover-V2-671B是一个专为Lean 4形式定理证明设计的开源大语言模型。它通过递归定理证明管道收集初始化数据，将非正式和正式的数学推理集成到统一模型中，在神经定理证明领域达到了先进水平。

🚀 快速开始

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

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

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

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

## 💻 使用示例
### 基础用法
以下是为miniF2F数据集中的问题生成证明的基本示例：
```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)

### 高级用法
文档未提及高级用法示例，故跳过该部分。

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

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

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

## 🔧 技术细节
### 合成冷启动推理数据的递归证明搜索
- 为构建冷启动数据集，我们开发了一个简单而有效的递归定理证明管道，利用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) 下载。

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

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

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