Resumen Técnico: Descubrimiento de Teoremas Auto-Supervisado en un Sistema Axiomático Formal

Declaración del Problema

Si bien los sistemas de IA recientes, particularmente los Modelos de Lenguaje de Gran Escala (LLMs), han demostrado un progreso significativo en el razonamiento matemático, dependen en gran medida de la información previa proporcionada por humanos, como textos matemáticos, código y bibliotecas de teoremas existentes. Una cuestión abierta crítica es: ¿Puede un agente descubrir teoremas útiles de forma autónoma partiendo únicamente de las reglas primitivas de un sistema axiomático formal, sin acceso a conocimientos previos humanos, bibliotecas de teoremas existentes o conjuntos de problemas de entrenamiento?

Los métodos actuales suelen depender de la construcción de conocimiento humano para iniciar el razonamiento. Incluso los agentes con capacidad de auto-mejora en dominios axiomáticos suelen depender de jueces externos para evaluar la utilidad de los teoremas descubiertos. Este artículo investiga si un agente puede no solo descubrir teoremas, sino también identificar y utilizar aquellos que son "útiles" para mejorar su propia búsqueda de pruebas y el rendimiento de sistemas de razonamiento externos, basándose exclusivamente en axiomas y reglas de inferencia.

Metodología

1. Entorno Formal: Sistema de Hilbert como una Máquina de Pila

Los autores instancian el problema dentro de un sistema de axiomas de Hilbert para la lógica proposicional. El sistema es deliberadamente mínimo, consistiendo en:

• Tres Axiomas:
  • $Ax1: A \to (B \to A)$ (Debilitamiento)
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ (Distribución)
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ (Contraposición)
• Una Regla de Inferencia: Modus Ponens (MP), derivando $Y$ a partir de $X$ y $X \to Y$.

Para facilitar el aprendizaje, los autores formulan la demostración de teoremas como un proceso de decisión determinista, condicionado al objetivo y basado en una máquina de pila $(S, A, s_0, P)$:

• Estado ($S$): Una pila finita de fórmulas.
• Acciones ($A$): Introducir instancias de $Ax1, Ax2, Ax3$ en la pila, o aplicar Modus Ponens (MP).
• Mecanismo: La acción MP utiliza la unificación de Hindley–Milner. Si el elemento superior de la pila se unifica con $X \to Y$ y el elemento inferior se unifica con $X$, ambos se extraen de la pila y se introduce $Y$.
• Éxito: Una demostración es exitosa si la pila contiene una única fórmula que coincide con el objetivo propuesto.

2. Algoritmo de Descubrimiento de Teoremas Auto-Supervisado

La contribución central es un algoritmo que alterna entre la búsqueda de pruebas y la extracción de teoremas útiles, construyendo una biblioteca de teoremas que sirven como lemas para búsquedas futuras.

A. Aprendizaje de Política Condicionada al Objetivo

El agente aprende una política $\pi_\theta(A|S, g)$ para predecir la siguiente acción dado el estado actual de la pila $S$ y un objetivo $g$.

• Aprendizaje de Perspectiva (Hindsight Learning): Durante un episodio de búsqueda, cualquier estado donde la pila contenga una única fórmula $f_t$ es tratado como un "teorema alcanzado", independientemente de si era el objetivo original.
• Señal de Entrenamiento: El prefijo de acciones que conduce a $f_t$ se trata como una demostración de $f_t$. Estos prefijos se añaden a un conjunto de entrenamiento $D_{train}$ para actualizar la política mediante pérdida de entropía cruzada.
• Búfer de Objetivos ($G$): Un búfer mantiene los teoremas descubiertos. El agente muestrea objetivos uniformemente de $G$ para episodios de búsqueda subsiguientes, efectivamente iniciando su propio currículo.

B. Extracción de Teoremas Útiles

Para evitar que la biblioteca se sature con teoremas triviales o redundantes, el algoritmo filtra los teoremas descubiertos basándose en dos criterios:

1. Generalidad: Los teoremas se filtran para eliminar aquellos que son meras especializaciones de otros candidatos. El sistema retiene solo los elementos "mínimos" bajo un orden parcial definido por la sustitución de fórmulas (es decir, manteniendo las formas más generales).
2. Reproducibilidad: El sistema estima la probabilidad de que la política actual pueda volver a demostrar un teorema. Utilizando una media posterior bayesiana (prior Beta(1,1)), prioriza los teoremas que han sido descubiertos pero que son difíciles de reproducir de manera fiable. Estos teoremas "difíciles de reproducir" son valiosos porque añadirlos como lemas comprime las rutas de demostración complicadas.

C. Expansión de la Biblioteca de Multi-Generación

