Goedel-Prover-V2: Schaalvergroting van Formeel Bewijzen met Scaffolded Data Synthese en Zelfcorrectie

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

August 5, 2025

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

Samenvatting

We introduceren Goedel-Prover-V2, een reeks open-source taalmodelen die een nieuwe standaard zetten in geautomatiseerd bewijzen van stellingen. Gebouwd op het standaard expert iteration- en reinforcement learning-pijplijn, integreert onze aanpak drie belangrijke innovaties: (1) Scaffolded data synthesis: We genereren synthetische taken van toenemende moeilijkheidsgraad om het model te trainen in het beheersen van steeds complexere stellingen; (2) Verifier-guided self-correction: We stellen het model in staat om zijn bewijzen iteratief te herzien door gebruik te maken van feedback van de Lean-compiler; (3) Model averaging: We combineren modelcheckpoints om de afname in diversiteit van modeloutput in latere trainingsfasen te beperken. Ons kleine model, Goedel-Prover-V2-8B, behaalt 84,6% pass@32 op MiniF2F en presteert beter dan DeepSeek-Prover-V2-671B onder dezelfde metriek, ondanks dat het 80 keer kleiner is. Ons vlaggenschipmodel, Goedel-Prover-V2-32B, behaalt 88,1% op MiniF2F bij pass@32 in standaardmodus en 90,4% in zelfcorrectiemodus, wat een aanzienlijke verbetering is ten opzichte van de vorige state-of-the-art. Daarnaast lost ons vlaggenschipmodel 86 problemen op op PutnamBench bij pass@184, waarmee het de eerste plaats inneemt onder open-source modellen op de leaderboard, en overtreft het het record van DeepSeek-Prover-V2-671B van 47 opgeloste problemen bij pass@1024 met een aanzienlijk kleiner modelformaat en rekenbudget. Op het moment van release (juli-augustus 2025) behaalt Goedel-Prover-V2 de sterkste algehele prestaties onder alle open-source stellingbewijzers. Het behoort ook tot de best presterende modellen—inclusief closed-source systemen met publiek gerapporteerde prestaties—onder een beperkt testtijd-rekenbudget. Onze modellen, code en data zijn vrijgegeven op https://github.com/Goedel-LM/Goed-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.