Goedel-Prover: Un Modello All'avanguardia per la Dimostrazione Automatica di Teoremi Open-Source

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

February 11, 2025

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

cs.AI

Abstract

Introduciamo Goedel-Prover, un modello linguistico di grandi dimensioni (LLM) open-source che raggiunge le prestazioni all'avanguardia (SOTA) nella generazione automatica di dimostrazioni formali per problemi matematici. La sfida principale in questo campo è la scarsità di enunciati matematici e dimostrazioni formalizzati, che affrontiamo nei seguenti modi. Alleniamo formalizzatori di enunciati per tradurre i problemi matematici in linguaggio naturale da Numina in linguaggio formale (Lean 4), creando un dataset di 1,64 milioni di enunciati formali. I LLM vengono utilizzati per verificare che gli enunciati formali preservino accuratamente il contenuto dei problemi originali espressi in linguaggio naturale. Successivamente costruiamo iterativamente un ampio dataset di dimostrazioni formali addestrando una serie di dimostratori. Ciascun dimostratore riesce a dimostrare molti enunciati che i precedenti non erano in grado di dimostrare, e queste nuove dimostrazioni vengono aggiunte al set di addestramento per il successivo dimostratore. Il dimostratore finale supera tutti i modelli open-source esistenti nella generazione dell'intera dimostrazione. Sul benchmark miniF2F, raggiunge un tasso di successo del 57,6% (Pass@32), superando il precedente miglior modello open-source del 7,6%. Su PutnamBench, Goedel-Prover risolve con successo 7 problemi (Pass@512), classificandosi al primo posto nella classifica. Inoltre, genera 29,7K dimostrazioni formali per i problemi di Lean Workbook, quasi raddoppiando le 15,7K prodotte dai lavori precedenti.

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.