Resumen Técnico: Informalización Simbólica

Planteamiento del Problema

El artículo aborda el desafío de la informalización simbólica: la conversión fiable de matemáticas formales (demostraciones y teoremas verificados por máquina) en lenguaje natural fluido sin pérdida de precisión. Aunque los métodos neuronales (Modelos de Lenguaje de Gran Escala - LLMs) han avanzado en la autoformalización (de informal a formal), estos sufren de "alucinaciones" y no pueden garantizar que el teorema formalizado coincida con el texto original. Por el contrario, aunque los resultados de la formalización pueden verificarse automáticamente, el proceso inverso —la informalización— suele ser difícil de automatizar simbólicamente.

Los intentos previos de informalización simbólica han sido criticados por tres razones principales, las cuales este artículo identifica como los requisitos fundamentales para un sistema exitoso:

1. Fluidez: Los resultados suelen carecer de la diversidad y flexibilidad del lenguaje natural, apareciendo rígidos.
2. Productividad: Los sistemas son difíciles de diseñar e implementar.
3. Multilingüismo: Los enfoques suelen fallar al escalar a través de diferentes lenguajes formales o lenguajes naturales.

El artículo argumenta que la informalización no es meramente una traducción "fácil", sino un problema de investigación complejo que requiere un equilibrio entre la solidez semántica (preservar el significado) y la completitud lingüística (cubrir todo el rango de la expresión matemática).

Metodología: El Sistema Informath

El artículo presenta Informath, un sistema construido sobre una arquitectura interlingua para abordar los tres objetivos de fluidez, productividad y multilingüismo.

1. Arquitectura

Informath utiliza un enfoque de interlingua de dos etapas:

• Interlingua Formal (Dedukti): Sirve como núcleo entre varios sistemas de prueba (Agda, Lean, Rocq). Dedukti es un marco lógico minimalista con tipos dependientes y reglas de reescritura. Actúa como la fuente de verdad para el contenido formal.
• Interlingua Lingüística (Grammatical Framework - GF): Gestiona el lado del lenguaje natural. GF es un formalismo gramatical basado en un marco lógico similar a Dedukti, diseñado para la traducción multilingüe.

El flujo de trabajo es: Sistema de Prueba $\to$ Dedukti $\to$ Sintaxis Abstracta de GF $\to$ Lenguaje Natural.

2. Multilingüismo

El multilingüismo se logra mapeando la sintaxis abstracta de Dedukti a la sintaxis abstracta de GF, la cual se linealiza posteriormente en lenguajes naturales concretos.

• Sintaxis Abstracta Compartida: Los conceptos matemáticos centrales se definen en un árbol de sintaxis abstracta (AST) independiente del lenguaje dentro de GF.
• Biblioteca de Gramática de Recursos (RGL): Informath aprovecha la RGL de GF, que proporciona estructuras lingüísticas predefinidas (flexión, concordancia, reglas sintácticas) para aproximadamente 40 idiomas. Esto permite que la misma sintaxis abstracta se renderice correctamente en inglés, francés, alemán, sueco, etc., gestionando automáticamente las variaciones gramaticales (por ejemplo, género, caso, número).

3. Productividad

Para abordar la dificultad de implementación, Informath emplea un stack de despliegue que abstrae la complejidad de GF y el código Haskell para los usuarios finales:

• Tablas de Símbolos (.dkgf): La capa más alta y accesible. Los usuarios definen anotaciones léxicas que mapean constantes de Dedukti a funciones de GF o plantillas de cadenas. Esto permite que personas no lingüistas extiendan el sistema a nuevos conceptos matemáticos sin escribir reglas gramaticales.
• Paradigmas Inteligentes: La RGL genera tablas de flexión a partir de formas de palabras básicas, reduciendo la necesidad de entradas léxicas manuales.
• Código Modular: El sistema separa el núcleo estable (MathCore, que gestiona la solidez semántica) de las extensiones extensibles (MathExtensions, que gestiona la completitud lingüística).

4. Fluidez y Generación de Lenguaje Natural (NLG)

Para lograr la fluidez, Informath va más allá de los Lenguajes Naturales Controlados (CNL) básicos mediante la implementación de un pipeline de NLG de múltiples pasos:

