Resumen Técnico: La Brecha de Fidelidad en la Autoformalización de LLM

1. Definición del Problema: La Brecha de Fidelidad

Los sistemas modernos de autoformalización, que traducen matemáticas en lenguaje natural (NL) a asistentes de pruebas formales (por ejemplo, Lean 4, Isabelle/HOL), están actualmente limitados no por la fluidez de la traducción, sino por la fidelidad. Aunque una sentencia formal generada puede estar sintácticamente bien formada (pasar el typecheck) e incluso ser demostrable, puede codificar un teorema semánticamente distinto de la sentencia original en NL.

Los autores identifican esto como la brecha de fidelidad. A diferencia del código, donde las pruebas unitarias proporcionan un oráculo ejecutable, la formalización matemática carece de un puente directo entre el lenguaje natural (interpretado bajo convenciones tácitas) y la lógica formal (interpretada bajo la teoría de tipos dependientes). Las métricas de evaluación estándar —como las puntuaciones BLEU frente a una referencia, las verificaciones puntuales de expertos o el éxito del demostrador posterior— no logran detectar fallos "insidiosos" donde la formalización es fluida y demostrable, pero semánticamente errónea.

El artículo formaliza este problema mediante una distribución de interpretación ($D_N$), que representa el conjunto de sentencias formales que matemáticos competentes aceptarían como expresión de una dada sentencia en NL $N$. Una formalización candidata $F$ es $\epsilon$-fiel si es demostrablemente equivalente a $1-\epsilon$ de las sentencias en $D_N$. Los autores categorizan la deriva semántica en cuatro clases canónicas:

1. $\Delta\forall$ (Inversión de Cuantificadores): Intercambiar el orden de los cuantificadores (ej., $\forall x \exists y$ frente a $\exists y \forall x$).
2. $\Delta H$ (Omisión de Hipótesis): Eliminar una premisa, haciendo que la sentencia formal sea estrictamente más fuerte de lo pretendido.
3. $\Delta C$ (Generalización de la Conclusión): Fortalecer la conclusión de tal manera que $F \Rightarrow N$ pero $N \not\Rightarrow F$.
4. $\Delta T$ (Coerción de Tipos): Recodificación silenciosa de tipos (ej., $\mathbb{R} \to \mathbb{Q}$), que suele ser lo más difícil de detectar sintácticamente.

2. Metodología: Huella Digital de Demostrabilidad Bidireccional (BPF)

La contribución central es la Huella Digital de Demostrabilidad Bidireccional (BPF, por sus siglas en inglés), un marco de referencia libre que certifica la fidelidad comparando los "vecindarios de consecuencia" de la sentencia en NL y la formalización candidata.

2.1. El Mecanismo Central

BPF opera bajo la idea de que el significado de una sentencia se define por lo que implica y por lo que la implica.

• Huella Digital Directa ($\Phi^+_F$): El conjunto de sondas implicadas por el candidato $F$.
• Huella Digital Inversa ($\Phi^-_F$): El conjunto de sondas que implican a $F$.
• Equivalencia: Dos sentencias son semánticamente equivalentes si sus huellas digitales directas e inversas coinciden sobre un conjunto suficientemente rico de sondas.

El proceso implica:

1. Generación de Sondas: Sintetizar un conjunto de sondas semánticas ($P$) a partir de la sentencia en NL $N$.
2. Autoformalización: Convertir estas sondas en sentencias formales.
3. Verificación de Implicación: Utilizar un asistente de pruebas (Lean 4 + mathlib4) como oráculo para computar las relaciones de implicación entre $F$ y las sondas.
4. Comparación de Huellas Digitales: Comparar la huella digital del candidato contra la huella digital predicha derivada de $N$.

2.2. Componentes Clave

El marco introduce cuatro componentes novedosos para mejorar la detección y la eficiencia:

1. Generación de Sondas Contrafácticas (CPG):
   En lugar de un muestreo genérico, la CPG utiliza un procedimiento contrastivo. Genera mecánicamente "gemelos con deriva" ($N^D$) para cada una de las cuatro clases de deriva (por ejemplo, intercambiando cuantificadores). Luego, un LLM es instruido para generar sondas que distingan específicamente $N$ de $N^D$. Esto apunta a los modos de fallo específicos que el certificador pretende detectar.

2. El Espectro de Equivalencia ($E(F, N)$):
   Sustituye los veredictos binarios frágiles (Fiel/Derivado) por una puntuación continua en $[0, 1]$. Esta puntuación se calibra con anotaciones de expertos para definir tres regiones de decisión:

   • ACEPTAR (ACCEPT): $E \ge 0.93$
   • REVISAR (REVIEW): $0.78 \le E < 0.93$ (requiere triaje humano)
   • RECHAZAR (REJECT): $E < 0.78$

