library_name: transformers

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测试中达到88.9%的通过率，并解决了PutnamBench中的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令牌的扩展上下文长度。

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"  # 或 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 = """
完成以下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模型的使用受模型许可证约束。

7. 联系我们

如有任何问题，请提交问题或通过service@deepseek.com联系我们。