• Determinación de Contenido y Planificación de Texto: Decidir qué decir y en qué orden.
• Agregación: Fusionar hechos atómicos (por ejemplo, convertir "x es par y x es primo" en "x es par y primo").
• Elección Léxica: Seleccionar las palabras apropiadas mediante tablas de símbolos.
• Realización de Superficie: Generar la cadena final utilizando la linealización de GF.
• Clasificación (Ranking): El sistema genera miles de variantes de expresiones para un solo enunciado formal. Estas se clasifican mediante una función de penalización basada en el tamaño del árbol, la profundidad, el recuento de tokens y reglas estilísticas (por ejemplo, evitar oraciones que comiencen con símbolos). Esto asegura que el resultado sea compacto y suene natural.

La gramática se divide en MathCore (un CNL mínimo que cubre todos los constructos de Dedukti) y MathExtensions (que aproxima el lenguaje completo de las matemáticas). El sistema soporta características complejas como:

• Constantes de enlace de variables: Gestión de cuantificadores e integrales mediante Sintaxis Abstracta de Orden Superior (HOAS).
• Cuantificación in situ: Colocación de cuantificadores dentro de predicados (por ejemplo, "cada número natural es par").
• Notación Simbólica: Generación de macros de LaTeX para las partes simbólicas mientras se mantiene la parte verbal de forma natural.

Contribuciones Clave

1. El Sistema Informath: Una implementación funcional que demuestra que la informalización simbólica puede ser fluida, productiva y multilingüe.
2. Arquitectura Interlingua: Un uso novedoso de Dedukti y GF como interlinguas duales para desacoplar la lógica formal de la variación lingüística.
3. Extensión de Bajo Código (Low-Code): Un mecanismo basado en tablas de símbolos que permite a los usuarios extender el sistema a nuevos dominios matemáticos sin modificar el código central del compilador o la gramática.
4. Gestión de la Ambigüedad: Una estrategia para gestionar la ambigüedad inherente del lenguaje natural (por ejemplo, el alcance de los cuantificadores, conjunciones) mediante la generación de múltiples variantes y el uso de la comprobación de tipos o la clasificación para resolverlas, en lugar de imponer reglas rígidas e inequívocas que sacrifiquen la fluidez.

Resultados

El artículo informa sobre el estado actual de Informath:

• Cobertura: El sistema cubre matemáticas de grado (aritmética, teoría de conjuntos, álgebra, topología) y ha sido probado en el proyecto "100 teoremas".
• Salida Multilingüe: Genera con éxito texto fluido en inglés, francés, alemán y sueco a partir de la misma fuente de Dedukti.
• Casos de Estudio:
  • Teoría de Tipos Homotópicos (HoTT): Un caso de estudio sobre un libro de HoTT reveló desafíos con traductores de terceros (Agda a Dedukti) que disparan la complejidad del código debido a los niveles de universo. Sin embargo, una vez convertido, Informath manejó con éxito la informalización, incluyendo escenarios complejos de "proposiciones como tipos".
  • Datos Sintéticos: Se utilizó Informath para generar datos sintéticos para ajustar un LLM (Qwen2.5-7B-Instruct), lo que resultó en un mejor rendimiento de la autoformalización en comparación con la línea base.
• Limitaciones: El sistema aún no es lingüísticamente completo (no cubre todo el lenguaje ordinario de las matemáticas) y la informalización de demostraciones sigue siendo un trabajo en progreso, particularmente en lo que respecta al orden y la omisión de los pasos de la demostración.

Significado y Reivindicaciones

El artículo sostiene que la informalización simbólica es un complemento necesario para la autoformalización neuronal. Mientras que los LLM pueden generar código formal, no pueden garantizar la corrección; la informalización simbólica proporciona un puente fiable y explicable que permite a los usuarios humanos interactuar con sistemas formales en lenguaje natural sin ver el código subyacente.

Los autores concluyen modestamente que, si bien Informath alcanza un nivel de fluidez superior a los CNL básicos, la cobertura total del lenguaje ordinario de las matemáticas sigue siendo un objetivo lejano. Los principales desafíos abiertos son la clasificación del creciente número de variantes generadas y la informalización de demostraciones. El artículo enfatiza que, a diferencia de la formalización, que puede verificarse automáticamente, la informalización requiere una fiabilidad y un conocimiento experto inherentes, lo que convierte el desarrollo de tales herramientas en un esfuerzo significativo pero necesario para el futuro de las matemáticas verificadas por máquina legibles por humanos.