🤖 AI

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Pythagoras-Prover es una familia de demostradores de teoremas Lean de código abierto y computacionalmente eficientes que aprovecha el ajuste fino supervisado basado en currículo y la Formalización Aumentada de Lean para lograr un rendimiento de vanguardia en evaluaciones de demostración formal con significativamente menos parámetros que los modelos existentes.

Autores originales: Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

Publicado 2026-06-12

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás intentando enseñarle a un robot a resolver acertijos matemáticos extremadamente difíciles, pero con un truco: el robot debe escribir su solución en un lenguaje estricto y legible por computadora llamado Lean. Si el robot comete incluso el más mínimo error lógico, la computadora rechaza la respuesta. Este es el mundo de la Demostración Automática de Teoremas.

Durante mucho tiempo, la única forma de que un robot fuera bueno en esto era alimentarlo con cantidades masivas de datos y usar un "cerebro" (un modelo de computadora) tan enorme que costaba millones de dólares ejecutarlo. Era como intentar ganar un torneo de ajedrez contratando a un equipo de 1,000 grandes maestros para que pensaran por ti.

El artículo presenta Pythagoras-Prover, una nueva familia de robots matemáticos que demuestra que no necesitas un cerebro gigante o un presupuesto de un millón de dólares para ganar. Lo lograron a través de tres trucos ingeniosos:

1. El "Campamento de Entrenamiento" (Aprendizaje por Currículo)

En lugar de lanzar al robot a lo más profundo con los problemas más difíciles de inmediato, los investigadores construyeron un campamento de entrenamiento con tres niveles: Fácil, Medio y Difícil.

La Analogía: Imagina enseñar a un niño a montar en bicicleta. No empiezas con ellos en un sendero de montaña. Empiezas en una acera plana (Fácil), luego en una colina suave (Medio) y finalmente en el sendero de la montaña (Difícil).
Cómo lo hicieron: Crearon una enorme biblioteca de problemas matemáticos. Si un problema era demasiado difícil para el robot, no lo desechaban simplemente. Utilizaban una "rúbrica" (una lista de verificación de errores comunes) para descomponer el problema en una versión más simple que el robot pudiera resolver. Esto permitió que el robot aprendiera paso a paso, construyendo confianza y habilidad antes de enfrentarse a los gigantes.

2. La Máquina de "Mad Libs" (Formalización Aumentada de Lean)

El mayor problema en este campo es la falta de buenos problemas de práctica. Los investigadores se dieron cuenta de que podían crear más problemas de práctica sin necesidad de que un humano los escribiera o de que una supercomputadora los verificara.

La Analogía: Imagina que tienes una historia matemática perfecta. En lugar de escribir una historia nueva desde cero, juegas a un juego de "Mad Libs". Sustituyes los números, cambias los nombres de los personajes o reorganizas el orden de los pasos, pero la lógica de la historia permanece igual.
Cómo lo hicieron: Tomaron sus problemas verificados y utilizaron una herramienta llamada ALF para mutarlos. Crearon variaciones (versiones más simples, versiones más difíciles o simplemente una redacción diferente). No verificaron cada nueva variación con la estricta computadora (que es lenta y costosa); solo verificaron que el nuevo problema pareciera un problema matemático válido. Esto hizo explotar su biblioteca de problemas de práctica por 2.5 veces, dándole al robot mucho más material para aprender.

3. El Bucle de "Autorreflexión" (Autodestilación)

Una vez que el robot aprendió lo básico, dejaron que se enseñara a sí mismo.

La Analogía: Imagina a un estudiante que ha estudiado mucho. En lugar de solo tomar un examen, intenta resolver nuevas variaciones de los problemas que acaba de aprender. Si lo logra, lo escribe como un nuevo ejemplo para estudiar más tarde.
Cómo lo hicieron: El robot generó demostraciones para esas variaciones de "Mad Libs". Aunque la computadora no verificó cada una de ellas, el hecho de que el robot pudiera generar una demostración para una versión mutada significaba que realmente entendía la lógica, no solo memorizaba la respuesta. Estos datos de "autoaprendizaje" hicieron al robot aún más inteligente.

