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

Dit paper introduceert TAO, een tolerantiebewust, optimistisch verificatieprotocol voor floating-point neurale netwerken dat bitwise gelijkheid vervangt door operator-specifieke acceptatiegebieden om uitvoeringen op heterogene hardware te verifiëren zonder vertrouwde hardware of deterministische kernen.

De kern

Stel je voor dat je een beroemde chef-kok (het AI-model) huurt om een complexe maaltijd voor je te bereiden. Maar in plaats van in je eigen keuken te werken, stuur je de receptuur naar een groot, onbekend restaurant in de cloud. Je betaalt ze, en ze sturen je het bord terug.

Het probleem? Je weet niet zeker of ze:

1. Het juiste recept hebben gebruikt.
2. De ingrediënten niet hebben verwisseld.
3. Of dat ze misschien een goedkopere, minder lekkere versie hebben gemaakt om tijd te besparen.

In de wereld van kunstmatige intelligentie (AI) gebeurt dit constant. Bedrijven gebruiken dure, snelle computers (GPU's) van anderen om hun AI-modellen te laten werken. Maar omdat deze computers soms heel kleinste, onzichtbare verschillen maken in de berekeningen (zoals een kok die een snufje zout anders aftikt), is het bijna onmogelijk om te bewijzen dat het eindresultaat 100% hetzelfde is als wat er had moeten gebeuren.

TAO is de oplossing die deze auteurs hebben bedacht. Het is als een slimme, eerlijke inspecteur die niet eist dat het bord exact hetzelfde smaakt als het origineel (want dat is onmogelijk bij verschillende koks), maar wel controleert of het binnen de aanvaardbare smaakgrenzen valt.

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. De "Tolerantie" (De Smaakgrens)

Stel je voor dat je een taart bestelt. Als de bakker 1 gram suiker meer of minder gebruikt, proef je het verschil niet. Dat is tolerantie.

• Huidige problemen: Andere systemen eisen dat de taart exact hetzelfde is, gram voor gram. Dat is onmogelijk als de bakkers verschillende ovens gebruiken.
• TAO's oplossing: TAO zegt: "Het is oké als de taart iets zoeter of iets minder zoet is, zolang het binnen de wetenschappelijke grenzen van 'een goede taart' blijft." Ze hebben twee regels voor deze grenzen:
  • De Theorie: De wiskundige wetten zeggen: "Een taart kan maximaal X gram suiker afwijken." (Dit is een ruime grens).
  • De Realiteit: Ze hebben gemeten dat echte bakkers op echte ovens eigenlijk veel minder afwijken. Ze gebruiken een strakke, echte grens gebaseerd op wat er in de praktijk gebeurt.

2. Het "Optimistische" Spel (De Eerlijke Verwachting)

Stel je een restaurantketen voor waar iedereen eerst mag betalen en eten, en pas later wordt gecontroleerd.

• Het Optimisme: De AI-leverancier (de bakker) zegt: "Hier is je taart, ik heb het recept gevolgd." De klant betaalt.
• De Controle: Als de klant twijfelt, zegt hij: "Wacht even, ik denk dat je de suiker verkeerd hebt gedaan."
• De Winst: Als niemand twijfelt binnen een bepaalde tijd, is de taart goedgekeurd en krijgt de bakker zijn geld. Dit is heel snel en goedkoop.

3. Het "Merkel-Boek" en de "Zoektocht" (Het Oplossen van Twijfels)

Als er een ruzie ontstaat ("Deze taart smaakt niet goed!"), hoe vind je dan wie er fout zat? Je kunt niet de hele keuken afzoeken.

• De Oplossing: TAO gebruikt een slimme zoektocht. Stel je voor dat de taart uit 100 lagen bestaat.
  • De bakker zegt: "De eerste 50 lagen zijn goed."
  • De klant zegt: "Nee, in de eerste 50 lagen zit iets mis."
  • Ze verdelen de taart weer in tweeën: "Lagen 1-25?" "Nee." "Lagen 26-50?" "Ja, daar zit het!"
  • Ze blijven zo halveren (zoals het zoeken in een woordenboek) tot ze bij één enkele laag (één operatie) zijn gekomen.
• De Rechter: Bij die ene laag kijken ze heel nauwkeurig. Is de suiker hier binnen de strakke grens? Zo ja, dan is de bakker in orde. Zo nee, dan heeft hij bedrogen.

4. De "Jury" (De Eerlijke Mensen)

Soms is het heel lastig om te zeggen of een kleine afwijking "goed" of "slecht" is.

• In dat geval roept TAO een jury op. Dit zijn een paar andere onafhankelijke bakkers die dezelfde taart maken.
• Als de meerderheid van de jury zegt: "Ja, dit smaakt binnen de normale grenzen," dan wint de oorspronkelijke bakker.
• Als de meerderheid zegt: "Nee, dit is raar," dan heeft de bakker bedrogen en moet hij een boete betalen.

Waarom is dit belangrijk?

• Snelheid: Het is niet nodig om alles opnieuw te berekenen met superduurzame computers (zoals bij andere methoden). Het werkt met de normale, snelle AI-chips.
• Veiligheid: Zelfs als een hacker probeert de AI te manipuleren om een verkeerd antwoord te geven, lukt dat niet zonder dat de "tolerantie-grenzen" worden overschreden. De ruzie wordt dan snel opgelost.
• Eerlijkheid: Je kunt AI gebruiken op welke computer dan ook, zonder te vertrouwen op de leverancier. Als ze liegen, worden ze gepakt en gestraft.

Kortom: TAO is een slim systeem dat zegt: "We vertrouwen je niet blindelings, maar we vertrouwen ook niet dat alles perfect identiek moet zijn. We controleren of het resultaat 'goed genoeg' is binnen de regels van de natuurkunde, en als er twijfel is, vinden we de fout heel snel en straffen we de bedrieger."

Technische samenvatting

1. Het Probleem

Neurale netwerken worden steeds vaker uitgevoerd op hardware buiten de controle van de gebruiker (bijv. cloud GPU's, inferentie-marktplaatsen, edge-accelerators). Dit creëert een "ML-as-a-Service" (MLaaS) omgeving waar gebruikers geen inzicht hebben in wat er daadwerkelijk is uitgevoerd. Er is een risico op "stille degradaties" (silent downgrades), zoals:

• Vervanging van het model door een goedkopere variant.
• Ongeautoriseerde kwantisatie (verminderde precisie).
• Grafische herschrijvingen of het wijzigen van advertentie-embeddings.

De kernuitdaging: Bestaande verificatiemethoden zijn ongeschikt voor moderne floating-point (FP) neurale netwerken op heterogene hardware:

• zkML (Zero-Knowledge ML): Te traag en geheugenintensief voor realistische FP-modellen; vereist vaak kwantisatie naar vaste komma-getallen.
• Deterministische replay: Vereist het uitschakelen van vendor-optimalisaties en kernel-fusie, wat prestaties kost en hardware-heterogeniteit beperkt.
• TEE's (Trusted Execution Environments): Verplaatst het vertrouwen naar één leverancier (microcode) en introduceert prestatieverlies.
• Replicatie: Te duur voor grote modellen.

Bovendien is floating-point rekenen (IEEE-754) inherent niet-deterministisch. Dezelfde berekening op verschillende hardware of zelfs herhaald op dezelfde GPU kan lichtjes verschillende uitkomsten geven door niet-associativiteit en thread-scheduling. Bestaande systemen eisen vaak bit-identieke gelijkheid, wat onrealistisch is in productieomgevingen.

2. Methodologie: TAO

TAO (Tolerance-Aware Optimistic) is een verificatieprotocol dat niet eist dat de uitkomst bit-identiek is, maar dat deze binnen een principiële tolerantie valt. Het protocol combineert een optimistische uitvoering met een interactief geschillenmechanisme.

A. Twee Complementaire Foutmodellen

TAO gebruikt twee modellen om de aanvaardbare foutmarge te definiëren:

1. Theoretische IEEE-754 grenzen: Berekening van de worst-case afrondingsfout per operator (basis op de IEEE-754 specificatie). Deze is "sound" (veilig) maar vaak te conservatief (te ruim) voor diepe netwerken.
2. Empirische percentiel-drempels: Offline kalibratie van de foutverdeling van operators over verschillende hardware (GPU's). Deze drempels zijn veel strakker (100-1000x strakker dan theoretische grenzen) en specifiek voor het model en de operator.

B. Het Protocol (4 Fasen)

1. Setup (Phase 0): De model-eigenaar commit de gewichten, de grafiekstructuur (Merkle roots) en de ge-kalibreerde empirische fout-drempels.
2. Optimistische Uitvoering (Phase 1): Een "Proposer" (rekenkracht) voert het model uit op native hardware en post een commitment. Als er binnen een tijdsvenster geen uitdaging komt, wordt het resultaat definitief.
3. Geschillenlocalisatie (Phase 2): Als een "Challenger" een afwijking ziet die de empirische drempel overschrijdt, start een interactief spel.
   • De grafiek wordt recursief opgedeeld in subgrafen (N-weg partitionering).
   • De Challenger identificeert het eerste kind (subgraf) dat buiten de drempel valt.
   • Dit proces herhaalt zich totdat het geschil is gereduceerd tot één enkele operator (een "leaf" in de Merkle-boom).
4. Adjudicatie (Phase 3): Bij de laatste operator worden twee methoden gebruikt:
   • Theoretische check: Een snelle, goedkope verificatie of de uitkomst binnen de theoretische IEEE-754 grens valt.
   • Comité-stemming: Als de theoretische grens te ruim is (inconclusief), stemt een klein comité van onafhankelijke uitvoerders over de uitkomst tegen de strakke empirische drempels.

C. Technische Implementatie

• Runtime: Een PyTorch-compatible runtime die de grafiek instrumenteert, theoretische grenzen in real-time berekent en Merkle-commitments genereert.
• Coordinator: Een smart contract (geïmplementeerd op Ethereum Holesky testnet) dat de staat beheert, bonds (zekerheden) vasthoudt en straffen oplegt bij fraude.
• Overhead: De runtime voert ongewijzigde vendor-kernels uit in FP32. De overhead is verwaarloosbaar (0,3% extra latentie op Qwen3-8B).

3. Belangrijkste Bijdragen

1. Semantiek voor economisch verifieerbare FP-ML: Formalisatie van "tolerantie-bewuste correctheid" en een protocol dat economische finaliteit bereikt zonder determinisme.
2. Foutanalyse op operator-niveau: Ontwikkeling van een dubbel foutmodel (theoretisch + empirisch) en een uitgebreide studie van aanvalsmogelijkheden binnen deze grenzen.
3. Efficiënte geschillenoplossing: Een Merkle-geankerd spel dat geschillen reduceert tot één operator, waardoor goedkope adjudicatie mogelijk is zonder GPU-VM's.
4. Uitvoerbare systeem: Een volledige implementatie met PyTorch-runtime en Ethereum smart contracts, bewezen werkend voor CNN's, Transformers, LLM's en diffusion-modellen.

4. Resultaten en Evaluatie

De evaluatie omvatte modellen zoals ResNet-152, BERT-large, Qwen3-8B en Stable Diffusion op diverse GPU's (A100, H100, RTX 4090, etc.).

• Strakheid van drempels: Empirische drempels zijn 10² tot 10³ keer strakker dan theoretische worst-case grenzen voor Transformers.
• Aanvalssuccess (ASR):
  • Onder empirische drempels: 0% succes voor alle geteste modellen, zelfs bij een 3x versoepeling van de drempels.
  • Onder theoretische grenzen alleen: Kleine maar niet-verwaarloosbare kwetsbaarheid (tot 2,4% ASR voor Qwen3-8B), wat aantoont dat theoretische grenzen soms te ruim zijn voor grote modellen.
• Valse Positieven: Geen enkele eerlijke uitvoering leidde tot een geschil (0% false positives).
• Kosten:
  • Overhead: 0,3% extra latentie tijdens normale uitvoering.
  • Geschilkosten: Het bereiken van een "leaf" kost ongeveer 0,39x tot 1,24x de rekenkracht van een normale forward pass.
  • On-chain kosten: Ongeveer 2 miljoen gas per geschil op Ethereum Holesky.
• Vergelijking met zkML: TAO is orders van grootte sneller en geheugenefficiënter dan zkML voor floating-point inferentie, omdat het geen bewijsgeneratie vereist tijdens de normale uitvoering.

5. Betekenis en Conclusie

TAO lost het fundamentele conflict op tussen schaalbaarheid (native GPU-prestaties, heterogeniteit) en verifieerbaarheid (betrouwbaarheid) in ML-as-a-Service.

• Paradigmaverschuiving: In plaats van te proberen floating-point non-determinisme te elimineren (wat duur is), accepteert TAO het en verifieert het binnen wetenschappelijk onderbouwde toleranties.
• Praktische toepasbaarheid: Het stelt gebruikers in staat om modellen uit te voeren op elke hardware in de markt zonder in te leveren op integriteit, transparantie of recourse.
• Veiligheid: Het protocol is robuust tegen geavanceerde aanvallen (zoals gradient-based perturbations) die proberen binnen de foutmarges te blijven, aangezien kleine lokale afwijkingen niet natuurlijk cumuleren tot een taakniveau-fout.

Kortom, TAO biedt een haalbare, schaalbare en veilige oplossing voor verifieerbare machine learning in de echte wereld, waar hardware-heterogeniteit en floating-point variabiliteit de norm zijn.