#AI #大模型 #DeepSeek DeepSeek-Prover-V2 是中国 AI 初创公司 DeepSeek 于 2025 年 4 月 30 日发布的最新开源大型语言模型，专为在 Lean 4 环境中进行形式化数学定理证明而设计。该模型基于 DeepSeek-V3 构建，采用了 6710 亿参数的混合专家（Mixture-of-Experts, MoE）架构，旨在提升数学推理和定理验证的能力。
🔍 主要特点与创新
• 递归定理证明训练流程：DeepSeek-Prover-V2 引入了一种创新的“冷启动”训练方法，利用 DeepSeek-V3 将复杂的数学问题分解为一系列子目标，并在 Lean 4 中形式化这些步骤，从而生成高质量的初始化数据 。
• 强化学习优化：通过强化学习（RL）方法，模型在初始阶段的基础上进一步优化，整合了非正式和正式的数学推理能力，提升了定理证明的效率和准确性 。
• 多模型协同训练：在训练过程中，研究人员还使用了一个较小的 70 亿参数模型来处理子目标的证明搜索任务，从而提高了训练的效率和多样性 。
📊 性能表现
• MiniF2F 测试集：在 MiniF2F 测试集上，DeepSeek-Prover-V2 达到了 88.9% 的通过率，显示出其在形式化定理证明任务中的强大能力 。
• PutnamBench 测试集：在 PutnamBench 的 658 个问题中，模型成功解决了 49 个，进一步验证了其在复杂数学问题上的处理能力 。
• AIME 竞赛问题：在最近的 AIME（美国数学邀请赛）竞赛的 15 个问题中，DeepSeek-Prover-V2 成功解决了 6 个，而 DeepSeek-V3 使用多数投票方法解决了 8 个，表明两者在数学推理能力上差距正在缩小 。
🧠 技术架构亮点
• 混合专家架构（MoE）：模型采用了混合专家架构，在每次推理中仅激活部分专家网络，从而在保持高性能的同时降低了计算成本 。
• Lean 4 集成：DeepSeek-Prover-V2 与 Lean 4 紧密集成，能够生成符合 Lean 4 语法和逻辑的形式化证明，方便数学家和计算机科学家进行验证和应用 。
🔍 主要特点与创新
• 递归定理证明训练流程：DeepSeek-Prover-V2 引入了一种创新的“冷启动”训练方法，利用 DeepSeek-V3 将复杂的数学问题分解为一系列子目标，并在 Lean 4 中形式化这些步骤，从而生成高质量的初始化数据 。
• 强化学习优化：通过强化学习（RL）方法，模型在初始阶段的基础上进一步优化，整合了非正式和正式的数学推理能力，提升了定理证明的效率和准确性 。
• 多模型协同训练：在训练过程中，研究人员还使用了一个较小的 70 亿参数模型来处理子目标的证明搜索任务，从而提高了训练的效率和多样性 。
📊 性能表现
• MiniF2F 测试集：在 MiniF2F 测试集上，DeepSeek-Prover-V2 达到了 88.9% 的通过率，显示出其在形式化定理证明任务中的强大能力 。
• PutnamBench 测试集：在 PutnamBench 的 658 个问题中，模型成功解决了 49 个，进一步验证了其在复杂数学问题上的处理能力 。
• AIME 竞赛问题：在最近的 AIME（美国数学邀请赛）竞赛的 15 个问题中，DeepSeek-Prover-V2 成功解决了 6 个，而 DeepSeek-V3 使用多数投票方法解决了 8 个，表明两者在数学推理能力上差距正在缩小 。
🧠 技术架构亮点
• 混合专家架构（MoE）：模型采用了混合专家架构，在每次推理中仅激活部分专家网络，从而在保持高性能的同时降低了计算成本 。
• Lean 4 集成：DeepSeek-Prover-V2 与 Lean 4 紧密集成，能够生成符合 Lean 4 语法和逻辑的形式化证明，方便数学家和计算机科学家进行验证和应用 。
