Goedel-Prover-V2: Scalabilità del Teorema Formale con Sintesi di Dati Scaffoldati e Autocorrezione

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

August 5, 2025

Autori: 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

Abstract

Presentiamo Goedel-Prover-V2, una serie di modelli linguistici open-source che stabiliscono un nuovo stato dell'arte nel campo del teorema automatico. Basato sulla pipeline standard di iterazione esperta e apprendimento per rinforzo, il nostro approccio incorpora tre innovazioni chiave: (1) Sintesi di dati strutturata: generiamo compiti sintetici di difficoltà crescente per addestrare il modello a padroneggiare teoremi sempre più complessi; (2) Autocorrezione guidata da verificatore: consentiamo al modello di rivedere iterativamente le sue dimostrazioni sfruttando il feedback del compilatore Lean; (3) Mediazione dei modelli: uniamo i checkpoint dei modelli per mitigare la riduzione della diversità degli output nelle fasi avanzate dell'addestramento. Il nostro modello più piccolo, Goedel-Prover-V2-8B, raggiunge l'84,6% di pass@32 su MiniF2F e supera DeepSeek-Prover-V2-671B con la stessa metrica, nonostante sia 80 volte più piccolo. Il nostro modello principale, Goedel-Prover-V2-32B, ottiene l'88,1% su MiniF2F a pass@32 in modalità standard e il 90,4% in modalità di autocorrezione, superando di gran lunga i precedenti SOTA. Inoltre, il nostro modello principale risolve 86 problemi su PutnamBench a pass@184, conquistando il primo posto tra i modelli open-source nella classifica, superando il record di DeepSeek-Prover-V2-671B di 47 problemi risolti a pass@1024, con dimensioni del modello e budget computazionale significativamente inferiori. Al momento del rilascio (luglio-agosto 2025), Goedel-Prover-V2 raggiunge le migliori prestazioni complessive tra tutti i dimostratori di teoremi open-source. Si colloca anche tra i modelli più performanti—inclusi i sistemi closed-source con prestazioni pubblicamente riportate—sotto un budget computazionale limitato durante il test. I nostri modelli, codice e dati sono disponibili su 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.