Goedel-Prover-V2: Escalonando a Prova de Teoremas Formais com Síntese de Dados Escalonada e Autocorreção

Resumo

Apresentamos o Goedel-Prover-V2, uma série de modelos de linguagem de código aberto que estabelecem um novo estado da arte na prova automática de teoremas. Construído com base no pipeline padrão de iteração de especialistas e aprendizado por reforço, nossa abordagem incorpora três inovações principais: (1) Síntese de dados escalonada: Geramos tarefas sintéticas de dificuldade crescente para treinar o modelo a dominar teoremas cada vez mais complexos; (2) Autocorreção guiada por verificador: Permitimos que o modelo revise iterativamente suas provas, aproveitando o feedback do compilador Lean; (3) Média de modelos: Combinamos checkpoints de modelos para mitigar a diminuição na diversidade das saídas do modelo em estágios posteriores do treinamento. Nosso modelo pequeno, Goedel-Prover-V2-8B, alcança 84,6% de pass@32 no MiniF2F e supera o DeepSeek-Prover-V2-671B na mesma métrica, apesar de ser 80 vezes menor. Nosso modelo principal, Goedel-Prover-V2-32B, atinge 88,1% no MiniF2F em pass@32 no modo padrão e 90,4% no modo de autocorreção, superando o SOTA anterior por uma grande margem. Além disso, nosso modelo principal resolve 86 problemas no PutnamBench em pass@184, garantindo o primeiro lugar entre os modelos de código aberto no leaderboard, superando o recorde do DeepSeek-Prover-V2-671B de resolver 47 problemas em pass@1024, com um tamanho de modelo e orçamento computacional significativamente menores. No momento de seu lançamento (julho-agosto de 2025), o Goedel-Prover-V2 alcança o melhor desempenho geral entre todos os provadores de teoremas de código aberto. Ele também está entre os modelos de melhor desempenho—incluindo sistemas de código fechado com desempenho publicamente relatado—sob um orçamento computacional restrito no momento do teste. Nossos modelos, código e dados são disponibilizados em https://github.com/Goedel-LM/Goedel-Prover-V2.

English

We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.

Goedel-Prover-V2: Escalonando a Prova de Teoremas Formais com Síntese de Dados Escalonada e Autocorreção

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

Resumo

Support