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

1. Il Problema

L'inferenza dei grandi modelli linguistici (LLM) è sempre più limitata dalla larghezza di banda della memoria piuttosto che dalla potenza di calcolo. Sebbene tecniche di compressione come il pruning (potatura), la quantizzazione e la fattorizzazione a basso rango abbiano prodotto risultati pratici notevoli, rimane una domanda fondamentale irrisolta: come si propagano gli errori di compressione attraverso i livelli di un transformer e quali proprietà strutturali dell'architettura governano questa propagazione?

Gli attuali metodi mancano di garanzie formali su quali componenti siano sicuri da comprimere e quali no, rendendo necessario un approccio empirico esaustivo per ogni nuovo modello. Inoltre, non è chiaro perché alcuni componenti siano catastroficamente sensibili alla compressione mentre altri sembrano comprimibili "gratis".

2. Metodologia

Gli autori introducono un approccio chiamato "Living Inference" (Inferenza Vivente), che combina analisi strutturale, teoria della stabilità e verifica formale.

• Mappatura della Sensibilità Strutturale: È stata condotta un'analisi granulare a livello di singola matrice su 468 matrici del modello GPT-2 Small (e successivamente su altri 4 modelli). Ogni matrice è stata compressa singolarmente per misurare l'impatto sul perplexity (perplessità).
• Teoria di Stabilità di Lyapunov: Per spiegare la propagazione degli errori, gli autori applicano la teoria della stabilità di Lyapunov ai sistemi dinamici. Definiscono l'energia dell'errore relativo $V(t)$ come il rapporto tra il quadrato dell'errore e il quadrato dello stato nascosto. L'obiettivo è dimostrare che le connessioni residue contraggono l'errore facendo crescere lo stato nascosto più velocemente dell'errore stesso.
• Verifica Formale con Lean 4: Sono stati sviluppati 10 teoremi verificati da macchina utilizzando il linguaggio di prova Lean 4. Questi teoremi stabiliscono limiti di errore per-matrice per tre stadi di approssimazione componibili:
  1. Semantic Caching (Caching semantico).
  2. Sparse Activation (Attivazione sparsa).
  3. Low-Rank Approximation (Approssimazione a basso rango tramite SVD).
     Nessun teorema contiene marcatori "sorry" (proof incompleti), garantendo la correttezza matematica dei limiti teorici.
• Validazione Sperimentale: I risultati sono stati validati su 5 architetture diverse (da 117M a 8B parametri: GPT-2 Small/Medium, LFM2-2.6B, Mistral-7B, Qwen3-8B) su dataset come WikiText-103 e C4, con valutazioni fino a 51.200 token.

3. Contributi Chiave

1. Mappatura della Sensibilità Strutturale:

   • È stata scoperta una gerarchia di sensibilità stabile che copre cinque ordini di grandezza.
   • La gerarchia è: MLP up-projection (early layer) $\gg$ Q > K > MLP projection > attn projection > V.
   • Scoperta Critica: Comprimere da sola la matrice mlp_fc dello strato 0 (una sola matrice su 468) aumenta la perplexità di 20.000 volte. Al contrario, le proiezioni di valore (V) sono quasi immuni alla compressione.
   • Esiste un "dirupo" (cliff) di sensibilità tra lo strato 2 e lo strato 3: gli strati iniziali sono catastrofici, mentre quelli centrali sono molto più resilienti.

2. Analisi di Stabilità di Lyapunov:

   • È stato dimostrato che le connessioni residue (non la sola LayerNorm) sono responsabili della contrazione degli errori. L'errore viene contratto perché lo stato nascosto cresce più velocemente dell'errore ($\rho < 1$).
   • Questo meccanismo spiega perché gli errori non si accumulano in modo catastrofico attraverso i 12+ strati, fornendo un limite geometrico 23 volte più stretto rispetto ai limiti lineari ingenui.

3. Validazione Cross-Architettura e "Fragilità":

   • La stabilità di Lyapunov è necessaria ma non sufficiente. Ad esempio, GPT-2 Small è totalmente contrattivo ($\rho_{max} = 0.96$) ma degrada di 120x, mentre LFM2-2.6B (ibrido) ha un $\rho_{max} > 1$ ma degrada solo 7x grazie alla ridondanza architetturale.
   • Viene introdotto un Compression Fragility Index (CFI) che combina l'instabilità di Lyapunov e la ridondanza limitata dalla larghezza del modello per prevedere la resilienza alla compressione.

4. Garanzie Formali Verificate:

   • I 10 teoremi Lean 4 forniscono limiti di errore per-matrice senza violazioni in 14.040+ configurazioni di GPT-2 Small. Questo conferma che i limiti formali sui componenti lineari sono conservativi anche quando composti nell'intero passaggio in avanti non lineare.

4. Risultati Principali

• Sensibilità Estrema degli Strati Iniziali: La compressione uniforme fallisce catastroficamente. L'allocazione non uniforme è essenziale. La compressione dello strato 0 di GPT-2 Small porta a una perplexità di ~1,5 milioni, mentre gli strati centrali rimangono stabili.
• Confronto tra Modelli:
  • Mistral-7B: Molto robusto (degradazione 11x a 50% di pruning), grazie a una maggiore ridondanza e una soglia di catastrofe più alta.
  • Qwen3-8B: Collassa catastroficamente (42.922x di degradazione) nonostante dimensioni simili a Mistral, a causa di embedding vincolati (tied embeddings) e un alto fattore di amplificazione ($\rho_{max} = 1.33$).
  • GPT-2 Small: Degradazione di 120x, nonostante la piena contrazione di Lyapunov, a causa della sua rappresentazione compatta (768 dimensioni) che offre meno margine di ridondanza.
• Strategie di Allocazione: Una strategia "greedy" (avida) che comprime prima i componenti meno sensibili (proiezioni V, output attention) e protegge gli strati iniziali MLP permette di risparmiare il 24% di FLOPS con un aumento di perplexità del solo 27%.
• Validazione su Scala: I pattern di degradazione e la gerarchia di sensibilità sono stati confermati stabili su dataset di 51.200 token e su diversi domini (WikiText, C4), dimostrando che non sono artefatti di valutazione su piccola scala.

5. Significato e Implicazioni

Questo lavoro cambia il paradigma della compressione dei transformer da un approccio puramente empirico a uno strutturalmente guidato e formalmente verificato.

• Teorico: Dimostra che la sensibilità alla compressione è una proprietà intrinseca dell'architettura, non un artefatto del metodo di pruning. Rileva che lo strato iniziale del MLP agisce come un "collo di bottiglia" irreducibile per la creazione di caratteristiche non lineari.
• Pratico: Fornisce una mappa precisa per gli ingegneri su quali componenti proteggere durante la compressione, permettendo di ottimizzare il compromesso costo/qualità senza test empirici esaustivi.
• Sicurezza: L'uso di Lean 4 per verificare i limiti di errore offre un livello di garanzia sulla qualità dell'output che manca nelle attuali tecniche di stato dell'arte (come SparseGPT o Wanda), aprendo la strada a deployment di modelli compressi in contesti critici dove la correttezza deve essere garantita matematicamente.

In sintesi, il paper stabilisce che la compressione efficace richiede una allocazione non uniforme basata sulla sensibilità strutturale (proteggendo gli strati iniziali MLP) e sulla stabilità di Lyapunov, supportata da garanzie formali che assicurano che gli errori non si accumulino in modo incontrollato.