TAO: Tolerance-Aware Optimistic Verification for Floating-Point Neural Networks

Il paper presenta TAO, un protocollo di verifica ottimistica e tollerante agli errori per le reti neurali in virgola mobile che, combinando limiti teorici e profili empirici calibrati su hardware eterogeneo, garantisce l'integrità dei risultati senza richiedere hardware fidato o kernel deterministici, con un overhead trascurabile.

L'essenziale

Il Problema: "La Scatola Nera" nel Cloud

Immagina di voler far cucinare un piatto gourmet da uno chef famoso, ma non puoi andare nella sua cucina. Devi affidarti a un servizio di consegna a domicilio (il "Cloud" o le GPU).

• Il rischio: Lo chef potrebbe usare ingredienti di qualità inferiore, cambiare la ricetta, o usare un forno leggermente diverso che altera il sapore. Tu ricevi il piatto, ma non sai se è davvero quello che hai ordinato.
• Il problema tecnico: I computer moderni (le GPU) sono così veloci che fanno calcoli matematici in modo leggermente diverso a seconda di come sono organizzati. È come se due chef, usando la stessa ricetta, tagliassero le verdure in un ordine leggermente diverso: il risultato finale è quasi identico, ma non esattamente uguale al milligrammo. I metodi vecchi per verificare il lavoro richiedevano che il risultato fosse bit-per-bit identico (esattamente lo stesso), il che è impossibile su computer diversi o troppo lento e costoso.

La Soluzione: TAO (Il Controllo di Qualità "Intelligente")

TAO è un nuovo sistema che cambia le regole del gioco. Invece di chiedere che il piatto sia identico al 100% (cosa impossibile), chiede che sia buono e dentro i limiti di accettabilità.

Ecco come funziona, passo dopo passo:

1. L'Approccio "Ottimista" (La scommessa)

Immagina che lo chef (il "Proposer") ti invii il piatto dicendo: "Ecco il tuo piatto, è perfetto".

• Fase Ottimista: Il sistema assume che lo chef sia onesto. Se nessuno si lamenta entro un certo tempo (la "finestra di sfida"), il pagamento viene rilasciato e il piatto è considerato valido. Non serve ricontrollare tutto subito, il che lo rende velocissimo.

2. La Sfida (Se qualcosa non va)

Se un cliente o un controllore (il "Challenger") pensa che il piatto sia rovinato, può lanciare una sfida.

• Il Gioco della Ricerca: Invece di ricucinare tutto il piatto da capo (che richiederebbe tempo e soldi), TAO usa un gioco intelligente. Immagina di dividere la ricetta in 4 parti (antipasto, primo, secondo, dolce).
  • Il controllore ricontrolla solo l'antipasto. Se è perfetto, passa al primo.
  • Se trova un errore nel primo, si ferma lì e divide quella parte in 4 sotto-parti.
  • Si continua a dividere e restringere il campo finché non si trova l'unico ingrediente specifico (o il singolo passaggio di cottura) che è stato sbagliato.
  • Analogia: È come cercare un errore di battitura in un libro di 1000 pagine. Invece di rileggere tutto, si controlla metà libro, poi un quarto, poi un ottavo, fino a isolare la singola parola sbagliata.

3. Due Tipi di "Regole" per il Giudizio

Quando si arriva all'ingrediente sbagliato (il "foglio"), TAO usa due metodi per decidere se è un errore grave o solo una variazione normale:

• A. Il Limite Teorico (La regola rigida): Si calcola matematicamente quanto potrebbe variare un calcolo a causa della fisica dei computer. Se l'errore è enorme (es. lo chef ha usato zucchero al posto del sale), viene punito subito.
• B. Il Limite Empirico (La regola flessibile e precisa): Questo è il trucco di TAO. Hanno fatto esperimenti su migliaia di computer diversi per vedere quanto realmente varia un calcolo tra un modello e l'altro. Hanno scoperto che le variazioni reali sono migliaia di volte più piccole di quelle teoriche.
  • Analogia: Se la teoria dice che un orologio può sbagliare di 1 minuto al giorno, ma nella realtà tutti gli orologi di quel modello sbagliano solo di 1 secondo, TAO usa la regola dei "1 secondo". Se lo chef sbaglia di 30 secondi, viene punito. Se sbaglia di 0,5 secondi (una variazione normale del computer), viene assolto.

4. Il Giudice Finale (Il Comitato)

