核心观点 - 新一代开源数学定理证明模型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]