深度求索AI宣布发布DeepSeek-Prover-V2，这是一个专为Lean 4环境中的形式定理证明设计的开源大语言模型。该最新版本基于先前工作，引入了创新的递归定理证明流程，利用DeepSeek-V3生成自身高质量初始化数据。由此产生的模型在神经定理证明中实现了领先性能，并伴随着ProverBench的推出，这是一个用于评估数学推理能力的新基准。
DeepSeek-Prover-V2的一个关键创新在于其独特的冷启动训练过程。这个过程始于提示强大的DeepSeek-V3模型将复杂数学定理分解为一系列更易管理的子目标。同时，DeepSeek-V3在Lean 4中形式化这些高级证明步骤，有效创建了结构化子问题序列。为了处理每个子目标的计算密集型证明搜索，研究人员使用了一个较小的7B参数模型。一旦一个挑战性问题的所有分解步骤被成功证明，完整的逐步形式证明与DeepSeek-V3相应的思维链推理配对。这种方法允许模型从综合数据集中学习，该数据集整合了非正式的高级数学推理和严格的形式证明，为后续强化学习提供了强大的冷启动。
在合成冷启动数据的基础上，深度求索团队精选了一系列挑战性问题，这些问题是7B证明模型无法端到端解决的，但所有子目标已成功处理。通过组合这些子目标的形式证明，构建了原始问题的完整证明。这个形式证明然后与DeepSeek-V3概述引理分解的思维链链接，创建了非正式推理后形式化的统一训练示例。证明模型然后在这个合成数据上进行微调，接着是强化学习阶段。这个阶段利用二元正确或错误反馈作为奖励信号，进一步优化模型在非正式数学直觉和形式证明精确构建之间弥合差距的能力。
这个创新训练过程的成果是DeepSeek-Prover-V2–671B，一个拥有6710亿参数的模型。该模型取得了显著成果，在神经定理证明中展示了领先性能。它在MiniF2F-test上达到了88.9%的通过率，并成功解决了PutnamBench中658个问题中的49个。DeepSeek-Prover-V2为miniF2F数据集生成的证明可供公开下载，允许进一步审查和分析。
除了模型发布，深度求索AI还推出了ProverBench，这是一个包含325个问题的新基准数据集。该基准旨在更全面地评估不同难度级别的数学推理能力。ProverBench包括15个从最近AIME竞赛形式化的问题，提供高中竞赛级别的真实挑战。其余310个问题来自精选的教科书示例和教育教程，提供了跨越不同领域的多样化和教育性强的形式化数学问题集合。ProverBench旨在促进更全面的评估。