Resumen Técnico: COMPOSE – Composición de Futuros Teoremas a partir de Citaciones y Estructura Formal

Definición del Problema

El artículo aborda el desafío de la generación fundamentada de matemáticas futuras: la tarea de predecir una afirmación matemática futura plausible (una declaración similar a un teorema) para un "papel ancla" dado. Los autores argumentan que una predicción válida debe satisfacer dos restricciones simultáneas:

1. Trayectoria Científica: Debe extender la dirección de investigación indicada por el grafo de citaciones científicas y la evolución de las ideas en la literatura.
2. Fundamentación Formal: Debe respetar las dependencias lógicas inherentes a las matemáticas formales, asegurando que la afirmación sea derivable válidamente de definiciones, lemas y teoremas existentes.

Los enfoques existentes suelen modelar solo una de estas fuentes. Los modelos entrenados únicamente en texto científico pueden generar afirmaciones fluidas pero lógicamente desfundamentadas, mientras que los sistemas de demostración de teoremas razonan sobre estructuras formales pero carecen del contexto científico para identificar direcciones de investigación prometedoras. El artículo postula que combinar estas fuentes complementarias no es trivial debido a las diferencias fundamentales en cómo los artículos científicos y las bibliotecas formales (como Mathlib) organizan el conocimiento.

Metodología: El Marco COMPOSE

Los autores proponen COMPOSE, un marco de doble grafo que condiciona un modelo de lenguaje tanto al contexto de citaciones científicas como a la estructura de teoremas formales. El enfoque consta de tres componentes principales:

1. Construcción de Datos

Los autores construyeron un conjunto de datos de 108,000 ejemplos de grafos pareados científico-formales derivados de artículos de matemáticas de arXiv (2000–2023) y la biblioteca Lean Mathlib.

• Grafo Científico ($G_s$): Construido a partir de un papel ancla y su contexto de citaciones (hasta dos saltos). Incluye nodos abstractos para artículos y nodos de teoremas extraídos del texto. Las aristas representan enlaces de citación y dependencias internas del artículo.
• Grafo Formal ($G_f$): Construido alineando teoremas informales extraídos con teoremas correspondientes en Mathlib. Esta alineación utiliza FrenzyMath (un corpus de descripciones informales escritas por humanos para teoremas de Mathlib) para realizar una recuperación de informal a informal, evitando el ruido de la autoformalización directa. El grafo formal se expande desde la raíz del teorema coincidente utilizando aristas de dependencia extraídas mediante LeanDojo.
• Punto de Referencia: Un conjunto de prueba temporalmente retenido de 47,000 artículos futuros de finales de 2024 y 2025, utilizado para evaluar la capacidad del modelo de predecir resultados publicados reales.

2. Arquitectura del Modelo

COMPOSE emplea una arquitectura de doble codificador seguida de un decodificador condicionado por grafo:

• Doble Codificadores: Dos Redes Neuronales de Grafos (GNN) dedicadas procesan $G_s$ y $G_f$ por separado.
  • Los nodos de $G_s$ se inicializan con incrustaciones E5 (texto científico).
  • Los nodos de $G_f$ se inicializan con incrustaciones DeepSeek-Math (firmas formales).
  • Ambos utilizan paso de mensajes dirigido y específico por tipo de arista con conexiones residuales con compuerta.
• Módulo de Fusión: Las representaciones de ambos grafos se proyectan en un espacio latente compartido y se fusionan mediante un mecanismo de atención cruzada bidireccional. Esto permite al modelo integrar la dirección científica con restricciones formales.
• Decodificador: Un LLM especializado en matemáticas preentrenado (DeepSeek-Math-7B o Mistral-7B) adaptado con LoRA. Se insertan capas de atención cruzada en el decodificador para condicionar la generación sobre las incrustaciones de grafo fusionadas, permitiendo que el modelo atienda a toda la estructura del grafo durante la generación de tokens.

3. Entrenamiento en Dos Etapas

