Goedel-Prover-V2：通过自我修正和逐步数据合成实现高效自动定理证明的新发展

27/08/2025

三个要点
✔️ Goedel-Prover-V2是一个用于小规模高性能自动定理证明的全新开源模型
✔️ 提出了结合支架式数据合成、自校正和模型平均的学习方法
✔️ 以及 MiniF2F 和 PutnamBench。通过实现超过传统大规模模型的性能来证明其效率

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
written by Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin
(Submitted on 5 Aug 2025)
Comments: 24 pages, 10 figures, 4 tables
Subjects: Machine Learning (cs.LG); Artificial Intelligence (cs.AI)

本文所使用的图片要么来自论文、介绍性幻灯片，要么是参考这些图片制作的。

概述

本文提出了自动定理证明（ATP）的新底层模型 Goedel-Prover-V2。

以往的研究需要超大模型（数百个 B 级参数）和庞大的推理计算，这限制了开源模型的性能。
因此，作者引入了一种新颖的学习方法和数据生成策略，以实现高效和高性能的定理证明。
具体来说，他们采用了 "脚手架式数据合成"（生成难度逐步调整的合成问题）、"验证者指导下的自我修正"（利用精益编译器的反馈）和 "模型平均"（保持输出多样性）。平均化 "来保持输出的多样性。

结果，即使只有 32B 大小的模型，也超越了传统的 671B 模型，成功解决了
MiniF2F 基准中的 88.1%（自校正后为 90.4%）和 PutnamBench 中的 86 个问题，为开源模型设定了新的高标准。开源建模达到了新的最高水平。

这表明，无需依赖庞大的计算资源，就能高效地进行高级数学推理。

建议的方法

拟议方法的核心是将 "自我修正 "和 "逐步数据合成 "与使用长思维链的定理证明融合在一起。

首先，"验证器指导下的自我修正 "是一种机制，模型生成的证明通过精益编译器运行，精益编译器分析错误信息并生成修改版本。
这样，用户就能从错误中吸取教训，完成证明，就像人类改进证明一样。

接下来，脚手架数据合成会合成未解决的子问题和从难题的失败尝试中获得的更简单的变体，为模型提供高效的学习信号。
这样，就能利用难度等级进行有效的训练。

此外，还引入了模型平均法，对不同训练阶段获得的模型进行加权平均，以提高性能，同时防止遗漏变体。
最后，我们设计了一个连贯的学习管道，将 SFT（监督微调）、RL（强化学习）和模型平均化结合在一起，从而产生了高效、稳健的定理证明模型。

实验

主要在 MiniF2F 和 PutnamBench 上进行了评估，结果证实，所提出模型的性能明显优于传统方法。

在MiniF2F（高中数学-国际数学奥林匹克水平）Goedel-Prover-V2-32Bはpass@32で88.1%，自校正模式达到90.4%，超过了DeepSeek-Prover-V2-671B。
此外，在 PutnamBench（大学数学竞赛题）中，它成功解决了 86 道题，比之前的 47 道题有了显著提高。

甚至在 MiniF2F 中，8B 模型的表现也优于 671B 模型，这有力地证明了它的效率。
此外，自我修正的效果也得到了量化证明，在 pass@32 的基础上平均提高了 2 分。
缩放分析也证实了 "高样本效率"，即只需生成少量样本即可实现高精度。

这些实验结果表明，即使对于小规模的模型，所提出的方法也能实现最先进的定理证明能力，支持其作为未来数学人工智能研究的基础。