Resumen Técnico: Nazrin: Una Táctica de Automatización de Pruebas Neuronales Atómicas en Lean 4

Planteamiento del Problema

La demostración de teoremas asistida por máquinas en sistemas como Lean 4 enfrenta desafíos significativos al entrenar agentes automatizados con pruebas escritas por humanos. Los obstáculos principales incluyen:

1. Espacios de Acción Sin Límite: Las pruebas humanas utilizan una variedad infinita de tácticas con parámetros arbitrarios (por ejemplo, simp con largas listas de argumentos, use con testigos arbitrarios), lo que crea un espacio de búsqueda ruidoso y difícil de aprender.
2. Vistas de Presentación vs. de Búsqueda: Las pruebas escritas por humanos suelen priorizar la concisión y la legibilidad (Vista de Presentación), ocultando los pasos incrementales de razonamiento hacia atrás (Vista de Búsqueda) que son realmente necesarios para descubrir la prueba. Esto incluye "saltos misteriosos" y la elisión de pasos intermedios.
3. Acoplamiento de Metavariables: En Lean, los objetivos suelen depender unos de otros (metavariables acopladas). Una búsqueda en árbol ingenua no tiene en cuenta el hecho de que resolver un objetivo puede resolver instantáneamente otro o hacer que un camino sea imposible, complicando la búsqueda en un Grafo Acíclico Dirigido (DAG) en lugar de un simple árbol.
4. Restricciones de Hardware: Los probadores de teoremas neuronales existentes a menudo requieren recursos computacionales significativos, lo que limita su accesibilidad y la escala de los datos de entrenamiento que pueden procesar.

Metodología

El artículo presenta Nazrin (Neural Atomizer for Inhabitation Problems), un agente de demostración de teoremas basado en redes neuronales de grafos (GNN). La metodología se basa en tres pilares fundamentales:

1. Tácticas Atómicas

Los autores definen un conjunto pequeño y finito de "tácticas atómicas" capaces de probar cualquier enunciado demostrable en Lean. Estas tácticas están diseñadas para tener un espacio de parámetros acotado, asegurando que el espacio de acción para el agente sea finito.

• Completitud: El conjunto cubre todos los constructores de expresiones de alto nivel en Lean (por ejemplo, intro para abstracción lambda, exact/apply para constantes, cases para tipos inductivos).
• Propiedades: Las tácticas son invariantes (no cambian las metavariables asignadas sin retroceder), completas, progresivas (siempre progresan) y deterministas.
• Minimización de la Sección Transversal: El conjunto se elige para minimizar las "secciones transversales" (el número de objetivos acoplados), reduciendo la dificultad del problema de generación de guía.

2. Atomización de Transposición

Para entrenar al agente, los autores desarrollaron un nuevo algoritmo para convertir las pruebas existentes escritas por humanos (Vista de Presentación) en secuencias de tácticas atómicas (Vista de Búsqueda).

• Atomización: El algoritmo traduce términos de prueba arbitrarios en una serie de pasos atómicos. Utiliza el término de prueba de verdad de base (ground-truth) para guiar la construcción de una nueva prueba utilizando solo tácticas atómicas.
• Transposición: El algoritmo reordena la ejecución de las tácticas para coincidir con la "Vista de Búsqueda". Prioriza los objetivos "sucesor" (objetivos cuyas soluciones informan a los predecesores) sobre los objetivos "predecesor". Esto imita el razonamiento hacia atrás utilizado en el descubrimiento (por ejemplo, pruebas $\epsilon$-$\delta$) en lugar de la presentación hacia adelante.
• Transposición a Nivel de Estado y de Objetivo: El sistema reordena la disposición de tácticas para evitar callejones sin salida. Por ejemplo, permite que las tácticas "semigradas" no conflictivas (que actúan sobre partes de un objetivo o de una variable libre) se dispongan en un orden arbitrario, incluso si los objetivos acoplados aún no han sido instanciados.

3. ExprGraph y Arquitectura Neuronal

El agente utiliza una Red Neuronal de Grafos (GNN) para procesar expresiones de Lean, representadas como ExprGraphs.

