Goedel-Beweiser: Ein fortschrittliches Modell für Open-Source-automatisierte Theorembeweise

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

February 11, 2025

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

cs.AI

Zusammenfassung

Wir stellen Goedel-Prover vor, ein Open-Source Large Language Model (LLM), das eine Spitzenleistung bei der automatisierten formalen Beweisgenerierung für mathematische Probleme erreicht. Die Hauptherausforderung in diesem Bereich ist die Knappheit formalisierter mathematischer Aussagen und Beweise, der wir auf folgende Weise begegnen. Wir trainieren Aussageformalisierer, um die natürlichsprachlichen mathematischen Probleme von Numina in formale Sprache (Lean 4) zu übersetzen und erstellen so einen Datensatz von 1,64 Millionen formalen Aussagen. LLMs werden verwendet, um zu überprüfen, ob die formalen Aussagen den Inhalt der ursprünglichen natürlichsprachlichen Probleme korrekt wiedergeben. Anschließend bauen wir iterativ einen großen Datensatz formaler Beweise auf, indem wir eine Reihe von Beweisern trainieren. Jeder Beweiser gelingt es, viele Aussagen zu beweisen, die den vorherigen nicht gelungen sind, und diese neuen Beweise werden dem Schulungssatz für den nächsten Beweiser hinzugefügt. Der endgültige Beweiser übertrifft alle bestehenden Open-Source-Modelle in der Generierung vollständiger Beweise. Auf dem miniF2F-Benchmark erreicht er eine Erfolgsquote von 57,6% (Pass@32), was die vorherigen besten Open-Source-Modelle um 7,6% übertrifft. Auf PutnamBench löst Goedel-Prover erfolgreich 7 Probleme (Pass@512) und belegt den ersten Platz in der Rangliste. Darüber hinaus generiert er 29,7K formale Beweise für Lean Workbook-Probleme, fast doppelt so viele wie die 15,7K, die von früheren Arbeiten erstellt wurden.

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.