Structural Sensitivity in Compressed Transformers: Error Propagation, Lyapunov Stability, and Formally Verified Bounds

Resumen Técnico: Sensibilidad Estructural en Transformers Comprimidos

1. El Problema

La inferencia de modelos de lenguaje grandes (LLM) está cada vez más limitada por el ancho de banda de memoria más que por la capacidad de cómputo, lo que ha impulsado el uso de técnicas de compresión como el pruning (poda), la cuantización y la factorización de bajo rango. Sin embargo, existe una brecha fundamental en el conocimiento: no se entiende cómo se propagan los errores de compresión a través de las capas del transformador ni qué propiedades estructurales gobiernan esta propagación.

Actualmente, los practicantes carecen de garantías formales sobre qué componentes son seguros de comprimir y cuáles no, dependiendo de pruebas empíricas exhaustivas para cada nuevo modelo. El artículo aborda la pregunta crítica: ¿por qué ciertos componentes son catastróficamente sensibles a la compresión mientras que otros son casi inmunes, y cómo se comporta el error a lo largo de la red?

2. Metodología

Los autores proponen un enfoque híbrido que combina análisis estructural, teoría de sistemas dinámicos y verificación formal:

• Mapeo de Sensibilidad Estructural: Se analiza la compresión a nivel de matriz individual (granularidad fina) en cinco arquitecturas (desde 117M hasta 8B parámetros). Se evalúan 468 matrices en GPT-2 Small y se miden los cambios en la perplejidad al comprimir componentes específicos (MLP, Q, K, V, etc.).
• Análisis de Estabilidad de Lyapunov: Se aplica la teoría de estabilidad de Lyapunov para modelar la propagación del error. Se define una función de energía de error relativo $V(t) = \|e_t\|^2 / \|h_t\|^2$. La hipótesis central es que las conexiones residuales (no solo la normalización de capa) contraen los errores si el estado oculto crece más rápido que el error ($\alpha > \beta$).
• Verificación Formal con Lean 4: Se formalizan diez teoremas en el asistente de pruebas Lean 4 para establecer límites de error por matriz para tres etapas de aproximación:
  1. Caché Semántica: Reutilización de salidas para entradas similares.
  2. Activación Escasa: Poda de pesos de menor magnitud.
  3. Aproximación de Bajo Rango: Truncamiento SVD.
     Estos teoremas se componen para proporcionar límites de error acumulativo sin marcadores "sorry" (no verificados).
• Living Inference Framework: Un sistema donde los límites de error se rastrean en cada paso de adelante (forward pass), permitiendo la adaptación dinámica.

3. Contribuciones Clave

1. Mapeo de Sensibilidad Jerárquica: Se descubre una jerarquía de sensibilidad consistente que abarca cinco órdenes de magnitud. La estructura crítica es:
   • Catastróficamente Sensible: Proyecciones de subida del MLP en capas tempranas (especialmente la capa 0). Comprimir solo la matriz de proyección de subida del MLP de la capa 0 en GPT-2 Small aumenta la perplejidad en 20,000 veces.
   • Poco Sensible: Proyecciones de valor (V) en la atención, que pueden comprimirse casi "gratis".
   • Jerarquía general: $mlp\_fc \gg Q > K > mlp\_proj > attn\_proj > V$.
2. Análisis de Estabilidad de Lyapunov: Se demuestra que las conexiones residuales contraen los errores geométricamente (en GPT-2 Small, $\rho_{max} = 0.96$), lo que explica por qué los errores no se acumulan catastróficamente a través de 12+ capas. Esto proporciona un límite 23 veces más ajustado que los límites lineales ingenuos.
3. Validación Trans-Arquitectónica: Se valida que la estabilidad de Lyapunov es necesaria pero no suficiente para la robustez.
   • Modelos con alta estabilidad (GPT-2 Small, $\rho < 1$) pueden degradarse mucho (120x) si carecen de redundancia estructural.
   • Modelos con inestabilidad moderada (LFM2-2.6B, híbrido conv-attention) pueden ser muy robustos (7x degradación) gracias a la redundancia arquitectónica.
4. Garantías Formales Verificadas: Diez teoremas verificados por máquina en Lean 4 establecen límites de error por matriz. Se probaron en 14,040+ configuraciones sin ninguna violación de los límites, confirmando que las garantías lineales son conservadoras incluso en el paso adelante no lineal completo.

4. Resultados Principales

• El "Abismo" de la Capa 0: Existe una transición de fase abrupta entre la capa 2 y la 3. Comprimir la capa 0 es catastrófico, mientras que comprimir capas medias tiene un impacto mínimo. Esto se debe a que la capa 0 actúa como un cuello de botella irreducible para la creación de características no lineales a partir de los embeddings.
• Comparación de Modelos:
  • GPT-2 Small: Totalmente contractivo ($\rho=0.96$), pero muy frágil ante la compresión uniforme (120x degradación).
  • Mistral-7B: Moderadamente inestable ($\rho=1.14$), pero robusto (11x degradación) debido a su mayor dimensión y redundancia.
  • Qwen3-8B: Muy inestable ($\rho=1.33$) y con embeddings atados, sufre una degradación masiva (42,922x).
  • LFM2-2.6B: Arquitectura híbrida que, a pesar de tener $\rho=1.12$, es la más robusta (7x degradación) gracias a la redundancia de sus capas convolucionales.
• Asignación de Presupuesto de Error: La asignación "greedy" (codiciosa) que protege las capas tempranas y comprime las tardes logra ahorrar un 24% de FLOPS con solo un 27% de aumento en perplejidad, superando a la compresión uniforme.
• Índice de Fragilidad de Compresión (CFI): Se propone una fórmula que combina la inestabilidad de Lyapunov y la penalización por ancho de dimensión para predecir la robustez de un modelo, logrando ordenar correctamente las arquitecturas probadas.

5. Significado e Impacto

• Fundamento Científico: El trabajo revela que la sensibilidad a la compresión no es un artefacto del método de poda (como Wanda o SparseGPT), sino una propiedad estructural intrínseca de los transformadores. Las capas MLP tempranas son críticas para la síntesis de características, mientras que las capas posteriores tienen alta redundancia.
• Guía para la Compresión: Proporciona una hoja de ruta para la compresión no uniforme: proteger estrictamente las proyecciones de subida del MLP en las primeras capas y comprimir agresivamente las proyecciones de valor y las capas medias/tardías.
• Verificación Formal en IA: Establece un nuevo estándar al proporcionar límites de error verificados matemáticamente para la inferencia de transformadores, cerrando la brecha entre la teoría de control (estabilidad de Lyapunov) y la práctica de aprendizaje profundo.
• Implicaciones de Diseño: Sugiere que las arquitecturas futuras deben considerar la "fragilidad de compresión" como un criterio de diseño, equilibrando la estabilidad de Lyapunov con la redundancia estructural para soportar modelos más eficientes.

En conclusión, el artículo demuestra que la compresión de transformadores no es un problema uniforme; es un paisaje estructural donde la ubicación y el tipo de componente determinan el éxito o el fracaso catastrófico, y que este comportamiento puede ser modelado, verificado y optimizado mediante herramientas formales y teoría de estabilidad.