• Esencialización: Las expresiones se convierten en grafos donde se eliminan las distinciones técnicas irrelevantes (por ejemplo, nombres de variables específicos, metadatos). El grafo preserva las simetrías fundamentales (por ejemplo, la $\alpha$-equivalencia) y asegura que las subexpresiones correspondan a subgrafos.
• Autómata Probabilístico Neuronal (NPA): En lugar de un modelo generativo estándar, Nazrin utiliza un NPA. La GNN condiciona las probabilidades de transición de un autómata de estados finitos.
  • Estado Kind: Selecciona el tipo de táctica (por ejemplo, intro, apply).
  • Estados Descendientes: Cabezales especializados de la GNN generan argumentos (por ejemplo, seleccionar una constante para apply o una variable libre).
• Eficiencia: El modelo es pequeño (1.5M de parámetros para la biblioteca estándar, 11M para Mathlib) y se ejecuta en hardware de CPU de consumo, generando miles de tácticas por minuto.

Principales Contribuciones

1. Tácticas Atómicas: Un conjunto finito y completo de tácticas que reduce el espacio de acción de la demostración de teoremas a un tamaño manejable, permitiendo un aprendizaje por refuerzo y un entrenamiento supervisado eficientes.
2. Algoritmo de Atomización de Transposición: Un método para generar datos de entrenamiento a gran escala convirtiendo las matemáticas formalizadas existentes en pruebas de vista de búsqueda atómica, enseñando efectivamente al agente cómo encontrar pruebas en lugar de cómo presentarlas.
3. ExprGraph: Una representación basada en grafos reducida de las expresiones de Lean que explota las simetrías matemáticas y las referencias de variables, imitando explícitamente los mecanismos de atención encontrados en los modelos de lenguaje.
4. Probador Nazrin: Un agente basado en GNN de bajos recursos que se entrena con éxito en datos atomizados y generaliza a nuevos teoremas.
5. Marco de Evaluación: Una evaluación rigurosa que imita el desarrollo de nuevas teorías, donde el agente es entrenado en una sección de la biblioteca y probado en la siguiente para asegurar que no haya fuga de información.

Resultados

Los autores evaluaron Nazrin en la biblioteca estándar de Lean y en Mathlib:

• Éxito de la Atomización: Aproximadamente el 58% de 170,180 teoremas fueron atomizados con éxito.
• Generalización:
  • Entrenado en la Sección 1 de la Biblioteca Estándar, Nazrin logró un 57% de precisión en la Sección 2.
  • Entrenado en la Sección 3 de Mathlib, logró un 34% de finalización en la Sección 4.
• Comparación: Nazrin demostró la capacidad de probar teoremas que las tácticas de automatización existentes (Aesop y Grind) no pudieron resolver dentro de un límite de tiempo de 15 segundos.
• Rendimiento: El sistema opera eficientemente en hardware de consumo, contrastando con los requisitos de alto recurso de muchos probadores basados en LLM.

Significado y Reivindicaciones

El artículo afirma que Nazrin aborda el desajuste fundamental entre la estructura de las pruebas escritas por humanos y los requisitos de la búsqueda automatizada. Al imponer un espacio de acción finito mediante tácticas atómicas y generar datos de entrenamiento mediante la atomización de transposición, los autores demuestran que:

• Los agentes de aprendizaje automático pueden ser entrenados para descubrir pruebas de forma incremental sin necesidad de generar parámetros complejos y arbitrarios desde cero.
• Las representaciones basadas en grafos son efectivas para capturar las simetrías estructurales de las demostraciones matemáticas.
• La demostración de teoremas de alto rendimiento es alcanzable con hardware modesto, haciendo que esta tecnología sea más accesible.

Los autores señalan que, si bien el sistema es prometedor, actualmente no cubre todos los teoremas (la atomización falla para algunas pruebas de sección transversal alta) y la arquitectura no ha sido totalmente ajustada. Sugieren que el trabajo futuro podría centrarse en mejorar la cobertura de la atomización, reducir las secciones transversales y refinar la arquitectura neuronal para manejar de forma más robusta el condicionamiento de múltiples parámetros y los datos no simbólicos (números/cadenas).