核心观点 - 新一代开源数学定理证明模型Goedel-Prover-V2在多个基准测试中大幅超越此前最先进的开源模型DeepSeek-Prover-V2-671B [1] - 32B旗舰模型在MiniF2F测试中正确率提升8% [6]，8B小尺寸模型性能与671B参数模型持平 [7] - 模型在PutnamBench排名第一 [9]，并在MathOlympiadBench等新基准中表现优异 [18][20] 主要成果 - **MiniF2F性能突破**：32B模型Pass@32正确率达88.1%（标准模式）和90.4%（自我修正模式），较前代SOTA提升8% [6][12] - **小模型高效性**：8B参数模型在MiniF2F上通过率83.3%，性能与671B参数模型相当 [7][12] - **PutnamBench领先**：32B模型在Pass@64下解决64题，远超前代Pass@1024解决47题的记录 [14][20] 技术方法 - **专家迭代与强化学习**：结合形式化问题生成与验证流程优化模型 [26] - **分层式数据合成**：自动生成渐进难度问题以提升训练效果 [26] - **验证器引导自我修正**：利用Lean编译器反馈迭代修正证明 [13][32] - **模型平均技术**：融合不同节点权重提升鲁棒性 [12][32] 性能表现 - **基准测试对比**：32B模型在MiniF2F、PutnamBench、MathOlympiadBench中均超越SOTA模型 [18][22] - **计算效率优势**：自我修正模式下输出长度仅从32K tokens增至40K tokens，保持高效 [16] - **扩展性曲线**：32B模型在不同采样预算下性能稳定优于同类模型 [21][25] 模型与数据发布 - **开源模型**：32B与8B模型已发布于HuggingFace [8][33] - **新基准数据集**：MathOlympiadBench包含360道奥林匹克竞赛级别题目 [30] 研究团队 - **核心成员**：普林斯顿大学林勇、唐山茖及金驰教授团队主导开发 [35][38][39] - **研究方向**：聚焦大模型形式化数学推理与高级决策能力 [39]