Se l'errore è così piccolo da essere vicino al limite, TAO chiama un piccolo "comitato" di altri chef onesti. Ognuno ricontrolla quel singolo passaggio. Se la maggioranza dice "È dentro i limiti", il piatto è valido. Se dicono "È fuori", lo chef viene punito.

Perché è Geniale?

1. Velocità: Non serve ricontrollare tutto il lavoro. Si controlla solo dove c'è il dubbio.
2. Flessibilità: Accetta che i computer moderni non siano perfetti, ma non accetta errori grossolani.
3. Sicurezza: Hanno provato a "imbrogliare" il sistema inserendo errori sottili per vedere se riuscivano a passare. Risultato: 0% di successo. Il sistema è così preciso che non si può ingannare senza farsi beccare.
4. Nessun Hardware Speciale: Non serve un computer speciale o costoso per verificare, basta un computer normale.

In Sintesi

TAO è come un controllore di qualità intelligente per l'intelligenza artificiale. Invece di dire "Se non è identico al 100%, è falso", dice: "Se è così vicino alla perfezione che nessun computer normale potrebbe fare diversamente, allora è vero. Se c'è un errore visibile o troppo grande, ti becco e ti punisco".

Questo permette di usare l'intelligenza artificiale su qualsiasi computer nel mondo (anche su GPU diverse) con la certezza che il risultato sia corretto, senza dover attendere ore per una verifica impossibile.

Sommario tecnico

1. Il Problema

L'outsourcing dell'addestramento e dell'inferenza delle reti neurali (ML-as-a-Service) su hardware di terze parti (cloud GPU, marketplace di inferenza, acceleratori edge) ha creato un problema critico di verificabilità.

• Opacità e Rischi: Gli utenti non possono verificare se il modello eseguito corrisponde a quello promesso, se gli input sono stati elaborati correttamente o se il servizio non è stato degradato silenziosamente (es. sostituzione del modello, quantizzazione non dichiarata, uscita anticipata).
• Non-determinismo Intrinseco: L'esecuzione in virgola mobile (IEEE-754) su acceleratori eterogenei è intrinsecamente non deterministica. A causa della non associatività dell'aritmetica in virgola mobile, del riordinamento delle riduzioni e della fusione degli operatori da parte dei vendor, lo stesso modello può produrre output leggermente diversi su hardware diverso o anche su esecuzioni ripetute sullo stesso hardware.
• Limiti delle Soluzioni Esistenti:
  • zkML (Zero-Knowledge Machine Learning): Troppo lento e costoso in termini di memoria per modelli floating-point reali; richiede spesso la conversione in campi finiti o fixed-point.
  • Replay Deterministico: Richiede librerie e kernel modificati, sacrificando le ottimizzazioni native dei vendor e le prestazioni.
  • TEE (Trusted Execution Environments): Spostano la fiducia sul vendor hardware e introducono overhead prestazionali.
  • Replicazione: Costosa e non scalabile per modelli di grandi dimensioni.

2. Metodologia: TAO

Il paper propone TAO, un protocollo di verifica ottimistica consapevole della tolleranza (tolerance-aware). L'idea centrale è accettare che l'output non debba essere bit-per-bit identico, ma deve rientrare in una regione di accettazione definita a livello di operatore, basata su limiti di errore giustificati.

Componenti Chiave:

1. Modelli di Errore Complementari:

   • Limiti Teorici IEEE-754: Calcolo dei limiti di arrotondamento nel caso peggiore per ogni operatore. Sono solidi e portabili, ma spesso troppo conservativi (lasciano un ampio margine di errore).
   • Soglie Empiriche Percentili: Profili di errore calibrati offline su diversi acceleratori (GPU). Questi profili catturano la distribuzione reale delle deviazioni tra hardware e sono molto più stretti (100-1000 volte più stretti dei limiti teorici) e specifici per il modello.

2. Gioco di Disputa Interattivo (Dispute Game):

   • Esecuzione Ottimistica: Un "proponente" (fornitore di calcolo) esegue il modello e pubblica un impegno crittografico (commitment) dell'output. Se non ci sono sfide entro una finestra temporale, il risultato è finale.
   • Localizzazione della Disputa: Se un "sfidante" rileva una discrepanza, avvia un gioco interattivo basato su un albero di Merkle. Il grafo di calcolo viene partizionato ricorsivamente (N-way partition) fino a isolare un singolo operatore (foglia) responsabile della discrepanza.
   • Guida delle Soglie: La selezione della partizione "offensiva" è guidata dalle soglie percentili empiriche, permettendo di navigare il grafo in modo deterministico nonostante la non-deterministicità dei float.

