DeepSeek发布DeepSeek-Prover-V2：利用递归证明搜索和新基准推进神经定理证明

DeepSeek AI宣布发布DeepSeek-Prover-V2，这是一个专为Lean 4环境中的形式定理证明设计的开源大型语言模型。该模型基于先前工作，引入了一种创新的递归定理证明管道，利用DeepSeek-V3生成高质量的初始化数据。最终模型在神经定理证明中达到了最先进水平，并同时推出了ProverBench，这是一个用于评估数学推理能力的新基准。

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

DeepSeek-Prover-V2的一个关键创新在于其独特的冷启动训练过程。该过程首先提示强大的DeepSeek-V3模型将复杂数学定理分解为一系列更易处理的子目标。同时，DeepSeek-V3在Lean 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包括15个来自最近AIME（美国邀请数学考试）竞赛（AIME 24和25）的形式化问题，提供了高中竞赛级别的真实挑战。其余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系统。