🤖 machine learning

Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism

Questo articolo adatta il Tensor Parallelism e il Fully Sharded Data Parallelism al framework di verifica $\alpha$ -CROWN per ridurre significativamente l'uso della memoria GPU, consentendo la verifica formale di reti neurali su larga scala come ResNet-large su CIFAR-100 che erano precedentemente impraticabili a causa dei vincoli di memoria.

Autori originali: Sergei Vorobyov, Eugene Ilyushin

Pubblicato 2026-06-09

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Sergei Vorobyov, Eugene Ilyushin

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di dover dimostrare che un'auto a guida autonoma non si schianterà mai, indipendentemente dalle condizioni meteorologiche o da come un pedone possa saltare improvvisamente sulla strada. Non puoi limitarti a testare l'auto un milione di volte; hai bisogno di una "dimostrazione" matematica che sia sicura in ogni possibile scenario. Questo è chiamato Verifica Formale delle Reti Neurali.

Il problema è che realizzare questa dimostrazione è estremamente pesante in termini di memoria del computer. È come cercare di risolvere un enorme puzzle, ma tutti i pezzi (i dati e le regole) devono stare su un unico, piccolo tavolo (una singola scheda grafica). Se il puzzle è troppo grande, il tavolo trabocca e la dimostrazione fallisce.

Questo articolo introduce due nuovi modi per risolvere questo puzzle usando più tavoli (GPU) che lavorano insieme, prendendo in prestito idee da come vengono addestrati i grandi modelli di IA oggi.

Ecco la suddivisione delle loro due soluzioni principali, spiegate con semplici analogie:

1. L'approccio "Dividi il Puzzle" (Parallelismo Tensoriale)

L'Idea: Immagina di avere un enorme puzzle a incastri. Invece di una sola persona che tiene tutto il puzzle, lo tagli a metà. La Persona A tiene la metà sinistra e la Persona B tiene la metà destra. Entrambi lavorano sui propri pezzi e si urlano i risultati a vicenda.

