Goedel-Prover-V2 : Mise à l'échelle de la démonstration formelle de théorèmes grâce à la synthèse de données échafaudées et à l'auto-correction

papers.abstract

Nous présentons Goedel-Prover-V2, une série de modèles de langage open-source qui établissent un nouvel état de l'art en démonstration automatique de théorèmes. Construit sur le pipeline standard d'itération experte et d'apprentissage par renforcement, notre approche intègre trois innovations clés : (1) Synthèse de données échafaudée : Nous générons des tâches synthétiques de difficulté croissante pour entraîner le modèle à maîtriser des théorèmes de plus en plus complexes ; (2) Auto-correction guidée par vérificateur : Nous permettons au modèle de réviser itérativement ses preuves en exploitant les retours du compilateur Lean ; (3) Moyennage de modèles : Nous fusionnons des points de contrôle de modèles pour atténuer la diminution de la diversité des sorties du modèle aux stades avancés de l'entraînement. Notre petit modèle, Goedel-Prover-V2-8B, atteint 84,6 % de réussite à pass@32 sur MiniF2F et surpasse DeepSeek-Prover-V2-671B selon la même métrique, malgré une taille 80 fois plus petite. Notre modèle phare, Goedel-Prover-V2-32B, atteint 88,1 % sur MiniF2F à pass@32 en mode standard et 90,4 % en mode auto-correction, surpassant largement les précédents SOTA. De plus, notre modèle phare résout 86 problèmes sur PutnamBench à pass@184, se classant premier parmi les modèles open-source sur le leaderboard, dépassant le record de DeepSeek-Prover-V2-671B qui résolvait 47 problèmes à pass@1024, avec une taille de modèle et un budget de calcul nettement inférieurs. Au moment de sa sortie (juillet-août 2025), Goedel-Prover-V2 atteint les performances globales les plus élevées parmi tous les démonstrateurs de théorèmes open-source. Il se classe également parmi les modèles les plus performants—y compris les systèmes fermés avec des performances publiquement rapportées—sous un budget de calcul limité en phase de test. Nos modèles, code et données sont disponibles à l'adresse 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.

Goedel-Prover-V2 : Mise à l'échelle de la démonstration formelle de théorèmes grâce à la synthèse de données échafaudées et à l'auto-correction

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

papers.abstract

Support