Resumen Técnico: Visored: Un probador de lenguaje natural controlado para matemáticas generadas por LLM

Declaración del Problema

Los modelos de lenguaje extensos (LLMs) han demostrado una capacidad creciente en el razonamiento matemático, sin embargo, siguen siendo propensos a las alucinaciones. En consecuencia, las pruebas generadas por IA son solo tan confiables como el proceso de verificación. Si bien los probadores de teoremas automáticos (ATPs) y los modelos de prueba completa (por ejemplo, aquellos que apuntan a Lean o Rocq) han logrado altas tasas de éxito en benchmarks como miniF2F, típicamente requieren una declaración ya formalizada como entrada. El cuello de botella crítico reside en la autoformalización: la traducción de la prosa matemática informal a una forma verificable por máquina.

Esta traducción no es trivial porque la matemática informal depende de un trasfondo compartido, condiciones laterales implícitas (por ejemplo, $x \neq 0$) y abusos de notación que los lectores completan automáticamente. Una traducción directa a un lenguaje formal requiere comprometerse con lemas de librerías específicos, subtipos, convenciones de casos límite y coerciones (por ejemplo, $\mathbb{N}$ vs. $\mathbb{Z}$ vs. $\mathbb{R}$) que no dejan rastro en el texto de origen. Los errores en estas decisiones rara vez se manifiestan como errores de compilación, sino más bien como un "desplazamiento semántico silencioso", donde una sentencia compila pero ya no refleja la intención original.

Metodología

Visored es un prototipo de investigación diseñado para cerrar la brecha entre la escritura matemática informal y la verificación formal mediante la introducción de una representación intermedia (IR) de tipos dependientes que se sitúa entre LaTeX y los probadores de bajo nivel como Lean.

Arquitectura Central

El sistema opera como un pipeline (Figura 2 en el artículo) que consta de las siguientes etapas:

1. Entrada de Lenguaje Natural Controlado (CNL): Visored acepta un subconjunto controlado de inglés matemático embebido en LaTeX. El vocabulario (plantillas de oraciones como "Let...", "Assume...", "Then..." y comandos LaTeX) está definido por archivos de especificación .lpcsv externos, lo que permite extender el lenguaje superficial sin modificar el parser.
2. Sintaxis y Semántica: La entrada se parsea en un árbol de sintaxis y luego se elabora en un AST tipado (sem AST). Esta etapa resuelve nombres, asigna tipos y clases, y garantiza la biendefinición en el momento de la comprobación de tipos. Siguiendo la tradición de PVS, las funciones parciales (por ejemplo, $1/x$, $\sqrt{x}$, $\log x$) portan argumentos de hipótesis implícitos (por ejemplo, $x \neq 0$, $x \ge 0$) que deben ser satisfechos antes de que la expresión sea aceptada.
3. IR de Nivel Medio (MIR): El AST tipado se reduce a Visored MIR, el sustrato para el solver.
4. Solver con Límite de Costo: El solver satisface las obligaciones de "Then..." y las condiciones de biendefinición utilizando un motor impulsado por reglas y con límite de costo (llamado "Miracle"). Emplea una base de datos de reglas hacia adelante y hacia atrás (inspirada en ProofGrader) y tácticas especializadas (por ejemplo, normalizadores algebraicos, solvers de cadenas) para cerrar pasos rutinarios que los matemáticos suelen omitir.
5. Emisión Opcional a Lean: Las pruebas aceptadas pueden transcribirse a Lean 4. La transposición es una etapa descendente opcional para la verificación del kernel externo. El proceso de transposición implica la reproducción del historial de normalización y la gestión de testigos de coerción entre sistemas numéricos.

Filosofía de Diseño

Visored se basa en dos observaciones primarias:

1. Fluidez de los LLM: Los LLMs están entrenados predominantemente en matemáticas informales. Una superficie de CNL se mantiene cerca del dominio donde los LLM ya son fluidos, evitando la necesidad de que el modelo aprenda la sintaxis de bajo nivel del probador (tácticas, nombres de lemas de librería) desde cero.
2. Tractabilidad: Tender el puente entre el razonamiento natural y el formal es más tratable que la demostración de teoremas totalmente automatizada. Al hacer que el LLM suministre el esquema de la prueba en CNL, el solver solo necesita cerrar pasos pequeños y obvios, una tarea que está plenamente al alcance de la ingeniería agéntica moderna.

El sistema trata el parsing semántico "ascendente" (LaTeX $\to$ Visored) como el problema difícil, manejado por el LLM, mientras que la proyección "descendente" (Visored $\to$ Lean) es un proceso determinista y mecánico.

Contribuciones Clave