• Etapa 1 (Aprendizaje de Representación): Los codificadores de grafos y el módulo de fusión se entrenan sin el decodificador utilizando tres objetivos:
  • Predicción de Enlaces: Para asegurar que los codificadores capturen la estructura del grafo.
  • Alineación Contrastiva: Para alinear la representación fusionada del grafo con el resumen y la afirmación principal del artículo objetivo.
  • Alineación Cruzada: Para alinear explícitamente los nodos de teoremas informales con sus contrapartes formales coincidentes.
• Etapa 2 (Generación): Se añade el decodificador y se ajusta fino utilizando:
  • Pérdida Autoregresiva: Predicción estándar del siguiente token.
  • Pérdida de Margen del Grafo: Un término de regularización que penaliza al modelo si genera el mismo texto para un par de grafos no coincidentes, obligándolo a depender del contexto específico del grafo.

Resultados Clave

Los experimentos se realizaron en el punto de referencia de 47K artículos futuros, comparando COMPOSE con líneas base sólidas (incluyendo GIANTS, FutureGen, GoAI y varias variantes solo de texto o solo de indicaciones).

• Rendimiento de Recuperación: COMPOSE logró el mayor Gap (0.240), definido como la diferencia en la similitud coseno entre el texto generado y el artículo futuro verdadero frente a artículos no relacionados. Superó significativamente a las líneas base en H@10 (50.8%) y H@100 (80.8%), lo que indica que sus afirmaciones generadas tienen mucha más probabilidad de recuperar el artículo futuro correcto del conjunto.
• Predicción de Afirmaciones Matemáticas Nuevas (NMCP): COMPOSE lideró en Precisión (0.560) y Coincidencia (0.730), demostrando que sus salidas se alinean con teoremas futuros tanto a nivel formal como informal, no solo temáticamente.
• Evaluación por Juez LLM: Un juez LLM (GPT-4.0) evaluó las salidas en Contenido, Profundidad, Novedad, Precisión y Especificidad. COMPOSE obtuvo la puntuación general más alta (3.36/5), particularmente en Profundidad Técnica (3.52) y Especificidad (3.52), produciendo salidas más concretas y matemáticamente ricas que las líneas base, que a menudo generaban resúmenes vagos.
• Estudios de Ablación: Eliminar cualquiera de los codificadores de grafo científico o formal causó caídas significativas en el rendimiento, confirmando que ambas modalidades proporcionan señales complementarias. El grafo formal fue crucial para la fundamentación, mientras que el grafo científico fue esencial para identificar la dirección de investigación correcta.

Significado y Afirmaciones

El artículo afirma que la generación de matemáticas futuras se beneficia de combinar el contexto científico con la estructura formal.

• Generación Fundamentada: Los autores demuestran que confiar únicamente en texto científico conduce a afirmaciones que son temáticamente relevantes pero lógicamente desfundamentadas, mientras que confiar únicamente en la estructura formal limita el modelo a teoremas conocidos sin anticipar nuevas direcciones. COMPOSE conecta con éxito esta brecha.
• Contribución de Datos: La construcción del conjunto de datos pareado de 108K y el punto de referencia de 47K artículos futuros proporciona un nuevo recurso para evaluar la generación matemática fundamentada, abordando la falta de puntos de referencia temporales en este campo.
• Avance Metodológico: El marco de doble grafo con fusión por atención cruzada ofrece un enfoque novedoso para integrar fuentes de conocimiento heterogéneas (literatura informal vs. lógica formal) para tareas generativas.

Los autores señalan limitaciones, específicamente que el método depende de una alineación aproximada informal-formal (lo cual puede introducir ruido en áreas con cobertura escasa de Mathlib) y que las afirmaciones generadas no son verificadas por un asistente de demostración, confiando en su lugar en la recuperación y la evaluación basada en LLM como señales proxy. Sugieren que el trabajo futuro podría incorporar verificación consciente de pruebas para comprobar directamente la corrección formal de las afirmaciones generadas.