El proceso opera en generaciones:

1. Aprendizaje de Política: Entrenar la política sobre el espacio de acciones actual (inicialmente solo axiomas y MP).
2. Extracción: Identificar teoremas útiles de la biblioteca de objetivos $G$ basados en generalidad y reproducibilidad.
3. Expansión del Espacio de Acciones: Añadir los teoremas extraídos como nuevas acciones de la biblioteca (por ejemplo, $Thm_1, Thm_2$). Cuando se seleccionan, estas acciones introducen el teorema correspondiente en la pila, actuando como un lema pre-verificado.
4. Iteración: Repetir el proceso, permitiendo que el agente utilice los teoremas descubiertos previamente para encontrar nuevos teoremas más complejos.

Contribuciones Clave

1. Formulación: La demostración de teoremas proposicionales se formula como un proceso de decisión de máquina de pila basado directamente en los axiomas de Hilbert y las reglas de inferencia, evitando la dependencia de corpus de pruebas externos.
2. Algoritmo: Se propone un algoritmo de descubrimiento de teoremas auto-supervisado que expande una biblioteca de teoremas partiendo únicamente de reglas primitivas. Reutiliza los teoremas extraídos como lemas para la búsqueda de pruebas posterior.
3. Descubrimiento Autónomo: El agente descubre decenas de miles de teoremas y encuentra demostraciones para problemas de referencia escritos por humanos sin utilizar conocimientos previos humanos para el entrenamiento.
4. Transferibilidad: Los teoremas extraídos sirven como conocimiento externo efectivo, mejorando el rendimiento de las demostraciones de LLMs externos cuando se les proporcionan como lemas en el prompt.

Resultados Experimentales

1. Descubrimiento de Teoremas y Cobertura

• Crecimiento: El número de teoremas descubiertos aumenta a lo largo de seis generaciones, demostrando la capacidad del agente para expandir su base de conocimientos de forma autónoma.
• Rendimiento en Benchmarks: El agente encuentra con éxito demostraciones del sistema de Hilbert para el 30% de un conjunto de referencia escrito por humanos (derivado del libro de texto de Kleene).
• Comparación: Mientras que GPT-5-high (el baseline más fuerte) logra solo un ~23% de precisión en estos benchmarks sin asistencia, la capacidad del agente para encontrar demostraciones para el 30% sugiere que descubre demostraciones no triviales que son significativas desde una perspectiva matemática humana.

2. Impacto en el Razonamiento de LLMs

• Lemas en el Prompt: Cuando los teoremas extraídos se proporcionan como lemas en el prompt a variantes de GPT-4o y GPT-5, sus tasas de éxito de demostración en los problemas de referencia mejoran significamente.
• Análisis Cualitativo:
  • Algunos teoremas descubiertos corresponden a principios bien conocidos (por ejemplo, el principio de explosión, $\neg A \to (A \to B)$), que son fácilmente interpretables.
  • Otros (por ejemplo, el levantamiento complejo de implicación) no son inmediatamente obvios para los humanos, pero funcionan eficazmente como conocimiento de apoyo en las demostraciones de los LLM.
  • Esto indica que el agente puede hacer emerger lemas útiles que los humanos no proporcionaron explícitamente, y que estos lemas son transferibles entre diferentes arquitecturas de razonamiento (del agente a los LLM).

Significado y Reivindicaciones

El artículo afirma proporcionar evidencia de que se pueden descubrir teoremas útiles mediante la búsqueda de pruebas sin depender de bibliotecas de teoremas proporcionadas por humanos.

• IA Auto-Evolutiva: El trabajo sugiere un camino hacia sistemas de IA auto-evolutivos para las matemáticas que puedan expandir autónomamente su conocimiento formal mediante la búsqueda de pruebas, asegurando al mismo tiempo que cada descubrimiento sea formalmente verificable.
• Verificabilidad Formal: A diferencia de los LLM que pueden alucinar enunciados plausibles pero incorrectos, los descubrimientos del agente están estrictamente fundamentados en los axiomas y las reglas de inferencia del sistema de Hilbert.
• Modestia: Los autores no pretenden haber superado a los LLM de vanguardia en el razonamiento general. En su lugar, demuestran que, en un entorno formal restringido, un agente puede aprender a descubrir y utilizar su propio conocimiento para resolver problemas que son difíciles incluso para los LLM avanzados, y que este conocimiento auto-descubierto puede aumentar otros sistemas.

El estudio está limitado a un único sistema axiomático (lógica proposicional de Hilbert), pero los autores postulan que el marco es generalizable a sistemas más ricos como la lógica de primer orden o la teoría de conjuntos, lo cual sigue siendo una dirección para trabajos futuros.