Goedel-Prover-V2是什么
goedel-prover-v2 是普林斯顿大学、清华大学、英伟达等顶尖机构联合推出的开源定理证明器。goedel-prover-v2通过分层式数据合成、验证器引导的自我修正和模型平均等创新技术，显著提升自动形式化证明生成的性能。模型包含两个参数版本：32b和8b。32b模型在minif2f基准测试中达到90.4%的pass@32成绩，超越671b的deepseek-prover-v2。goedel-prover-v2 在putnambench和matholympiadbench基准测试中位居榜首，展现强大的定理证明能力。goedel-prover-v2的推出为ai在数学定理证明领域的研究提供新的里程碑。
Goedel-Prover-V2的主要功能
自动生成证明：为复杂的数学问题生成形式化的证明。自我修正能力：通过Lean编译器的反馈，模型能迭代修正自身的证明，提高证明质量。高效训练与优化：用分层式数据合成和模型平均技术，提升训练效率和模型性能。开源与可扩展性：提供开源模型和数据集，便于研究者进一步开发和改进。Goedel-Prover-V2的技术原理
分层式数据合成（Scaffolded Data Synthesis）：自动生成难度逐步递增的证明任务，帮助模型从简单问题逐步过渡到复杂问题。基于生成中级难度的问题，填补简单问题和复杂问题之间的空白，提供更密集的训练信号。验证器引导的自我修正（Verifier-Guided Self-Correction）：模型用Lean编译器的反馈，学习如何迭代修正自身的证明。高度模拟人类在完善证明时的修正过程，提升证明的准确性和可靠性。模型平均（Model Averaging）：基于平均多个训练阶段的模型检查点，恢复模型的多样性。在更大的Pass@K值下显著提升模型的整体性能，增强鲁棒性。Goedel-Prover-V2的性能表现
MiniF2F 基准测试：32B模型：Pass@32：达到 90.4%，显著优于DeepSeek-Prover-V2-671B的 82.4%。自校正模式：在自校正模式下，Pass@32成绩进一步提升至 90.4%。8B模型：Pass@32：达到 83.3%，与DeepSeek-Prover-V2-671B的 82.4% 相当，但模型规模小了近100倍。PutnamBench 基准测试：32B模型：Pass@64：解决 64个问题，位居榜首。Pass@32：解决了 、57个问题，显著优于DeepSeek-Prover-V2-671B的 47个问题。8B模型：Pass@32：表现也十分出色，与DeepSeek-Prover-V2-671B相当。MathOlympiadBench 基准测试：32B模型：解决 73个问题，显著优于DeepSeek-Prover-V2-671B的 50个问题。8B模型：表现也非常接近，展现强大的定理证明能力。