Goedel-Prover-V2: Escalando la Demostración Formal de Teoremas con Síntesis de Datos Escalonada y Autocorrección

Resumen

Presentamos Goedel-Prover-V2, una serie de modelos de lenguaje de código abierto que establecen un nuevo estado del arte en la demostración automática de teoremas. Basado en el flujo estándar de iteración experta y aprendizaje por refuerzo, nuestro enfoque incorpora tres innovaciones clave: (1) Síntesis de datos escalonada: Generamos tareas sintéticas de dificultad creciente para entrenar al modelo en el dominio de teoremas cada vez más complejos; (2) Autocorrección guiada por verificador: Permitimos que el modelo revise iterativamente sus demostraciones aprovechando la retroalimentación del compilador Lean; (3) Promediado de modelos: Fusionamos puntos de control del modelo para mitigar la disminución en la diversidad de salidas en etapas avanzadas del entrenamiento. Nuestro modelo pequeño, Goedel-Prover-V2-8B, alcanza un 84.6% en pass@32 en MiniF2F y supera a DeepSeek-Prover-V2-671B bajo la misma métrica, a pesar de ser 80 veces más pequeño. Nuestro modelo principal, Goedel-Prover-V2-32B, logra un 88.1% en MiniF2F en pass@32 en modo estándar y un 90.4% en modo de autocorrección, superando ampliamente el SOTA anterior. Además, nuestro modelo principal resuelve 86 problemas en PutnamBench en pass@184, asegurando el primer lugar entre los modelos de código abierto en el ranking, superando el récord de DeepSeek-Prover-V2-671B de resolver 47 problemas en pass@1024, con un tamaño de modelo y presupuesto computacional significativamente menores. En el momento de su lanzamiento (julio-agosto de 2025), Goedel-Prover-V2 logra el mejor rendimiento general entre todos los demostradores de teoremas de código abierto. También se encuentra entre los modelos de mayor rendimiento—incluyendo sistemas de código cerrado con rendimiento reportado públicamente—bajo un presupuesto computacional limitado en tiempo de prueba. Nuestros modelos, código y datos están disponibles en 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: Escalando la Demostración Formal de Teoremas con Síntesis de Datos Escalonada y Autocorrección

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

Resumen

Support