• IR de Tipos Dependientes para Autoformalización: Visored introduce una IR semánticamente rica donde cada decisión que no tiene rastro superficial en LaTeX (subtipos, lemas de librería, convenciones de casos límite, casts) se hace explícita.
• Extensibilidad Impulsada por Especificaciones: La superficie de CNL se define mediante archivos de configuración externos en lugar de parsers codificados, lo que permite ajustar el vocabulario a convenciones matemáticas específicas (libros de texto, competencias, investigación) sin recompilar el sistema.
• Diagnósticos Localizados: A diferencia de los sistemas que proporcionan un veredicto único de aceptar/rechazar tras una compilación completa en Lean, Visored proporciona diagnósticos localizados en la etapa de elaboración o resolución. Esto permite un bucle de "verificar y revisar" donde un LLM puede identificar y corregir errores específicos.
• Imposición de Biendefinición: El sistema impone la biendefinición (por ejemplo, asegurar que $x \neq 0$ antes de $1/x$) mediante argumentos de hipótesis implícitos satisfechos por el solver, en lugar de depender de las convenciones de totalización del probador objetivo.
• Integración de Escuelas Existentes: Visored sintetiza elementos de Mizar/Naproche (superficie CNL), PVS (biendefinición en el tiempo de comprobación de tipos), Lean/Rocq (tipos dependientes) y ProofGrader (resolución impulsada por reglas con presupuesto de costo) en un único pipeline orientado al LLM.

Resultados Experimentales

Los autores reportan un estudio de cobertura sobre la división miniF2F-valid (244 problemas), que sirvió tanto de conjunto de desarrollo como de evaluación.

• Rendimiento: Un agente de codificación de LLM (Claude), guiado por un documento de habilidades que describe la superficie de CNL, produjo pruebas verificadas por Visored para 222 de los 244 problemas (91%).
• Desglose:
  • Inducción: 100% (8/8)
  • Álgebra: 98% (86/88)
  • Teoría de Números: 97% (66/68)
  • AMC/AIME: 93% / 87%
  • IMO (Olimpiada): 35% (7/20)
• Análisis de Fallos: Los problemas no resueltos se atribuyeron a brechas en la base de datos de reglas de Visored (por ejemplo, falta de la desigualdad AM-GM, ausencia de tipos de campos finitos, identidades trigonométricas) o regresiones en el prototipo, más que a la incapacidad del LLM para encontrar la estrategia de la prueba. Los autores afirman explícamente que el agente falló al resolver estos problemas porque la "maquinaria" necesaria aún no se había implementado en el sistema.
• Costo de Transposición: El esquema de emisión dispersa actual resulta en una salida de Lean altamente verbosa, con una relación de recuento de líneas mediana de $\approx 250\times$ comparada con las pruebas de Lean escritas a mano, y una cola que alcanza $\approx 25,000\times$. Esto se debe a la reproducción de los pasos de normalización y los testigos de coerción.

Significancia y Reivindicaciones

El artículo posiciona a Visored no como un probador de teoremas automatizado competitivo, sino como una prueba de concepto para una nueva infraestructura para verificar y organizar las matemáticas informales producidas por IA.

• Reivindicaciones Modestas: Los autores declaran explícitamente que no pretenden ser un probador de teoremas automatizado competitivo, ni extrapolan los resultados a divisiones de prueba no contenidas. El 91% de cobertura se presenta como un límite inferior de lo que el diseño puede expresar, no como una tasa de éxito ajustada.
• Cambio de Cuello de Botella: El trabajo apoya la visión de que la restricción vinculante en las matemáticas de IA se está desplazando de "generar ideas" a "verificarlas y organizarlas a escala".
• Modos de Utilidad: Visored está diseñado para funcionar en cuatro modos:
  1. Verificador en tiempo de inferencia: Un chequeador en tiempo real para salidas de LLM.
  2. Bucle de autoformalización: Un mecanismo para que los LLM reescriban pruebas basadas en diagnósticos localizados.
  3. Señal de recompensa densa: Proporcionar retroalimentación paso a paso para el Aprendizaje por Refuerzo (RL).
  4. Generador de datos CNL: Crear un corpus renovable de pruebas leídas naturalmente y formalmente verificadas.

El artículo concluye que la combinación de una superficie de CNL, una IR de tipos dependientes y un solver impulsado por reglas crea un pipeline donde los fallos son localizados y accionables, ofreciendo una ruta más fiable desde la prosa informal hacia pruebas verificadas por el kernel que los enfoques actuales de autoformalización directa. Los problemas no resueltos representan un retraso en la implementación de reglas y maquinaria, no una limitación fundamental del diseño.