近日，AI 开源社区 Hugging Face 迎来了一项新成果，深度求索（DeepSeek）团队发布了名为 DeepSeek-Prover-V2-671B 的大型语言模型。与此同时，该团队还在 GitHub 等平台分享了相关论文，详细介绍了这一新模型的特性和成就。
DeepSeek-Prover-V2 是一款专注于形式化数学推理的开源模型，其基础是 DeepSeek-V3-0324。为了生成训练所需的初始数据，团队采用了递归定理证明管道的方法。这一创新使得模型在处理复杂数学问题时，能够展现出更高的精确度和效率。
DeepSeek 团队推出了两个版本的模型：DeepSeek-Prover-V2-671B 和 DeepSeek-Prover-V2-7B。前者结合了 V3 基础大模型的优点，后者则是一个增强模型。团队还发布了 DeepSeek-ProverBench 数据集，为评估模型性能提供了有力工具。
DeepSeek-Prover-V2-671B 的架构与 DeepSeek V3-0324 相同，但其应用场景却大相径庭。这款模型并非用于常规对话或推理，而是专注于形式化定理证明，专门增强了数学能力。为了实现这一目标，团队采用了复杂的策略。
首先，他们引导 DeepSeek-V3 模型将复杂的数学定理分解为一系列子目标。这一步骤整合了非形式化与形式化数学推理，使得模型能够在 Lean 4 平台上逐步完成形式化证明。接着，团队利用一个较小的 7B 参数模型来处理这些子目标的证明搜索，从而大大减轻了计算负担。
在训练过程中，团队精心筛选了一批难题，这些难题虽然 7B 模型无法直接解决，但其子目标已被证明。通过整合这些子目标的证明，团队形成了完整的形式化证明，并与 DeepSeek-V3 的推理过程对接，生成了丰富的合成数据。这些数据为模型的微调提供了坚实的基础。
随后，团队利用强化学习进一步提升模型的能力。他们以二元反馈（正确或错误）作为奖励机制，通过不断的试错和优化，使得 DeepSeek-Prover-V2-671B 在神经定理证明领域取得了显著进展。在 MiniF2F-test 数据集上，该模型的通过率达到了 88.9%，在 PutnamBench 数据集中也成功解决了 49 个问题。
为了推动模型在多样化场景下的测试与应用，DeepSeek 团队还发布了 ProverBench 基准数据集。该数据集包含了 325 个形式化数学问题，其中 15 个问题源自近期的 AIME 竞赛，涉及数论与代数等高中竞赛难度的内容。其余 310 个问题则涵盖了线性代数、微积分、概率等多个领域，为高中竞赛和本科数学提供了全面的评估标准。
