Goedel-Prover : Un modèle de pointe pour la démonstration automatisée de théorèmes en open source

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

February 11, 2025

Auteurs: Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin

cs.AI

Résumé

Nous présentons Goedel-Prover, un modèle de langage large (LLM) open-source qui atteint des performances de pointe (SOTA) en génération automatique de preuves formelles pour des problèmes mathématiques. Le défi clé dans ce domaine est la rareté des énoncés mathématiques formalisés et des preuves, que nous abordons de la manière suivante. Nous formons des formaliseurs d'énoncés pour traduire les problèmes mathématiques en langage naturel de Numina en langage formel (Lean 4), créant ainsi un ensemble de données de 1,64 million d'énoncés formels. Les LLM sont utilisés pour vérifier que les énoncés formels préservent fidèlement le contenu des problèmes mathématiques en langage naturel d'origine. Ensuite, nous construisons de manière itérative un grand ensemble de données de preuves formelles en formant une série de prouveurs. Chaque prouveur réussit à prouver de nombreux énoncés que les précédents n'ont pas pu, et ces nouvelles preuves sont ajoutées à l'ensemble d'entraînement pour le prouveur suivant. Le prouveur final surpasse tous les modèles open-source existants dans la génération de preuves complètes. Sur le benchmark miniF2F, il atteint un taux de réussite de 57,6% (Pass@32), dépassant le précédent meilleur modèle open-source de 7,6%. Sur PutnamBench, Goedel-Prover résout avec succès 7 problèmes (Pass@512), se classant premier au classement. De plus, il génère 29,7K preuves formelles pour les problèmes du Lean Workbook, soit près du double des 15,7K produites par les travaux antérieurs.

English

We introduce Goedel-Prover, an open-source large language model (LLM) that achieves the state-of-the-art (SOTA) performance in automated formal proof generation for mathematical problems. The key challenge in this field is the scarcity of formalized math statements and proofs, which we tackle in the following ways. We train statement formalizers to translate the natural language math problems from Numina into formal language (Lean 4), creating a dataset of 1.64 million formal statements. LLMs are used to check that the formal statements accurately preserve the content of the original natural language problems. We then iteratively build a large dataset of formal proofs by training a series of provers. Each prover succeeds in proving many statements that the previous ones could not, and these new proofs are added to the training set for the next prover. The final prover outperforms all existing open-source models in whole-proof generation. On the miniF2F benchmark, it achieves a 57.6% success rate (Pass@32), exceeding the previous best open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7 problems (Pass@512), ranking first on the leaderboard. Furthermore, it generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the 15.7K produced by earlier works.