Los Resultados: Cerebro Pequeño, Grandes Victorias

El artículo compara a sus nuevos robots con los "gigantes" actuales del campo:

El Robot de 4B: Este robot tiene 4 mil millones de "neuronas" (parámetros). Es aproximadamente 167 veces más pequeño que el campeón anterior (DeepSeek-Prover-V2, que tiene 671 mil millones de neuronas).
- El Resultado: A pesar de ser diminuto, el robot de 4B resolvió más problemas correctamente que el robot gigante. Es como si un genio de las matemáticas de secundaria venciera a un equipo de doctores en PhD porque el genio fue entrenado mejor.
El Robot de 32B: Este robot, un poco más grande, se convirtió en el mejor robot de código abierto jamás probado en estos parámetros, resolviendo el 93% de los problemas.

El Experimento de "Difusión"

Los investigadores también probaron una forma diferente de pensar llamada Difusión.

La Analogía:
- Estándar (Autorregresivo): Escribir una oración palabra por palabra, de izquierda a derecha. Si cometes un error al principio, tienes que reescribir todo.
- Difusión: Imagina un boceto borroso de una oración. El robot mira el boceto completo y rellena las palabras faltantes de una sola vez, refinando la imagen hasta que esté clara. Puede corregir un error en el medio sin tener que reescribir el principio.
El Resultado: Este robot de "Difusión" fue 2.5 veces más rápido generando respuestas que el robot estándar, aunque fue ligeramente menos preciso. Esto muestra una nueva forma de intercambiar velocidad por precisión.

La "Prueba de Estrés" (MiniF2F-ALF)

Para ver si los robots solo estaban memorizando respuestas o si realmente estaban aprendiendo, los investigadores crearon una "prueba de estrés". Tomaron las preguntas del examen y las mutaron ligeramente (cambiando números, intercambiando variables) usando la misma técnica de "Mad Libs".

El Resultado: La mayoría de los robots fallaron esta prueba porque habían memorizado las preguntas originales. Sin embargo, Pythagoras-Prover manejó las mutaciones mucho mejor. Esto demuestra que aprendieron la lógica de las matemáticas, no solo las respuestas específicas.

Resumen

Pythagoras-Prover demuestra que no necesitas una supercomputadora para resolver demostraciones matemáticas difíciles. Al usar un programa de entrenamiento inteligente, crear infinitas variaciones de problemas de práctica y dejar que el robot se enseñe a sí mismo, puedes construir un robot pequeño y eficiente que supere a los gigantes masivos y costosos del pasado.

Resumen Técnico: Pythagoras-Prover

Declaración del Problema

Los demostradores de teoremas modernos en Lean han logrado un sólido rendimiento, pero dependen en gran medida de un sustancial cómputo de entrenamiento e inferencia, lo que a menudo requiere modelos de escala de frontera (cientos de miles de millones de parámetros) o procedimientos de inferencia computacionalmente intensivos como la búsqueda extensiva, la autocorrección y grandes presupuestos de muestreo. Esta dependencia es impulsada por la escasez de datos de pruebas verificadas y las largas trazas de razonamiento requeridas para la búsqueda de pruebas formales, lo que hace que el ajuste fino supervisado (SFT) y el muestreo sean costosos. En consecuencia, existe una brecha significativa entre los demostradores de código abierto pequeños y sus contrapartes más grandes, lo que limita la accesibilidad para investigadores y profesionales sin recursos de cómputo masivos.

Metodología

Los autores presentan Pythagoras-Prover, una familia de demostradores de Lean 4 de código abierto y computacionalmente eficientes. El enfoque se basa en un pipeline de datos por etapas y frugal en el uso de cómputo, en lugar de la escala bruta del modelo.

1. Construcción de Datos y Aprendizaje por Currículo

El corpus de entrenamiento se construye en tres niveles de dificultad (Fácil, Medio, Difícil), todos controlados por el comprobador de tipos de Lean para garantizar la corrección:

