Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Este artículo introduce el Bucle de Conjetura-Prueba (CPL), una tubería que aprovecha el aprendizaje en contexto alimentando iterativamente a un LLM con sus propios teoremas y pruebas formalmente verificados en Lean 4 para mejorar significativamente la tasa de descubrimiento y el éxito de conjeturas matemáticas novedosas y difíciles de demostrar.

Lo esencial

Imagina que estás intentando enseñar a un robot muy inteligente, pero ligeramente olvidadizo, cómo resolver acertijos matemáticos complejos. El robot es un Modelo de Lenguaje Grande (LLM), y los acertijos son demostraciones matemáticas formales escritas en un lenguaje informático estricto llamado Lean.

El artículo presenta una nueva forma de enseñar a este robot, llamada el Bucle de Conjetura-Demostración (CPL). Así es como funciona, explicado mediante analogías sencillas:

El Problema: La Trampa de "Adivinar y Comprobar"

Por lo general, cuando las personas intentan que la IA haga matemáticas, le piden que adivine un acertijo y lo resuelva de una sola vez.

• La Analogía: Imagina pedirle a un estudiante que "Escriba un problema matemático y lo resuelva inmediatamente".
• El Problema: El estudiante se vuelve perezoso. Escribe problemas fáciles (como "2 + 2 = 4") porque son fáciles de resolver. Evita los problemas difíciles porque sabe que podrían fallar. La IA termina generando miles de demostraciones fáciles y aburridas, y se pierde las difíciles e interesantes.

La Solución: La "Danza de Dos Pasos" (CPL)

Los autores dividen el proceso en dos roles distintos: un Conjeturador (el Generador de Ideas) y un Demostrador (el Resolvedor).

1. El Conjeturador (El Arquitecto): Esta parte de la IA examina una biblioteca de reglas matemáticas existentes y saca a la luz nuevas ideas (conjeturas). No intenta resolverlas todavía; simplemente las escribe.
2. El Demostrador (El Constructor): Esta parte toma las ideas e intenta construir una demostración para ellas. Si falla, lo intenta de nuevo. Sigue intentándolo hasta que tiene éxito o se le acaban los intentos.
3. La Biblioteca (La Memoria): Cada vez que el Demostrador construye una demostración con éxito, esa demostración se añade a la biblioteca.

El Ingrediente Mágico: Aprendizaje en Contexto
Aquí está la parte ingeniosa: el Demostrador no solo mira las reglas matemáticas originales. Examina la biblioteca de demostraciones que ya ha construido con éxito durante la sesión actual.

• La Analogía: Imagina a un estudiante que rinde un examen. A la antigua, tenía que confiar solo en lo que había memorizado antes de que comenzara el examen. De esta nueva manera, cada vez que el estudiante resuelve un problema correctamente, se le permite leer su propia solución antes de abordar el siguiente problema. Aprende los "trucos" y las "estrategias" de sus propios éxitos recientes.

Lo Que Descubrieron

Los investigadores probaron esto en algunos conceptos complicados de topología (una rama de las matemáticas que trata sobre formas y espacios) que la IA aún no conocía bien.

• Cantidad vs. Calidad: El método antiguo (adivinar y resolver al mismo tiempo) generó más teoremas en total, pero la mayoría eran cortos y fáciles. El nuevo método (CPL) generó menos teoremas en total, pero eran mucho más difíciles y largos.
• El Gran Éxito: El nuevo método descubrió con éxito un teorema específico y difícil sobre "conjuntos alfa-abiertos" que el método antiguo nunca encontró, incluso después de 20 intentos.
• Aprendiendo del Éxito: Cuando se le dio a la IA la biblioteca de sus propias demostraciones anteriores como una "chuleta" (contexto), pudo demostrar teoremas difíciles que no podía resolver sin ese contexto. Incluso cuando la IA no podía demostrar el teorema en inglés llano, podía demostrarlo en código Lean una vez que había visto demostraciones exitosas similares.

La Conclusión

El artículo afirma que, al separar la "generación de ideas" de la "resolución de demostraciones" y permitir que la IA aprenda de sus propios éxitos verificados en tiempo real, podemos lograr que descubra verdades matemáticas más difíciles y complejas que de otro modo pasaría por alto. Es como darle a la IA un impulso inicial permitiéndole estudiar sus propios deberes antes de presentarse al examen final.

Nota: El artículo se centra estrictamente en este método para generar y verificar teoremas matemáticos. No afirma que este método funcione para diagnósticos médicos, previsiones financieras u otras aplicaciones del mundo real fuera de las matemáticas formales.

Resumen técnico

Resumen Técnico: Descubrimiento de Nuevos Teoremas mediante LLMs con Aprendizaje de Pruebas en Contexto en Lean

Enunciado del Problema
Los Modelos de Lenguaje Grandes (LLMs) han demostrado ser prometedores en la demostración formal de teoremas, pero enfrentan desafíos significativos: pueden alucinar, y generar simultáneamente una conjetura matemática y su prueba a menudo conduce a una convergencia hacia teoremas triviales o fáciles. Los enfoques existentes dependen típicamente del Ajuste Fino Supervisado (SFT) o del Aprendizaje por Refuerzo con Recompensas Verificadas (RLVR), los cuales requieren grandes volúmenes de datos de entrenamiento y son difíciles de aplicar a modelos de código cerrado. Además, los métodos actuales suelen tener dificultades para descubrir teoremas "difíciles de demostrar", ya que la probabilidad de generar un teorema está fuertemente ponderada por la tasa de éxito inmediata de demostrarlo, lo que provoca que la búsqueda colapse en pruebas simples y cortas.

