DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Aquí presento un resumen técnico detallado del artículo "DRIFT: DECOMPOSE, RETRIEVE, ILLUSTRATE, THEN FORMALIZE THEOREMS", publicado en ICLR 2026.

1. El Problema: Limitaciones en la Autoformalización con LLMs

La autoformalización (traducir enunciados matemáticos en lenguaje natural a lenguajes formales verificables como Lean) sigue siendo un desafío mayor para los Modelos de Lenguaje Grandes (LLMs). Aunque los LLMs han avanzado en el razonamiento informal, enfrentan dificultades críticas al intentar formalizar:

• Falta de correspondencia directa: Los enunciados informales son densos y multifacéticos, careciendo de un mapeo directo a los teoremas y lemas específicos de las bibliotecas formales (como Mathlib).
• Limitaciones de la recuperación actual: Los métodos de recuperación aumentada (RAG) existentes suelen consultar bibliotecas externas utilizando el enunciado informal completo como consulta. Esto es subóptimo porque:
  1. La complejidad del enunciado hace que la recuperación sea imprecisa para definiciones atómicas necesarias.
  2. Incluso si se recuperan las definiciones correctas, los modelos a menudo carecen del conocimiento contextual sobre cómo usar esas definiciones sintácticamente en un teorema, lo que lleva a errores estructurales y de sintaxis.
• Problemas de conocimiento estático: El ajuste fino (fine-tuning) de modelos para autoformalización es riesgoso debido a la actualización constante de las bibliotecas formales, lo que puede causar alucinaciones sobre objetos que han sido renombrados o eliminados.

2. Metodología: El Framework DRIFT

Para abordar estas limitaciones, los autores proponen DRIFT (Decompose, Retrieve, Illustrate, Then Formalize Theorems), un marco de cuatro etapas diseñado para adaptar la recuperación de dependencias y la augmentación de contexto a la complejidad de las matemáticas formales.

Etapa 1: Descomposición (Decompose)

En lugar de tratar el enunciado informal como una consulta monolítica, un LLM descompone el enunciado en un conjunto de sub-consultas atómicas ($Q$).

• Cada sub-consulta aísla un único concepto matemático (ej. "un número primo de la forma $4t+3$").
• Cada sub-consulta incluye una descripción en lenguaje natural y una representación formal predicha por el modelo (ej. p : ℕ con condiciones Nat.Prime p).
• Objetivo: Transformar una búsqueda compleja en búsquedas precisas y granulares que coincidan mejor con la estructura de dependencias de las bibliotecas formales.

Etapa 2: Recuperación (Retrieve)

Para cada sub-consulta generada, un recuperador denso (fine-tuned con BGE-M3) identifica las premisas dependientes en la biblioteca formal (ej. Mathlib).

• Se utiliza un recuperador entrenado específicamente para la tarea de "recuperación de dependencias", alineando enunciados informales con sus objetos formales necesarios.
• Se recuperan los mejores candidatos (top-1) para cada sub-consulta y se agregan eliminando duplicados para formar el conjunto de premisas recuperadas ($R_{DRIFT}$).

Etapa 3: Ilustración (Illustrate)

Este es un componente clave que diferencia a DRIFT. Simplemente recuperar definiciones no es suficiente; el modelo necesita ver cómo se usan.

• Se selecciona un pequeño conjunto de teoremas ilustrativos ($T$) que demuestran el uso práctico de las premisas recuperadas.
• Se utiliza un algoritmo codicioso (greedy) para maximizar la cobertura de las premisas recuperadas con el menor número de teoremas (presupuesto $m=3$).
• Objetivo: Proporcionar ejemplos de sintaxis y patrones de aplicación, actuando como un "andamio" (scaffold) para guiar al modelo en la integración correcta de las definiciones.

Etapa 4: Formalización de Teoremas (Formalize Theorems)

Finalmente, un LLM (el formalizador) genera el enunciado formal ($FS$) condicionado en todo el contexto ensamblado:
$$C = I \oplus R_{DRIFT} \oplus T \oplus IF$$
Donde $I$ son instrucciones, $R_{DRIFT}$ son las premisas recuperadas, $T$ son los teoremas ilustrativos e $IF$ es el enunciado original.

3. Contribuciones Clave

1. Marco DRIFT: Introducción de un enfoque de recuperación aumentada impulsado por la descomposición, que rompe la barrera entre la definición formal y su uso sintáctico mediante la descomposición de consultas y la augmentación con ejemplos.
2. Nuevos Estados del Arte (SOTA): Logro de nuevos récords en recuperación de dependencias y autoformalización en los conjuntos de datos ProofNet y ConNF, utilizando tanto modelos de frontera (GPT-4.1, DeepSeek-V3.1) como modelos especializados de código abierto (Goedel-V2-8B).
3. Análisis de Límites del Modelo: Demostración de que la utilidad de las dependencias recuperadas depende de la brecha entre el conocimiento paramétrico del modelo y la complejidad del enunciado. Esto resalta la necesidad de estrategias de recuperación adaptativas.

4. Resultados Experimentales

Los experimentos se realizaron en tres benchmarks: ProofNet (matemáticas universitarias, distribución interna), MiniF2F-test (olimpiadas, autocontenido) y ConNF (teoría de conjuntos avanzada, fuera de distribución - OOD).

• Recuperación de Dependencias: DRIFT mejoró consistentemente la recuperación en comparación con la línea base monolítica (DPR). En ProofNet, el puntaje F1 se duplicó casi (de ~13.77% a ~27.68% con Claude-Opus-4).
• Autoformalización (Conjunto OOD - ConNF):
  • DRIFT mostró un rendimiento excepcional en el benchmark ConNF, donde los modelos tienen poco conocimiento paramétrico.
  • Con GPT-4.1, DRIFT mejoró el puntaje BEq+@10 en un 55.57% en comparación con la línea base sin recuperación, superando incluso al "oráculo imperfecto" (que tiene las dependencias correctas pero sin contexto de uso).
  • Esto demuestra que los teoremas ilustrativos son cruciales para la generalización en dominios desconocidos.
• Análisis de Ablación:
  • La eliminación del módulo de Ilustración causó una caída significativa en la corrección semántica (BEq+), confirmando que las definiciones por sí solas no bastan.
  • En problemas simples (MiniF2F-test), el contexto excesivo puede actuar como distractor, lo que sugiere la necesidad de estrategias de recuperación dinámicas (activar/desactivar recuperación según la necesidad).

5. Significado e Impacto

El trabajo de DRIFT es significativo por varias razones:

• Puente entre Semántica y Sintaxis: Resuelve el problema de que los LLMs pueden encontrar definiciones correctas pero no saben cómo aplicarlas sintácticamente, un problema común en la formalización matemática.
• Generalización Fuerte: Al depender de la recuperación dinámica en lugar del conocimiento estático del modelo, DRIFT es robusto ante la obsolescencia de las bibliotecas formales y capaz de manejar dominios matemáticos nuevos (OOD) donde los modelos pre-entrenados fallan.
• Dirección Futura: El estudio sugiere que los futuros sistemas de demostración de teoremas automatizados deben ser agentes adaptativos que puedan juzgar cuándo recuperar información externa y cuándo confiar en su conocimiento interno, iterando basándose en la retroalimentación del compilador.

En resumen, DRIFT representa un avance fundamental al tratar la autoformalización no como una simple traducción, sino como un proceso de descomposición de consultas, recuperación de dependencias precisas y aprendizaje contextual a través de ejemplos, logrando así una mayor precisión y robustez en la generación de teoremas formales verificables.