Goedel-Prover: Un Modelo de Vanguardia para la Demostración Automatizada de Teoremas de Código Abierto

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

February 11, 2025

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

cs.AI

Resumen

Presentamos Goedel-Prover, un modelo de lenguaje grande (LLM, por sus siglas en inglés) de código abierto que logra un rendimiento de vanguardia en la generación automatizada de pruebas formales para problemas matemáticos. El desafío principal en este campo es la escasez de enunciados matemáticos y pruebas formalizadas, que abordamos de las siguientes maneras. Entrenamos formalizadores de enunciados para traducir los problemas matemáticos en lenguaje natural de Numina a lenguaje formal (Lean 4), creando un conjunto de datos de 1.64 millones de enunciados formales. Los LLM se utilizan para verificar que los enunciados formales preserven con precisión el contenido de los problemas originales en lenguaje natural. Luego construimos de manera iterativa un extenso conjunto de datos de pruebas formales entrenando una serie de demostradores. Cada demostrador tiene éxito en demostrar muchos enunciados que los anteriores no pudieron, y estas nuevas pruebas se agregan al conjunto de entrenamiento para el siguiente demostrador. El demostrador final supera a todos los modelos de código abierto existentes en la generación de pruebas completas. En el benchmark miniF2F, logra una tasa de éxito del 57.6% (Pass@32), superando al mejor modelo de código abierto anterior en un 7.6%. En PutnamBench, Goedel-Prover resuelve con éxito 7 problemas (Pass@512), clasificándose en primer lugar en la tabla de clasificación. Además, genera 29.7K pruebas formales para problemas de Lean Workbook, casi duplicando las 15.7K producidas por trabajos anteriores.

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.