3. Asignación Adaptativa del Presupuesto de Sondas (APBA):
   Un enrutador de información teórica que asigna dinámicamente el "presupuesto de tácticas" (tiempo/coste de búsqueda de pruebas) limitado. La APBA selecciona sondas que maximizan la reducción esperada de la entropía respecto al estado de la deriva, en lugar de realizar un muestreo uniforme. Esto logra la misma tasa de detección con significativamente menos sondas.

4. Decodificación Guiada por la Fidelidad (FGD):
   Un bucle de retroalimentación donde las puntuaciones de BPF se utilizan como señal de recompensa durante el proceso de autoformalización. En una configuración de muestreo y reordenamiento (sample-and-rerank), los candidatos son puntuados por BPF. Si los mejores candidatos caen en las zonas de "REVISAR" o "RECHAZAR", la "sonda testigo" de mayor puntuación (la sonda específica que reveló la deriva) se introduce de nuevo al LLM como una pista contextual para reparar el error.

3. Garantías Teóricas

El artículo proporciona dos resultados teóricos principales:

• Teorema de Detección de Deriva: Demuestra que para cualquier clase de deriva $D$ específica, si el generador de sondas tiene una "tasa de capacidad de testimonio" ($\alpha$) distinta de cero, BPF puede detectar la deriva con una probabilidad de $1-\delta$ utilizando un presupuesto de sondas de $k \ge \frac{1}{\alpha} \log(1/\delta)$.
• PAC-Fidelidad: Establece que la clase de equivalencia de una sentencia en NL es aprendible a partir de $O(\log(1/\delta)/\epsilon)$ sondas, asumiendo que la distribución de las sondas puede dar testimonio de cualquier deriva alcanzable.

Los autores también reconocen limitaciones: BPF no puede detectar la deriva de convención (donde la notación cambia pero el contenido lógico permanece idéntico) y depende de la completitud del oráculo de pruebas (las pruebas incompletas pueden conducir a falsos negativos).

4. Resultados Experimentales

Los autores lanzaron DRIFTBENCH, un banco de pruebas de 2,183 pares NL/Lean 4 con etiquetas de deriva controladas a través de seis subcampos matemáticos.

Rendimiento de Detección:

• BPF + CPG detecta el 89.6% de las formalizaciones con deriva con una tasa de falsos positivos del 3.0%.
• Esto supera significativamente a los modelos de base:
  • Solo verificación de tipo (Typecheck only): 11.4% de detección.
  • Demostrabilidad (flag de no demostrable): 41.2% de detección.
  • Evaluador LLM (verificación directa de fidelidad): 63.3% de detección.
  • Back-translation: 58.9% de detección.
• APBA reduce el coste computacional (tiempo de ejecución) en 3.2× en comparación con el muestreo uniforme manteniendo las tasas de detección.

Impacto de FGD:
Al aplicarse como paso de post-procesamiento a un autoformalizador de vanguardia, FGD redujo la tasa de sentencias derivadas emitidas del 19.4% al 10.3% (una reducción relativa del 47%), principalmente mediante el re-prompting sobre errores de omisión de hipótesis y generalización de conclusiones.

5. Significación y Reivindicaciones

El artículo sostiene que la brecha de fidelidad es el principal cuello de botella para la autoformalización fiable a escala de librerías matemáticas completas. La importancia de este trabajo reside en:

1. Certificación sin Referencia: Proporciona un método para verificar la fidelidad sin requerir una formalización de "estándar de oro", que a menudo no está disponible.
2. Operacionalización de la Semántica: Desplaza el paradigma de evaluación desde la superposición sintáctica (BLEU) o la demostrabilidad hacia la semántica inferencial (vecindarios de consecuencia), alineándose con la semántica de la teoría de la prueba.
3. Escalabilidad: Al introducir APBA y el Espectro de Equivalencia, ofrece una herramienta de triaje práctica y rentable que puede priorizar la revisión de expertos humanos en lugar de reemplazarla.
4. Benchmarking: DRIFTBENCH se presenta como el primer benchmark con etiquetas de deriva controladas, permitiendo la evaluación sistemática de la fidelidad en lugar de solo la capacidad del demostrador.

Los autores posicionan a BPF no como una solución perfecta que elimina todos los errores (notando específicamente la limitación respecto a la deriva de convención), sino como un paso concreto hacia el cierre de la brecha de fidelidad, permitiendo la integración segura de la matemática generada por IA en librerías rigurosas.