模型性能突破 - DeepSeek-Prover-V2在普特南测试中刷新记录至49道题解答，远超当前第一名Kimi-Prover的10道题表现[2][3] - 在miniF2F测试中，671B参数的Prover-V2通过率达到88.9%，7B参数版本在非CoT模式下解决13个671B模型未能处理的问题[36][9] - 7B小模型展现出独特推理能力，在处理有限基数问题时使用Cardinal.toNat等671B模型未掌握的技巧[9][10] 技术架构创新 - 采用"形式化和非形式化数学证明统一模型"设计，整合DeepSeek-V3的高上下文窗口和自然语言推理能力[15] - 引入"子目标分解的强化学习"方法，通过递归证明搜索合成冷启动数据，使用70亿参数模型处理子目标证明[19][21] - 建立两阶段训练体系：第一阶段生成非CoT数据，第二阶段采用高精度CoT模式强化复杂问题推理能力[28][29] 训练方法论 - 采用GRPO算法进行强化学习，通过二元奖励机制（正确证明得1分）优化策略，避免使用单独裁判模型[32][33] - 监督微调数据包含两个来源：专家迭代收集的非CoT形式化验证数据，以及冷启动CoT结构化证明路径数据[31] - 对7B模型执行与671B相同的强化学习阶段，使其上下文窗口扩展至32768个token并融入非CoT证明数据[35] 行业影响与生态建设 - 推出ProverBench基准数据集，包含325个形式化数学问题（15道AIME竞赛题+310道教科书问题）[38][39] - GitHub仓库12小时内获350+星标，引发X/Twitter和Hugging Face社区热烈讨论，包括Kimina-Prover团队祝贺[51][52][59] - 普林斯顿教授评价miniF2F测试最后10%-20%问题的攻克标志着"能力重大飞跃"，显示行业竞争白热化[57] 团队与研发背景 - 18人团队包含DeepSeek-V3/R1/Prover系列前作核心成员，新增清华背景研究员Shirong Ma等资深成员[42][44][45] - 采用Fire-Flyer AI-HPC架构降低训练成本，但未披露具体基础设施优化细节[48][49] - 研究延续DeepSeek-Prover系列技术路线，从V1的合成数据微调演进至V2的子目标分解强化学习[12][13][14]