DeepSeek-Prover-V2

背景：让AI学会做数学证明题——一个困扰学界数十年的难题

想象一下，你让一个聪明的大学生证明一道数学定理。他会先理解题意，然后在大脑里构思证明思路，最后把每一步逻辑严谨地写下来。这对人类来说需要多年训练，对AI来说更是难上加难。

数学定理证明之所以困难，在于它要求严格的形式化推理——每一步推导都必须有据可查、逻辑自洽，不能有丝毫模糊。传统的神经网络擅长模式识别和概率生成，但在这种需要精确逻辑链的任务上表现不佳。这就是神经定理证明（Neural Theorem Proving）成为AI研究前沿的原因。

DeepSeek-Prover-V2 是 DeepSeek 团队在这个方向上的最新突破。这个开源模型专门针对 Lean 4 这一形式化数学证明语言进行训练，能够将非形式化的数学推理与形式化的证明构建统一在同一个模型中。

图1：DeepSeek-Prover-V2 在 MiniF2F-test 数据集上的性能对比

一、技术突破：从冷启动到强化学习的两阶段训练

1.1 递归式证明搜索：冷启动数据合成

DeepSeek 团队设计了一套巧妙的递归定理证明管道来生成训练数据。核心思路是利用 DeepSeek-V3 作为总指挥，将复杂的数学问题分解为一系列子目标（subgoal）。

具体流程是：先用 DeepSeek-V3 将一道难题拆解成若干中间步骤，这些步骤对应 Lean 4 中的引理（lemma）。然后，用一个较小的 7B 模型分别去证明每个子目标。一旦所有子目标都被解决，就把完整的证明链与 DeepSeek-V3 的思维链结合起来，形成冷启动训练数据。

这种方法的好处是：既利用了大模型的规划与分解能力，又通过小模型降低了计算开销。整个数据合成过程不需要人工标注，纯靠模型自动化完成。

1.2 强化学习：从冷启动到泛化

在冷启动数据上微调之后，团队进一步引入了强化学习（RL）阶段，使用二元反馈（证明正确/错误）作为奖励信号。这与标准推理模型的训练目标一致，目的是增强模型在非形式化推理与形式化证明构建之间建立桥梁的能力。

最终产出的 DeepSeek-Prover-V2-671B 建立在 DeepSeek-V3-Base 之上，DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base，并支持最高 32K 的上下文长度。

二、核心能力：两个模型规模，多个基准测试

2.1 基准测试成绩

DeepSeek-Prover-V2 在多个权威基准上展现了 SOTA（当前最优）性能：

• MiniF2F-test：通过率达到 88.9%，显著超越此前的开源方法。MiniF2F 是形式化数学证明领域最常用的基准之一，涵盖初等代数、数论等多个领域。
• PutnamBench：在包含 658 道题的 Putnam 数学竞赛题上成功解决了 49 道，这是该基准上有记录以来最高的自动化解决率之一。
• ProverBench：团队自建的基准数据集，包含 325 道题目，其中 15 道来自 AIME 24/25 高中数学竞赛，其余涵盖数论、线性代数、抽象代数、实分析等大学数学内容。

2.2 Lean 4 形式化证明生成

用户只需使用 HuggingFace Transformers 加载模型，输入一段 Lean 4 定理陈述，模型即可自动生成证明代码：

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch

model_id = "DeepSeek-Prover-V2-7B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, device_map="auto", torch_dtype=torch.bfloat16, 
    trust_remote_code=True
)
outputs = model.generate(inputs, max_new_tokens=8192)

模型会先输出详细的证明计划（Proof Plan），阐述主要证明步骤和策略，再生成正式的 Lean 4 证明代码。这种双阶段输出兼顾了推理的可解释性和证明的严谨性。

三、技术架构：为什么 DeepSeek 选择这个方向？

3.1 形式化数学的意义

形式化数学不仅让证明可以被机器验证，还能推动数学知识的数字化、可复用化和自动化。Lean 4 作为一种现代证明助手语言，已被广泛应用于数学研究、软件验证和AI安全领域。

DeepSeek-Prover-V2 的意义在于：让开源社区也能用上接近闭源前沿水平的自动定理证明工具。此前，该领域主要由微软 Research 的 LeanDojo 等项目主导，而 DeepSeek 通过开源模型权重和 ProverBench 数据集进一步降低了研究门槛。

3.2 子目标分解策略的启发性

递归证明搜索中的子目标分解策略，与人类数学家处理复杂问题的思维方式高度一致：将一个大问题拆解为多个可管理的小问题，逐个击破后组合成完整证明。这种策略在 AlphaProof（Google DeepMind）中也得到了应用，DeepSeek 的方法在理念上与之呼应，但在实现上更侧重于冷启动数据的自动化合成。

四、适用人群与上手门槛

适合使用的群体：

• 数学研究者：验证猜想、探索引理、建立证明
• 形式化数学爱好者：学习 Lean 4 证明语言和自动化证明技术
• AI/ML 研究者：基于开源模型进行定理证明方向的研究和二次开发
• 计算机科学学生：理解形式化方法和证明助手的实际应用

硬件门槛：

• 7B 模型：需要约 16GB GPU 显存（如一张 A100 40GB 或 RTX 3090），32GB+ 系统内存，14GB 磁盘空间
• 671B 模型：需要约 1400GB GPU 显存（需要多卡集群），512GB+ 系统内存，1.4TB 磁盘空间

纯 CPU 推理在合理时间内几乎不可行，强化学习训练则需要更大规模的计算资源。

五、局限性与挑战

尽管 DeepSeek-Prover-V2 取得了 SOTA 成绩，仍有几点值得注意：

1. 证明成功率仍有提升空间：在 PutnamBench 上，671B 模型仅解决了约 7.4% 的题目，说明复杂数学推理仍是巨大挑战。
2. Lean 4 语言复杂性：生成的证明可能依赖 Mathlib 标准库中大量引理，对没有 Lean 4 基础的用户来说，理解和修改证明有一定门槛。
3. 训练数据来自 DeepSeek-V3：冷启动数据的质量受限于 V3 的能力，若 V3 在某些数学领域存在盲点，可能影响下游证明效果。
4. 模型许可证限制：LICENSE-MODEL 文件中包含模型使用协议，需要仔细阅读合规使用。

六、行业意义与未来展望

DeepSeek-Prover-V2 的开源发布具有三层意义：

第一，它将神经定理证明的能力边界从 Top-of-the-line 大学的专属研究项目，带到了普通研究者的可及范围内。任何人只要有 GPU，就能下载权重进行推理实验。

第二，ProverBench 数据集的发布填补了高中数学竞赛到本科数学的自动化证明评估空白，为后续研究提供了更精细的评测工具。

第三，证明了基于大模型规划加小模型执行证明的递归策略在形式化数学领域的可行性，为后续更高效的冷启动数据合成提供了参考范式。

随着形式化数学工具的成熟，我们有理由期待在未来 5-10 年内，AI 将能够独立完成越来越多的数学研究工作——这不仅是 DeepSeek 的愿景，也是整个 AI for Science 领域的共同方向。