Come funziona: I ricercatori dividono i "pesi" (i pezzi del puzzle) e le "regole" (la matematica) tra due GPU.
La Buona Notizia: Questo riduce la memoria necessaria su ogni computer di quasi la metà (riduzione di circa 2x). È molto efficiente per puzzle piccoli o poco profondi.
Il Problema: Quando il puzzle diventa profondo (molti strati), le due persone devono indovinare la connessione tra le loro metà senza vedere l'immagine completa. Per risparmiare tempo, utilizzano un metodo di stima "veloce e approssimativo" (chiamato IBP) per le parti centrali.
Il Risultato: La dimostrazione finale è comunque sicura (non dirà che un'auto è sicura se in realtà è pericolosa), ma la risposta diventa un po' più "sfocata" o meno precisa man mano che il puzzle diventa più profondo. È come stimare la distanza da una montagna guardando l'orizzonte invece di misurarla esattamente.

2. L'approccio "Biblioteca Condivisa" (Parallelismo dei Dati Completamente Frammentato - FSDP)

L'Idea: Immagina una biblioteca dove i libri sono troppo grandi per stare su un singolo scaffale. Invece di copiare l'intero libro per ogni lettore, la biblioteca divide il libro in pagine.

Come funziona: I ricercatori dividono i "pesi" (le pagine del libro) tra le GPU.
Il Trucco Magico: Quando un computer deve fare un calcolo, raccoglie rapidamente tutte le pagine di cui ha bisogno dagli altri computer, esegue la matematica e poi mette immediatamente via le pagine. In ogni singolo momento, nessun computer sta trattenendo l'intero libro.
La Buona Notizia:
- Precisione Perfetta: Poiché la matematica viene eseguita esattamente nello stesso modo in cui verrebbe fatta se un solo computer avesse l'intero libro, il risultato è identico bit per bit alla versione a computer singolo. Nessuna "sfocatura".
- Risparmio di Memoria: Risparmia una enorme quantità di memoria (l'80–90% per la configurazione base, e il 34–39% per l'uso di picco).
Il Problema: Richiede un po' di "comunicazione" tra i computer per raccogliere le pagine, il che richiede un briciolo di tempo, ma il risparmio di memoria ne vale la pena.

La Grande Sorpresa: Cosa sta davvero Ingolfando la Memoria?

I ricercatori si aspettavano che i "pesi" (i pezzi del puzzle o le pagine del libro) fossero il problema principale. Si sbagliavano.

Una volta utilizzati questi nuovi metodi per liberare spazio per i pesi, hanno scoperto il vero collo di bottiglia: un tipo specifico di dato chiamato "tensori alfa".

L'Analogia: Immagina di risolvere il puzzle. I "pesi" sono i pezzi del puzzle, ma i "tensori alfa" sono i post-it che devi scrivere su ogni singolo pezzo per tracciare i tuoi progressi.
La Scoperta: Nella modalità di verifica più avanzata (dove controllano gli incidenti usando un metodo chiamato Branch-and-Bound), questi post-it occupano il 99% della memoria, non i pezzi del puzzle.
La Conclusione: Anche se hanno avuto successo nel dividere i pezzi del puzzle tra i computer, i "post-it" sono ancora troppo grandi per starci. Per risolvere i problemi più grandi (come verificare l'IA complessa per le auto a guida autonoma), il lavoro futuro dovrà capire come dividere anche quei post-it tra i computer.

Sintesi dei Risultati

Parallelismo Tensoriale: Ottimo per risparmiare memoria, ma rende la risposta leggermente meno precisa per le reti profonde.
FSDP: Mantiene la risposta perfettamente precisa e risparmia molta memoria. Ha verificato con successo un modello complesso di riconoscimento delle immagini (ResNet) che prima era troppo grande per essere controllato.
Il Futuro: La chiave per verificare persino le IA più grandi non è più solo dividere i pesi; si tratta di capire come dividere i "post-it" (tensori alfa) che tracciano il processo di verifica.

In breve, l'articolo mostra come usare più computer per verificare la sicurezza dell'IA, ma rivela anche che abbiamo ancora un grande ostacolo di memoria da superare prima di poter verificare i sistemi di IA più grandi e complessi.

Sintesi Tecnica: Scalare la Verifica di Reti Neurali con il Parallelismo Tensoriale e il Fully Sharded Data Parallelism

1. Definizione del Problema

La verifica formale delle reti neurali mira a dimostrare matematicamente che una rete soddisfi proprietà di sicurezza per tutti gli input all'interno di un dominio specificato. Sebbene gli algoritmi di propagazione dei limiti come IBP, CROWN e $\alpha$ -CROWN siano lo stato dell'arte per questo compito, la loro applicazione pratica è severamente limitata dalla memoria della GPU. Le implementazioni standard richiedono che le matrici dei pesi e le matrici di rilassamento lineare $A$ risiedano interamente su un singolo acceleratore. Per reti grandi (ad esempio, un singolo strato nascosto con larghezza $h=262.144$ ), le sole matrici dei pesi possono superare i 4 GB in float32, lasciando memoria insufficiente per le matrici $A$ , il batching o i tensori intermedi necessari per la verifica. Questo articolo affronta la necessità di rimuovere questo collo di bottiglia della memoria del singolo GPU, adattando le strategie di partizionamento dei parametri (parameter-sharding) dal training di modelli su larga scala al framework di verifica.

2. Metodologia

Gli autori adattano due tecniche di parallelismo — il Parallelismo Tensoriale (TP) e il Fully Sharded Data Parallelism (FSDP) — al framework di verifica auto LiRPA / $\alpha, \beta$ -CROWN.

2.1 Parallelismo Tensoriale (TP)

Il TP suddivide le moltiplicazioni matriciali all'interno di un singolo strato tra $P$ GPU.

Implementazione: Gli autori hanno implementato operatori personalizzati BoundLinearTP Col e BoundLinearTP Row. I pesi sono partizionati lungo le dimensioni di output (colonna) o di input (riga).
Meccanismo: In una coppia Column–Row, il calcolo è distribuito, richiedendo un'operazione di AllReduce per recuperare il risultato.
Limitazione: Quando si verificano attivazioni ReLU all'interno di una zona partizionata (tra gli strati Column e Row), il passaggio backward di CROWN richiede limiti intermedi per determinare le pendenze di rilassamento ( $\lambda_i$ ). Calcolare questi limiti esattamente richiederebbe una comunicazione inter-GPU ad ogni step. Per preservare la località, gli autori sostituiscono questi limiti intermedi con la più semplice Propagazione dei Limiti d'Intervallo (IBP). Ciò introduce un "effetto wrapping", causando una degradazione della precisione dei limiti (bound tightness) all'aumentare della profondità della zona partizionata.

2.2 Fully Sharded Data Parallelism (FSDP)

L'FSDP partiziona i tensori dei parametri equamente tra $P$ GPU, ma li ricostruisce per il calcolo.

Implementazione: Implementato con circa 100 righe di codice Python, l'FSDP sostituisce i tensori BoundParams con i loro shard. Prima del calcolo di uno strato, un AllGather assembla la matrice dei pesi completa; immediatamente dopo, il tensore completo viene liberato, mantenendo solo lo shard.
Meccanismo: Questo approccio garantisce che al massimo una matrice dei pesi completa risieda nella memoria della GPU in un dato istante. Fondamentalmente, l'FSDP non altera l'ordine o il tipo di operazioni aritmetiche; cambia semplicemente la posizione di archiviazione dei pesi.
Correttezza: Poiché l'aritmetica rimane identica alla baseline a singola GPU, l'FSDP produce limiti bitwise-identici ( $\Delta = 0$ ).
Integrazione: L'FSDP si integra perfettamente con la verifica completa ( $\beta$ -CROWN + Branch-and-Bound) e gli strati convoluzionali (BoundConv).

2.3 Setup Sperimentale

Gli esperimenti sono stati condotti su GPU NVIDIA A40 utilizzando PyTorch 2.x e la libreria auto LiRPA. Gli autori hanno introdotto un flag bab.force_synchronous per garantire confronti equi tra le modalità a singola GPU e distribuita, disabilitando il ridimensionamento automatico del batch e il pruning nel percorso a singola GPU, assicurando carichi di lavoro identici.

3. Contributi Chiave

Implementazione di TP per la Verifica: Gli autori hanno implementato il TP per auto LiRPA utilizzando operatori personalizzati, ottenendo una riduzione della memoria di picco di circa $2\times$ con $P=2$ . Hanno analizzato formalmente il compromesso, confermando che, sebbene la correttezza (soundness) sia preservata, la precisione dei limiti degrada con il numero di zone partizionate a causa della sostituzione con IBP.
Implementazione di FSDP: Hanno implementato l'FSDP per la propagazione dei limiti, ottenendo una riduzione della memoria baseline dell'80–90% e una riduzione della memoria di picco del 34–39% su MLP ampi. Fondamentalmente, questo metodo produce limiti bitwise-identici alla baseline a singola GPU.
Integrazione con la Verifica Completa: L'FSDP è stato integrato con successo con $\beta$ -CROWN e Branch-and-Bound (BaB), consentendo la prima verifica completa (risultato UNSAT) di un modello ResNet-large per CIFAR-100.
Identificazione del Collo di Bottiglia: Attraverso estesi esperimenti, gli autori hanno identificato che, in modalità $\alpha$ -CROWN + BaB, il principale collo di bottiglia della memoria non sono le matrici dei pesi, ma i tensori alpha per neurone (pendenze ReLU).

4. Risultati

4.1 Riduzione della Memoria

TP: Ha ottenuto un fattore di riduzione della memoria di picco di $\approx 1.985$ (vicino al teorico $P=2$ ) per un MLP ampio ( $h=262.144$ ).
FSDP:
- Memoria Baseline: Ridotta dell'80–90% in vari modelli, poiché vengono allocati solo gli shard prima del calcolo dei limiti.
- Memoria di Picco: Ridotta del 34–39% su MLP ampi ( $h \ge 4096$ ). Il risparmio è inferiore rispetto alla riduzione della baseline perché le matrici $A$ non partizionate (che scalano con il quadrato della larghezza) rimangono in memoria.

4.2 Accuratezza dei Limiti e Correttezza (Soundness)

TP:
- I modelli con una zona partizionata (senza ReLU intermedia) hanno raggiunto un accordo alla precisione di macchina ( $\sim 10^{-8}$ ) con il riferimento a singola GPU.
- I modelli con più zone partizionate hanno mostrato deviazioni significative (es. $\sim 750$ unità per un modello a 3 zone) a causa della sostituzione con IBP, sebbene la correttezza (sovra-approssimazione a senso unico) sia stata preservata.
FSDP:
- Ha ottenuto una deviazione esattamente pari a zero ( $\Delta lb = \Delta ub = 0.00$ ) in tutti i modelli testati (MLP e benchmark ONNX) sia per IBP che per CROWN.
- Ha verificato con successo un modello Transformer (ViT) e ResNet convoluzionali con risultati bitwise-identici alla baseline.

4.3 Verifica Completa (BaB)

In modalità $\beta$ -CROWN + BaB, il consumo di memoria è dominato dai tensori alpha (es. 1.5 GB per i tensori alpha contro 1.5 MB per i pesi in un particolare modello MNIST).

La partizione dei pesi tramite FSDP ha fornito un risparmio di memoria di picco trascurabile in questa modalità perché i tensori alpha non erano partizionati.
Tuttavia, l'FSDP ha permesso con successo la verifica di un modello ResNet-large (VNN-COMP 2024) che sarebbe altrimenti impossibile o difficile da gestire, confermando una proprietà UNSAT senza il branching di BaB.

5. Significato e Limitazioni

Il documento dimostra che le strategie di partizionamento dei parametri utilizzate nel training possono essere trasferite alla verifica formale con un modesto sforzo di ingegneria.

Significato: L'FSDP offre una via per verificare reti più grandi con limiti esatti, mentre il TP offre la massima riduzione di memoria a costo della precisione dei limiti per reti profonde. Il lavoro stabilisce che l'FSDP è compatibile con i requisiti complessi della verifica completa (BaB) e con diverse architetture (CNN, Transformer).
Limitazioni:
- Scalabilità: Gli esperimenti sono stati limitati a $P=2$ . Gli autori osservano che all'aumentare di $P$ , le matrici $A$ non partizionate diventeranno probabilmente il costo dominante, portando a rendimenti decrescenti.
- Precisione del TP: La degradazione della precisione dei limiti nel TP per reti profonde limita la sua utilità per la verifica precisa di architetture profonde.
- Spostamento del Collo di Bottiglia: Gli esperimenti rivelano che la futura ricerca sulla verifica multi-GPU deve concentrarsi sulla partizione dei tensori alpha per neurone, non solo sui pesi, per ottenere una scalabilità significativa nelle modalità di verifica completa.

Gli autori concludono che, sebbene l'FSDP risolva il collo di bottiglia dell'archiviazione dei pesi, il collo di bottiglia dei tensori alpha rimane la sfida critica per scalare la verifica completa verso modelli più grandi.