[LG]《Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction》Y Lin, S Tang, B Lyu, Z Yang... [Princeton University & Tsinghua University] (2025)
Goedel-Prover-V2：开源自动定理证明领域的新标杆，兼具卓越准确率与高效计算性能
• 创新三大核心：① Scaffolded数据合成，训练模型逐步掌握更复杂的定理；② Lean编译器反馈驱动的自我修正，实现多轮迭代校正证明错误；③ 模型平均化，提升后期训练中输出多样性，避免性能退化。
• 旗舰32B模型MiniF2F数据集pass• 在PutnamBench上，32B模型自纠错模式解决86道题目，领先其他开源对手，刷新最佳公开记录，展现强大问题解决力。
• 训练流程涵盖专家迭代、强化学习与模型平均，结合长链思维推理与编译器反馈，极大提升证明质量和推理效率。
• 模型在有限推理预算下表现卓越，实现样本效率高，适合社区进一步创新和验证新算法。
• 公开代码、模型及数据，促进自动定理证明和形式化数学研究持续进步。
详见👉 arxiv.org/pdf/2508.03613
自动定理证明形式化验证机器学习人工智能数学AI