3. Adjudicazione a Livello Singolo (Leaf Adjudication):
   Una volta isolato l'operatore, la disputa viene risolta in due modi:

   • Controllo del Limite Teorico: Un controllo economico e verificabile (senza fiducia) che verifica se l'errore rientra nei limiti teorici IEEE-754.
   • Voto di Comitato Empirico: Se il controllo teorico è inconcludente (l'errore è dentro i limiti teorici ma potenzialmente fuori da quelli empirici), un comitato di piccoli nodi onesti esegue l'operatore e vota basandosi sulle soglie empiriche calibrate.

4. Implementazione:

   • Un runtime compatibile con PyTorch che strumentizza i grafi di calcolo, calcola i limiti in tempo reale e traccia i risultati intermedi.
   • Un coordinatore basato su Smart Contract Ethereum (testato su Holesky) che gestisce gli impegni, le finestre di sfida, i depositi (bond) e le penalità.

3. Contributi Chiave

1. Semantica per ML Verificabile: Formalizza la correttezza "tollerante" per programmi tensoriali, permettendo la verifica economica senza richiedere determinismo bit-per-bit.
2. Analisi degli Errori e Attacchi: Sviluppa modelli di errore duali (teorici ed empirici) e conduce uno studio completo su attacchi avversari adattivi, dimostrando che le perturbazioni ammissibili non si accumulano per creare errori a livello di task.
3. Risoluzione delle Dispute Efficiente: Progetta un gioco di disputa ancorato a Merkle che riduce il costo di verifica da un controllo dell'intero modello a un controllo di un singolo operatore.
4. Sistema End-to-End: Implementazione funzionante di un runtime PyTorch e contratti intelligenti, dimostrando la fattibilità in scenari di modelli aperti (open-model).

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su modelli rappresentativi (ResNet-152, BERT-large, Qwen3-8B, Stable Diffusion) e diverse GPU (A100, H100, RTX 4090, ecc.).

• Strettezza delle Soglie: Le soglie empiriche sono 100-1000 volte più strette dei limiti teorici worst-case per i modelli Transformer.
• Robustezza agli Attacchi:
  • Sotto le soglie empiriche, il tasso di successo degli attacchi avversari (ASR) è 0% anche quando le soglie sono allentate di un fattore 3.
  • I limiti teorici da soli lasciano una piccola finestra di vulnerabilità (fino al 2.4% di ASR su Qwen3-8B), giustificando l'uso del voto di comitato per i casi borderline.
  • Nessun falso positivo: le esecuzioni oneste non hanno mai innescato dispute.
• Overhead Prestazionale:
  • L'esecuzione ottimistica (happy path) ha un overhead trascurabile: 0.3% di latenza aggiuntiva su Qwen3-8B.
  • Non richiede memoria aggiuntiva oltre all'esecuzione nativa.
  • Il costo di on-chain per una disputa è di circa 2 milioni di gas (su Ethereum Holesky).
• Scalabilità: Il numero di round di disputa scala come $O(\log_N |V|)$, dove $N$ è la dimensione della partizione. Una partizione di 8-12 elementi minimizza il tempo di risoluzione.

5. Significato e Impatto

TAO rappresenta un cambiamento di paradigma nella verifica del Machine Learning:

• Riconciliazione di Scalabilità e Verificabilità: Permette di utilizzare l'hardware eterogeneo e le ottimizzazioni native dei vendor (mantenendo le prestazioni di produzione) senza sacrificare la trasparenza o la possibilità di ricorso.
• Indipendenza dal Vendor: Non richiede hardware fidato (TEE) né la riscrittura dei kernel per renderli deterministici.
• Applicabilità Reale: È la prima soluzione pratica che gestisce la non-deterministicità intrinseca delle GPU moderne, rendendo possibile un mercato decentralizzato di inferenza ML affidabile per modelli di grandi dimensioni (LLM) e modelli di diffusione, dove le soluzioni basate su zkML sono attualmente impraticabili.

In sintesi, TAO dimostra che è possibile costruire sistemi ML verificabili che rispettano la realtà fisica dell'hardware moderno, accettando piccole variazioni numeriche controllate invece di cercare un'impossibile esattezza bit-per-bit.