DeepSeek 推出 DeepSeek-Prover-V2：通过递归证明搜索和新基准测试推进神经定理证明

DeepSeek AI 宣布发布 DeepSeek-Prover-V2，这是一个开创性的开源大型语言模型，专为 Lean 4 环境中的形式定理证明而设计。这个最新的迭代建立在以前的工作基础上，引入了一个创新的递归定理证明管道，利用 DeepSeek-V3 的强大功能来生成自己的高质量初始化数据。由此产生的模型在神经定理证明方面取得了最先进的性能，并伴随着 ProverBench 的引入，这是评估数学推理能力的新基准。

开创性冷启动推理数据生成

DeepSeek-Prover-V2 的一个关键创新在于其独特的冷启动训练程序。这个过程首先促使强大的 DeepSeek-V3 模型将复杂的数学定理分解为一系列更易于管理的子目标。同时，DeepSeek-V3 在精益 4 中将这些高级证明步骤形式化，有效地创建了一个结构化的子问题序列。

为了处理每个子目标的计算密集型证明搜索，研究人员采用了较小的 7B 参数模型。一旦一个具有挑战性的问题的所有分解步骤都得到成功证明，完整的逐步形式证明就会与 DeepSeek-V3 的相应思维链推理配对。这种巧妙的方法使模型能够从综合数据集中学习，该数据集集成了非正式的高级数学推理和严格的形式证明，为后续强化学习提供了强大的冷启动。

用于增强推理的强化学习

基于合成的冷启动数据，DeepSeek 团队策划了一系列具有挑战性的问题，这些问题是 7B 验证器模型无法端到端解决的，但所有子目标都已成功解决。通过组合这些子目标的形式证明，构建了原始问题的完整证明。然后，这个形式证明与 DeepSeek-V3 概述引理分解的思维链相关联，创建一个非正式推理后形式化的统一训练示例。

然后，根据这些合成数据对证明者模型进行微调，然后是强化学习阶段。这个阶段利用二进制正确或错误的反馈作为奖励信号，进一步完善了模型弥合非正式数学直觉和形式证明的精确构建之间差距的能力。

最先进的性能

这种创新训练过程的巅峰之作是 DeepSeek-Prover-V2–671B，该模型拥有 6710 亿个参数。该模型取得了显著的成果，展示了神经定理证明的先进性能。它在 MiniF2F 测试中达到了令人印象深刻的 88.9% 通过率，并成功解决了 PutnamBench 的 658 个问题中的 49 个。DeepSeek-Prover-V2 为 miniF2F 数据集生成的证明是公开的，可以进行进一步的审查和分析。

ProverBench 简介：评估新标准

除了模型发布之外，DeepSeek AI 还推出了 ProverBench，这是一个包含 325 个问题的新基准数据集。该基准测试旨在对不同难度级别的数学推理能力进行更全面的评估。

ProverBench 包括从最近的 AIME（美国数学邀请考试）比赛（AIME 24 和 25）中正式确定的 15 个问题，提供高中比赛级别的真实挑战。其余 310 个问题来自精心策划的教科书示例和教育教程，提供了跨越各个领域的多样化且教学合理的形式化数学问题集合：

ProverBench 旨在促进对神经定理证明者在具有挑战性的竞争问题和基础本科水平数学中的更全面评估。

可用性

DeepSeek AI 发布了两种模型大小的 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 的发布和 ProverBench 的推出标志着神经定理证明领域向前迈出了重要一步。通过利用递归证明搜索管道并引入具有挑战性的新基准测试，DeepSeek AI 使社区能够开发和评估更复杂、更强大的形式数学 AI 系统。