Goedel-Prover-V2: Масштабирование формального доказательства теорем с использованием структурированного синтеза данных и самокоррекции
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
August 5, 2025
Авторы: 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
cs.AI
Аннотация
Мы представляем Goedel-Prover-V2, серию открытых языковых моделей, которые устанавливают новый эталон в области автоматизированного доказательства теорем. Основанный на стандартном конвейере экспертной итерации и обучения с подкреплением, наш подход включает три ключевых инновации: (1) Синтез данных с постепенным усложнением: мы генерируем синтетические задачи возрастающей сложности, чтобы обучить модель осваивать всё более сложные теоремы; (2) Самоисправление с использованием верификатора: мы позволяем модели итеративно корректировать свои доказательства, используя обратную связь от компилятора Lean; (3) Усреднение моделей: мы объединяем контрольные точки моделей, чтобы смягчить снижение разнообразия выходных данных на поздних этапах обучения. Наша небольшая модель, Goedel-Prover-V2-8B, достигает 84,6% pass@32 на MiniF2F и превосходит DeepSeek-Prover-V2-671B по тому же показателю, несмотря на то, что она в 80 раз меньше. Наша флагманская модель, Goedel-Prover-V2-32B, достигает 88,1% на MiniF2F при pass@32 в стандартном режиме и 90,4% в режиме самоисправления, значительно опережая предыдущие достижения. Кроме того, наша флагманская модель решает 86 задач на PutnamBench при pass@184, занимая первое место среди открытых моделей в рейтинге, превосходя рекорд DeepSeek-Prover-V2-671B, который решил 47 задач при pass@1024, при значительно меньшем размере модели и вычислительных ресурсах. На момент выпуска (июль-август 2025 года) Goedel-Prover-V2 демонстрирует наилучшую общую производительность среди всех открытых систем доказательства теорем. Она также входит в число лучших моделей, включая закрытые системы с публично заявленной производительностью, при ограниченном бюджете вычислительных ресурсов на этапе тестирования. Наши модели, код и данные доступны по адресу https://github.com/Goedel-LM/Goedel-Prover-V2.
English
We introduce Goedel-Prover-V2, a series of open-source language models that
set a new state-of-the-art in automated theorem proving. Built on the standard
expert iteration and reinforcement learning pipeline, our approach incorporates
three key innovations: (1) Scaffolded data synthesis: We generate synthetic
tasks of increasing difficulty to train the model to master increasingly
complex theorems; (2) Verifier-guided self-correction: We enable the model to
iteratively revise its proofs by leveraging feedback from the Lean compiler;
(3) Model averaging: We merge model checkpoints to mitigate the decrease in
model output diversity in later stages of training. Our small model,
Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms
DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our
flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in
standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a
large margin. Additionally, our flagship model solves 86 problems on
PutnamBench at pass@184, securing the first place among open-source models on
the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47
problems by pass@1024 with a significantly smaller model size and compute
budget. At the time of its release (July-August 2025), Goedel-Prover-V2
achieves the strongest overall performance among all open-source theorem
provers. It also ranks among the top-performing models--including closed-source
systems with publicly reported performance--under a constrained test-time
compute budget. Our models, code, and data are released at
https://github.com/Goedel-LM/Goedel-Prover-V2.