Goedel-Prover: Um Modelo de Vanguarda para Prova Automática de Teoremas em Código Aberto

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

Resumo

Apresentamos o Goedel-Prover, um modelo de linguagem de grande escala (LLM) de código aberto que alcança o desempenho de ponta (SOTA) na geração automatizada de provas formais para problemas matemáticos. O principal desafio nessa área é a escassez de enunciados e provas matemáticas formalizados, que abordamos das seguintes maneiras. Treinamos formalizadores de enunciados para traduzir problemas matemáticos em linguagem natural do Numina para linguagem formal (Lean 4), criando um conjunto de dados com 1,64 milhão de enunciados formais. LLMs são usados para verificar se os enunciados formais preservam com precisão o conteúdo dos problemas originais em linguagem natural. Em seguida, construímos iterativamente um grande conjunto de dados de provas formais treinando uma série de provadores. Cada provador consegue demonstrar muitos enunciados que os anteriores não conseguiram, e essas novas provas são adicionadas ao conjunto de treinamento para o próximo provador. O provador final supera todos os modelos de código aberto existentes na geração de provas completas. No benchmark miniF2F, ele alcança uma taxa de sucesso de 57,6% (Pass@32), superando o melhor modelo de código aberto anterior em 7,6%. No PutnamBench, o Goedel-Prover resolve com sucesso 7 problemas (Pass@512), ocupando o primeiro lugar no ranking. Além disso, ele gera 29,7 mil provas formais para problemas do Lean Workbook, quase dobrando as 15,7 mil produzidas por trabalhos 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.