Niveles Fácil y Medio: Generados mediante un pipeline de tres etapas inspirado en "Teorema Prover como Juez". Problemas de lenguaje natural de conjuntos de datos como DART-Math-Hard, DeepScaleR y OpenR1-Math son autoformalizados en sentencias de Lean. Las pruebas fallidas son analizadas, y un proceso de destilación guiada por rúbricas genera variantes sintéticas simplificadas que apuntan a categorías de error específicas (por ejemplo, fallos de tácticas, desajustes de tipos). Este proceso produce una mejora relativa del 30% en las tasas de éxito de la autoformalización.
Nivel Difícil: Obtenido de problemas de nivel de competición (Olimpiadas, AIME, AMC) de Big-Math-RL-Verified. A diferencia de los niveles más fáciles, estos no se simplifican para preservar su dificultad para el aprendizaje por refuerzo (RL).
SFT por Currículo: Los modelos se entrenan utilizando un currículo ordenado por dificultad (Fácil $\to$ Medio $\to$ Difícil) con LoRA (Adaptación de Bajo Rango) para mantener la eficiencia de los parámetros. Se aplica un esquema de filtrado dinámico de razonamiento de pruebas durante el SFT para gestionar el presupuesto de contexto de 8k tokens: si la cadena de razonamiento más la prueba exceden el límite, el razonamiento se descarta mientras se retiene la prueba; si la prueba por sí sola excede el límite, la instancia se descarta.

2. Formalización de Lean Aumentada (ALF) y Autodestilación

Para superar el cuello de botella de la capacidad de verificación de Lean, los autores introducen la Formalización de Lean Aumentada (ALF).

Mecanismo: ALF aplica cinco operadores de mutación estructurados (simplificación, generalización, propuesta de lemas, descomposición de pasos de prueba, reformulación) a instancias semilla verificadas.
Eficiencia: En lugar de verificar cada instancia mutada con Lean (lo cual es computacionalmente prohibitivo), ALF utiliza un chequeo de alineación de sentencias ligero. Verifica que la prueba generada haga referencia a la sentencia mutada, asegurando la validez estructural sin una compilación completa.
Autodestilación: El modelo post-RL genera pruebas para estas sentencias mutadas. Esto expande el corpus aproximadamente 2.5 $\times$ (a ~2M de instancias) sin requerir la verificación por instancia. Este corpus expandido se utiliza para el SFT continuado y para entrenar un demostrador basado en difusión.

3. Arquitecturas de Modelos

La familia abarca dos paradigmas de generación:

Demostradores Autorregresivos: Modelos de 4B y 32B de parámetros entrenados con el pipeline anterior.
Demostrador Basado en Difusión: Pythagoras-Prover-Diffusion-4B, el primer concepto de demostrador basado en difusión para Lean. Utiliza enmascaramiento basado en tácticas, donde tácticas completas de Lean son enmascaradas y denotadas como unidades en lugar de tokens individuales, alineando el objetivo de denotación con los pasos de razonamiento discretos.

4. Aprendizaje por Refuerzo (RL)

El RL se realiza en problemas difíciles reservados utilizando GRPO (Optimización de Política Relativa de Grupo) con ajuste fino de todos los parámetros. La recompensa es binaria (la prueba compila y se alinea con la sentencia). Los autores señestan que el RL produce solo ganancias modestas sobre el modelo de currículo-SFT, sugiriendo que el corpus supervisado de alta calidad ya interioriza un fuerte comportamiento de búsqueda de pruebas.

Contribuciones Clave

