DeepSeek-Prover-V2

Source | HN Comments

DeepSeek-Prover-V2 是一个开源大型语言模型，专为 Lean 4 形式化定理证明设计。它利用 DeepSeek-V3 进行子目标分解，通过递归定理证明流程生成冷启动数据，结合思维链和强化学习，将非形式化与形式化数学推理相结合。该模型在神经定理证明中表现出色，并在 MiniF2F-test 和 PutnamBench 上取得了显著成果。文章还介绍了 ProverBench 数据集，并提供了模型和数据集的下载链接及使用示例。

DeepSeek-Prover-V2：通过强化学习进行子目标分解，推进形式化数学推理

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 个问题来自精选的教科书示例和教育教程，贡献了一个多样化且具有教学基础的形式化数学问题集合。该基准旨在对高中竞赛问题和本科数学进行更全面的评估。

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

4. 模型 & 数据集下载

我们发布了两种模型大小的 DeepSeek-Prover-V2：7B 和 671B 参数。 DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 之上训练的。 DeepSeek-Prover-V2-7B 构建于 DeepSeek-Prover-V1.5-Base 之上，并具有高达 32K tokens 的扩展上下文长度。

| Model | Download | | ----------------------- | ----------------------------------------------------------------------------------------------------------------- | | DeepSeek-Prover-V2-7B | 🤗 HuggingFace | | DeepSeek-Prover-V2-671B | 🤗 HuggingFace |

| Dataset | Download | | -------------------- | ------------------------------------------------------------------------------------------------------------- | | DeepSeek-ProverBench | 🤗 HuggingFace |

5. 快速开始

您可以直接使用 Huggingface's 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 模型的使用受 [模型许可](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/LICENSE-MODEL) 的约束。

## 7. 联系方式

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