Metodología: El Bucle de Conjetura-Demostración (CPL)
Los autores proponen el Bucle de Conjetura-Demostración (CPL), una tubería diseñada para generar automáticamente conjeturas matemáticas y verificarlas en Lean 4. El marco separa la generación de conjeturas de la generación de pruebas, utilizando una biblioteca de teoremas previamente verificados como contexto para ambas etapas.

La tubería opera a través de cuatro componentes principales: un Conjeturador (agente LLM), un Demostrador (agente LLM), un Servidor Lean y una Biblioteca (datos de código Lean).

1. Fase de Conjetura: El Conjeturador genera nuevas declaraciones matemáticas en formato Lean 4 basadas en la biblioteca actual. Consulta al Servidor Lean para garantizar la validez sintáctica y la novedad (verificando que la declaración no sea ya demostrable por teoremas existentes en Mathlib4 o en la biblioteca actual).
2. Fase de Demostración: Para cada conjetura válida, el Demostrador intenta construir una prueba formal. Crucialmente, el Demostrador recibe la biblioteca (que contiene teoremas y pruebas previamente verificados) como contexto. Esto permite que el LLM aprenda estrategias de prueba mediante aprendizaje en contexto sin reentrenamiento del modelo. El Demostrador itera hasta un número máximo de intentos (establecido en 16 en los experimentos), utilizando los mensajes de error del Servidor Lean para refinar sus intentos.
3. Iteración: Los pares verificados de conjeturas y pruebas se añaden a la biblioteca, la cual luego sirve como contexto para iteraciones subsiguientes.

Esta separación permite que el sistema asigne recursos de búsqueda según la dificultad de la prueba. A diferencia de un bucle simple (SL) donde una declaración y una prueba se generan simultáneamente, el CPL intenta múltiples pruebas para una sola declaración antes de descartarla. Esto desplaza la distribución de los teoremas generados hacia aquellos que son demostrables pero difíciles, en lugar de aquellos que son meramente fáciles de demostrar.

Contribuciones Clave

1. Propuesta de Tubería: La introducción del CPL, un marco que desacopla la generación de conjeturas de la generación de pruebas, permitiendo el descubrimiento de pruebas más largas y complejas.
2. Aprendizaje en Contexto para Modelos de Código Cerrado: La demostración de que los LLMs de código cerrado (específicamente ChatGPT-o3) pueden mejorar sus capacidades de demostración mediante el aprendizaje en contexto a partir de sus propias salidas previamente verificadas, eliminando la necesidad de actualizaciones de parámetros o ajuste fino.
3. Validación Teórica y Empírica: El artículo proporciona un modelo teórico que muestra que el CPL aumenta la probabilidad de generar teoremas difíciles de demostrar en comparación con los marcos de generación simultánea. Experimentalmente, verifica que el CPL redescubrió con éxito un teorema específico de nivel de investigación que el marco de referencia no logró encontrar.

Resultados Experimentales
Los autores evaluaron el CPL frente a una línea base de Bucle Simple (SL) utilizando nociones topológicas (semi-abertura, $\alpha$-abertura y preabertura) definidas dentro de Mathlib pero aún no incluidas en la biblioteca. El objetivo fue el teorema que establece que la intersección de dos conjuntos $\alpha$-abiertos es $\alpha$-abierta.

• Tasa de Descubrimiento: En 20 ejecuciones experimentales, el CPL descubrió el teorema objetivo 5 veces. En contraste, el marco SL, que generó significativamente más teoremas en promedio (328 frente a 106), no logró generar el teorema objetivo ni una sola vez. La prueba exacta de Fisher confirmó que esta diferencia fue estadísticamente significativa ($p = 0.024$).
• Longitud de la Prueba: El CPL generó teoremas con longitudes de prueba significativamente mayores (en conteo de caracteres) en comparación con el SL, apoyando la afirmación teórica de que el marco desplaza el enfoque hacia pruebas más difíciles.
• Efectividad del Contexto:
  • Re-demostración: Al re-demonstrar teoremas generados, proporcionar la biblioteca como contexto aumentó la tasa de éxito del 91% al 99% ($p = 4 \times 10^{-35}$).
  • Teorema Objetivo: Al intentar re-demonstrar el teorema objetivo de intersección $\alpha$-abierta, el demostrador tuvo éxito 7 veces de 80 intentos cuando se le proporcionó la biblioteca generada como contexto. Sin la biblioteca, falló el 100% de las veces.
  • Línea Base en Lenguaje Natural: Cuando se le pidió demostrar el teorema en lenguaje natural, ChatGPT-4o juzgó frecuentemente el teorema como falso o proporcionó pruebas incorrectas, y ChatGPT-o3 lo juzgó consistentemente como falso, lo que indica que el teorema estaba fuera del conocimiento preentrenado de los modelos. El éxito en Lean 4 se atribuyó al aprendizaje en contexto de estrategias de prueba a partir de la biblioteca generada.

Significado y Afirmaciones
El artículo afirma que el CPL aborda eficazmente la limitación de los LLMs en el descubrimiento de teoremas no triviales aprovechando el aprendizaje en contexto a partir de pruebas verificadas auto-generadas. Los autores enfatizan que este enfoque permite la expansión automática de bibliotecas de matemáticas formales (como Mathlib) mediante la generación de proposiciones sobre nociones dadas que pueden no ser explícitamente conocidas por el LLM. El trabajo sugiere que separar las fases de conjetura y demostración, combinado con el enriquecimiento iterativo del contexto, es una estrategia viable para la demostración de teoremas neuronal, particularmente para modelos de código cerrado donde los métodos de entrenamiento tradicionales no son aplicables. Los autores mantienen una postura modesta, señalando que, aunque el marco redescubrió con éxito un teorema conocido de nivel de investigación, se necesita trabajo futuro para refinar el proceso de generación para declaraciones matemáticas más profundas y perspicaces.