Demostradores Computacionalmente Eficientes: Una familia de demostradores de Lean de código abierto (4B, 32B y un modelo de difusión de 4B) que desafía la suposición de que el razonamiento formal fuerte requiere modelos de escala de frontera.
Pipeline de Datos ALF: Un esquema de mutación estructurado que expande los corpus verificados aproximadamente 2.5 $\times$ utilizando chequeos de sanidad ligeros en lugar de la verificación de Lean por instancia, desacoplando la expansión del corpus del rendimiento del verificador.
Benchmark MiniF2F-ALF: Un benchmark de perturbación sensible a la contaminación creado aplicando mutaciones de ALF al conjunto de prueba MiniF2F. Sirve como una prueba de estrés para evaluar si los modelos dependen de la recuperación exacta del benchmark o poseen comportamientos de prueba transferibles.
Primer Demostrador de Difusión: Un demostrador basado en difusión viable para Lean, demostrando que el refinamiento iterativo es una estrategia de decodificación factible para pruebas formales, aunque con limitaciones actuales de longitud de contexto.

Resultados Experimentales

Evaluados en MiniF2F-Test, PutnamBench y MiniF2F-ALF:

MiniF2F-Test (Pass@32):
- Pythagoras-Prover-4B logra un 86.1%, superando a DeepSeek-Prover-V2-671B (82.4%) a pesar de ser aproximadamente 167 $\times$ más pequeño. También supera a Goedel-Prover-V2-8B (84.6%) y Kimina-Prover-70B (84.0%).
- Pythagoras-Prover-32B logra un 89.8%, liderando todos los demostradores de código abierto evaluados sin autocorrección.
MiniF2F-Test (Pass@2048):
- Pythagoras-Prover-32B alcanza un 93.03%, estableciendo un nuevo estado del arte para demostradores de red neuronal de pesos abiertos sin autocorrección, superando a Goedel-Prover-V2-32B (92.2% en Pass@8192) con un cuarto del presupuesto de muestreo.
PutnamBench:
- Pythagoras-Prover-32B resuelve 93 de 672 problemas en Pass@2048, el resultado más fuerte de código abierto, superando a Goedel-Prover-V2 (86 en Pass@184 con autocorrección).
MiniF2F-ALF (Robustez):
- Todos los modelos evaluados se degradan en este benchmark perturbado, confirmando que la alta precisión en el split original no garantiza la robustez ante variantes estructurales.
- Pythagoras-Prover-32B sigue siendo el más fuerte (85.0%), y Pythagoras-Prover-4B (83.2%) alcanza la paridad con el Goedel-Prover-V2-32B que es 8 $\times$ más grande (83.6%), degradándose menos bajo la perturbación.
Eficiencia de la Difusión:
- Pythagoras-Prover-Diffusion-4B logra un 63.25% de Pass@32 en MiniF2F-Test. Aunque es menos preciso que su contraparte autorregresiva, genera pruebas 2.58 $\times$ más rápido (10.56 vs 4.10 tokens/seg), ofreciendo un mayor rendimiento por segundo de GPU.

Significado y Reivindicaciones

El artículo afirma que el razonamiento de teoremas de Lean fuerte no necesita depender exclusivamente de modelos de escala de frontera. Los resultados demuestran que la construcción cuidadosa de datos (aprendizaje por currículo, aumentación ALF, autodestilación) y las recetas de entrenamiento eficientes (LoRA, filtrado dinámico) pueden sustituir, en parte, la escala bruta del modelo.

Específicamente, los autores destacan:

Eficiencia: Pythagoras-Prover-4B supera a un modelo de 671 mil millones de parámetros, lo que sugiere que la receta de entrenamiento propuesta se transfiere limpiamente a regímenes de modelos pequeños donde las líneas base de escala de miles de millones son impracticables.
Robustez: El uso de mutaciones ALF durante el entrenamiento mejora la robustez ante perturbaciones a nivel de sentencia, como se evidencia por la menor caída de rendimiento en MiniF2F-ALF en comparación con las líneas base.
Nuevos Paradigmas: La introducción de un demostrador basado en difusión establece una línea base inicial para el refinamiento iterativo en la demostración de pruebas, abriendo una dirección complementaria donde los demostradores pueden compararse por rendimiento y pruebas por segundo de GPU, no solo por precisión.

Los autores concluyen que el pipeline de datos "frugal en cómputo" es el principal motor de estos resultados, permitiendo un rendimiento de estado del arte bajo presupuestos de cómputo prácticos.