Un sistema de IA sin fine-tuning demostró los 6 problemas de la IMO 2026 en Lean

Investigadores de Case Western Reserve University (el trabajo se hizo durante unas prácticas en Amazon Web Services) han demostrado que un modelo de lenguaje grande ya entrenado, sin ningún fine-tuning, puede demostrar teoremas complejos y la corrección de programas si se organiza bien el trabajo a su alrededor. Como modelo eligieron Anthropic Fable-5. Las demostraciones se escriben en Lean, un lenguaje en el que un pequeño «núcleo» comprueba cada paso del razonamiento y al que no se puede engañar.

El sistema resolvió los seis problemas formalizados de la Olimpiada Internacional de Matemáticas de 2026. También superó todos los problemas de VERINA (un conjunto de programación verificada) y resolvió las condiciones de verificación de NTP4VC, un conjunto industrial de verificación formal de código. Además, resuelve problemas de PutnamBench, un conjunto de problemas formalizados de la olimpiada universitaria Putnam.

Cada resultado contabilizado es una demostración o una refutación del enunciado, y ambas están verificadas por el núcleo de Lean.

Un árbol de agentes en lugar de una serie de reinicios

La dificultad está en que Lean solo responde a una pregunta local: si un paso concreto es válido. Una mala descomposición del problema o la falta de un lema (un enunciado auxiliar) se descubren decenas de pasos después. A ello se suman las limitaciones del modelo: la ventana de contexto y el presupuesto de cómputo.

Los autores lo resuelven de forma recursiva. El agente principal lanza agentes hijos, y cada uno busca otra estrategia de demostración o el lema necesario. Los detalles son estos:

• cada descendiente tiene su propio contexto limpio y su propia copia del proyecto; • un descendiente puede generar a su vez nuevos descendientes, y las herramientas son las mismas para todos; • un descendiente puede gastar decenas de llamadas en un solo lema, pero al padre le devuelve únicamente el lema terminado, un contraejemplo o hallazgos parciales; • los resultados llegan al padre en el turno siguiente, sin esperar a las demás ramas, de modo que un hallazgo temprano puede redirigir la búsqueda; • la búsqueda termina cuando se acepta la primera demostración válida.

En espíritu, esto se parece a la búsqueda en árbol de Monte Carlo, pero las decisiones las toma el propio modelo. Lee el contenido de las respuestas de los descendientes y elige por sí mismo qué ramas continuar, cambiar o ampliar. No se usan contadores de visitas ni estimaciones promediadas.

Otra herramienta es la prueba paralela de tácticas. El agente lanza varios candidatos a la vez sobre el estado actual de la demostración. El que funciona vuelve al contexto, y los rastros de los intentos fallidos se descartan, de modo que el contexto no se llena de ruido.

Lean como servicio escalable

Las demostraciones más difíciles requirieron decenas de subagentes en una sola ejecución. Una máquina no tenía potencia suficiente para Lean, así que la verificación se trasladó a un servicio independiente y sin estado. Los clientes envían el código fuente de Lean por JSON-RPC, en lugar de referirse a archivos locales. Cualquier réplica lista, con las mismas versiones de Lean y Mathlib, puede procesar cualquier solicitud.

Dentro de cada réplica hay un pool de procesos de trabajo con la biblioteca Mathlib ya cargada. La importación tarda decenas de segundos, por lo que los procesos se reutilizan, y la verificación en un proceso «caliente» es notablemente más rápida. Las réplicas se ejecutan en Kubernetes y su número se ajusta automáticamente a la carga.

El sistema cuenta además con una protección específica contra las trampas. Un agente que edita el archivo de la demostración podría debilitar el enunciado del teorema, dejar un marcador sorry o añadir un axioma. Por eso todo lo anterior a la firma del teorema está congelado, y la comprobación final la hace Lean Comparator: el archivo debe compilar sin marcadores y usar solo los axiomas permitidos. El informe del propio agente sobre su éxito no se tiene en cuenta.

Un nuevo examen: código de olimpiada como tareas de verificación

Los benchmarks antiguos están casi agotados, y los conjuntos de verificación de código escritos a mano son pequeños: contienen cientos de problemas, y se pueden memorizar o encontrar en los datos de entrenamiento. Por eso los autores construyeron un pipeline que genera las tareas automáticamente:

• un agente programador escribe soluciones seguras en Rust para problemas al estilo de LeetCode, con una sola función pura sobre datos simples (números, listas, cadenas, árboles, listas enlazadas); • la solución pasa pruebas de referencia y luego se traduce a un modelo ejecutable en Lean; • Rust y Lean se ejecutan con las mismas entradas, y solo se aceptan los programas cuyas salidas coinciden por completo; • un agente distinto escribe la especificación, es decir, una propiedad que debe cumplirse o violarse; • el enunciado se congela y el demostrador lo demuestra o lo refuta.

A diferencia de los conjuntos escritos a mano, estas tareas incorporan obligaciones a nivel de implementación: aritmética de precisión fija, errores explícitos, bucles generados, conversiones de tipo y sustitución funcional del estado mutable. Las refutaciones aportan etiquetas negativas, que no existen en los pipelines con solo demostraciones. La especificación la escribe otro agente antes de que el demostrador la vea, y este no puede elegir un enunciado más fácil.

En una muestra de enunciados con un límite de 30 minutos por cada uno, el sistema resuelve solo una parte. Para un demostrador que casi ha agotado los benchmarks antiguos, estas tareas siguen lejos de la saturación. Se pueden escalar con cómputo, usar para comparar otros demostradores y emplear como recompensas en el aprendizaje por refuerzo con recompensas verificables (RLVR). El test de código no «adivina» nada: ofrece un veredicto verificable del núcleo. Las mutaciones de programas (pequeñas ediciones de código correcto) generan tareas adicionales con etiquetas negativas, pero el artículo no las evalúa.

Qué aporta a los ingenieros

La principal conclusión práctica: sin fine-tuning, el esfuerzo puede ponerse en la infraestructura que rodea al modelo. El aislamiento de contextos, la búsqueda asíncrona, las pruebas paralelas y un servicio de verificación elástico permiten que un modelo convencional obtenga de Lean un resultado que antes exigía modelos entrenados específicamente, como Goedel-Code-Prover. A quienes construyen agentes para verificar código también les servirá el esquema de enunciado congelado más una comprobación final independiente: cierra las vías habituales para engañar al verificador.