DeepSeek-Prover-V2：数学定理证明领域的新突破

前言

在人工智能飞速发展的当下，模型的迭代与创新层出不穷。

五一假期期间，DeepSeek 再次发力，推出了令人瞩目的新模型 ——DeepSeek-Prover-V2。

与大众期待的 R2 通用推理模型不同，这次 DeepSeek 将目光聚焦于数学定理证明领域，旨在利用先进的人工智能技术，为数学研究与教育提供强大助力。

聚焦数学定理证明

DeepSeek-Prover-V2 主打 formal theorem proving in Lean 4，简单来说，就是进行数学定理的证明。

那么，人类是如何证明数学定理的呢？当面对复杂困难的证明题目时，通常会将其分解为多个逻辑严密的步骤，然后逐一验证每个步骤的正确性，这便是常用的 step-by-step 方式。

通过这样的方式，DeepSeek-Prover-V2 致力于在数学定理证明方面实现高效且准确的运算。

多维度技术创新

高质量的模型离不开高质量的数据支持。对于数据证明题这类专业程度极高的数据，如果完全依靠人工标注，成本将高得难以承受。

DeepSeek 官方采用了 Synthesize Cold-Start Reasoning Data through Recursive Proof Search 的方法。

即使用 V3 将复杂问题分解成自然语言形式的草稿，同时在 Lean 4 中将这些证明步骤形式化，从而产生一系列子目标。

为了减轻计算负担，团队使用较小的 7B 模型来处理每个子目标的证明搜索。

一旦具有挑战性的问题的分解步骤得到解决，就将完整的逐步形式化证明与 DeepSeek-V3 产生的相应思维链过程相结合，生成冷启动推理数据。

简单来说，V3 对原论点进行分解，转化为多个步骤，同时转化为标准的 Lean 4 proof 结构，然后用 7B 的模型证明每个步骤，最终形成用于训练的冷启动数据集。

双模式训练

在完成数据合成后，便进入了训练阶段。DeepSeek-Prover-V2 采用了两种不同的训练模式：

High-efficiency non-Chain-of-Thought (non-CoT) mode：该模式针对快速生成正式的 Lean 证明代码进行了优化，专注于在不显示中间推理步骤的情况下生成简洁证明，因此速度较快，能够有效加速迭代训练和数据收集过程。

模型能力的进一步提升则依赖后续的 SFT 和 RL，这里采用的是 expert iteration 的范式。

在每次训练迭代中，当前最佳的证明策略用于为那些在前几次迭代中仍未解决的具有挑战性的问题生成证明尝试。

那些经 Lean 证明助手验证成功的尝试将被纳入 SFT 数据集，以训练改进后的模型。通过这种迭代循环，模型不仅能够从初始演示数据集中学习，还能提炼自身经验，不断优化。

High-precision Chain-of-Thought (CoT) mode：这是大家较为熟悉的 COT 模式，它会系统地阐述中间推理步骤，强调推理过程的透明度和逻辑连贯性，在构建最终的正式证明之前，逐步清晰地展示推理思路，从而生成精确的推理过程 。

模型性能

此次 DeepSeek-Prover-V2 提供了两种模型尺寸：7B 和 671B 参数。

其中，DeepSeek-Prover-V2-671B 在 DeepSeek-V3-Base 基础上训练，展现出最强的推理性能；DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，上下文长度扩展至高达 32K token。

技术报告显示，DeepSeek-Prover-V2 在神经定理证明方面取得了当前最优的性能。

在 MiniF2F-test 上，DeepSeek-Prover-V2-671B 达到了 88.9% 的通过率，并解决了 PutnamBench 中 658 个问题中的 49 个。

在包含 325 道题目的 ProverBench 基准数据集上，该模型也有出色表现，其中 15 道题目源自最近 AIME 竞赛（AIME 24&25）中的数论和代数题目，代表了极具挑战性的高中竞赛级别题目，剩余 310 道题目来自精选的教科书例题和教学教程，构建了一个多样化的、具有教学意义的形式化数学题目集合，全面评估了高中竞赛和本科阶段的数学水平。

结语

DeepSeek-Prover-V2 的发布，为数学定理证明领域注入了新的活力。

它在模型构建、数据处理以及训练方式上的创新，为后续相关模型的发展提供了宝贵的借鉴经验。