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

Ce papier présente TAO, un protocole de vérification optimiste et tolérant aux erreurs qui garantit l'intégrité des inférences de réseaux de neurones flottants sur des matériels hétérogènes non fiables en acceptant des résultats dans des plages d'erreur définies et en utilisant un jeu de contestation hiérarchique, le tout sans nécessiter de matériel de confiance ni de noyaux déterministes.

L'essentiel

Imaginez que vous commandez un plat délicieux dans un restaurant très populaire, mais que vous ne pouvez pas entrer dans la cuisine. Vous ne savez pas si le chef a utilisé les ingrédients frais que vous avez payés, ou s'il a triché en utilisant des conserves bon marché, ou même s'il a changé la recette à votre insu.

C'est exactement le problème que rencontre l'intelligence artificielle (IA) aujourd'hui. Les entreprises font tourner leurs modèles d'IA sur des serveurs qu'elles ne contrôlent pas (dans le "cloud"). Elles reçoivent un résultat, mais elles ne peuvent pas être sûres à 100 % que le calcul a été fait correctement, sans triche, et avec le bon modèle.

Le papier que vous avez soumis présente TAO, une solution ingénieuse pour résoudre ce problème. Voici comment cela fonctionne, expliqué simplement avec des analogies.

1. Le Problème : La "Non-Exactitude" des Ordinateurs

Le premier défi, c'est que les ordinateurs modernes (les puces graphiques ou GPU) ne sont pas des machines parfaites.

• L'analogie : Imaginez que vous demandez à 100 comptables différents d'additionner une longue liste de nombres. Même s'ils sont tous honnêtes et utilisent la même calculatrice, il est possible que le 100e comptable ait un résultat qui diffère d'un centième de centime du 1er, simplement parce qu'ils ont additionné les nombres dans un ordre légèrement différent.
• La réalité : En IA, les calculs sont si complexes que deux machines différentes peuvent donner des résultats légèrement différents (par exemple, 0,123456789 vs 0,123456790). Les méthodes de vérification actuelles exigent que les résultats soient identiques au bit près (comme une empreinte digitale parfaite). Mais comme les machines font des "arrondis" différents, ces méthodes échouent ou sont trop lentes.

2. La Solution TAO : La "Tolérance Intelligente"

TAO change la règle du jeu. Au lieu de demander une copie parfaite, il demande un résultat suffisamment proche.

• L'analogie du "Cercle de Tolérance" : Imaginez que vous lancez une flèche sur une cible. Au lieu de dire "Tu as raté parce que tu n'as pas touché le centre exact", TAO dit : "Tu as gagné si ta flèche est dans le cercle rouge autour du centre". Ce cercle est calculé mathématiquement pour être sûr que le résultat est correct, même avec de petits arrondis.

TAO utilise deux types de "cercles" pour vérifier la vérité :

1. La Théorie (Le Cercle Large) : C'est une règle mathématique stricte (basée sur les normes IEEE-754) qui dit : "Même dans le pire des cas, l'erreur ne peut pas dépasser X". C'est sûr, mais le cercle est large.
2. L'Expérience (Le Cercle Étroit) : TAO a observé des milliers de fois comment les machines se comportent réellement. Il sait que, en pratique, les erreurs sont souvent 1000 fois plus petites que la théorie ne le prévoit. Il utilise donc un cercle beaucoup plus petit et précis pour vérifier.

3. Le Jeu de la "Chasse au Trésor" (Le Protocole de Dispute)

Si un utilisateur pense que le résultat est faux, il ne faut pas rejouer tout le jeu (ce qui prendrait des heures). TAO utilise un système de jeu interactif pour trouver la faute rapidement.

• L'analogie du "Trouver l'Intrus" : Imaginez un livre de 1000 pages. Si vous pensez qu'il y a une faute de frappe, vous ne relisez pas tout le livre.
  1. Vous divisez le livre en deux moitiés.
  2. Vous vérifiez quelle moitié contient la faute.
  3. Vous divisez cette moitié en deux, et ainsi de suite.
  4. En quelques étapes, vous avez isolé une seule page (voire une seule phrase) qui contient l'erreur.

Dans TAO, le "livre" est le réseau de neurones (le modèle d'IA). Si quelqu'un conteste le résultat, le système divise le calcul en petits morceaux jusqu'à ce qu'il ne reste qu'une seule opération (un seul calcul mathématique) à vérifier.

4. Le Juge Final (Le Comité)

Une fois qu'on a isolé le seul calcul suspect :

• Si l'erreur est énorme, le système la rejette immédiatement grâce à la "Théorie".
• Si l'erreur est petite mais douteuse, un petit comité d'experts (des ordinateurs honnêtes) rejoue juste ce petit calcul et vote. Si la majorité dit que le résultat est dans le "cercle de tolérance", c'est validé.

Pourquoi c'est génial ?

1. Pas besoin de confiance aveugle : Vous n'avez pas besoin de faire confiance au fournisseur de service. Le système prouve mathématiquement que le résultat est correct.
2. Pas de ralentissement : Contrairement aux méthodes actuelles qui ralentissent tout de 1000 fois (comme essayer de faire du calcul cryptographique complexe), TAO fonctionne à la vitesse normale des GPU. L'ajout de sécurité ne coûte que 0,3 % de temps en plus.
3. Adapté au monde réel : Il accepte que les machines fassent de petits arrondis, ce qui est inévitable, mais s'assure que ces arrondis ne changent pas le résultat final (par exemple, que l'IA ne confonde pas un "chat" avec un "chien" à cause d'un arrondi).

En résumé

TAO est comme un inspecteur de qualité ultra-rapide pour l'IA. Au lieu de demander une copie parfaite et impossible à obtenir, il vérifie que le résultat est dans la "zone de sécurité" acceptable. S'il y a un doute, il utilise un jeu de division rapide pour trouver la petite erreur, sans avoir besoin de relire tout le livre. Cela permet d'utiliser l'IA sur n'importe quelle machine, n'importe où, en toute sécurité et sans perdre de temps.

Résumé technique

1. Le Problème : La Vérification des Réseaux de Neurones sur du Matériel Hétérogène

L'industrie du Machine Learning (ML) s'oriente de plus en plus vers le "ML-as-a-Service" (MLaaS), où l'entraînement et l'inférence sont externalisés vers des infrastructures tierces (cloud, marchés d'inférence, accélérateurs spécialisés). Cela soulève un problème critique de confiance et de vérifiabilité :

• Opacité des services : Les utilisateurs ne peuvent pas vérifier si le modèle exécuté est bien celui promis, ni si les résultats reflètent fidèlement les entrées. Ils sont vulnérables à des dégradations silencieuses (remplacement de modèles, quantification non déclarée, réécriture de graphes).
• Non-déterminisme inhérent : L'exécution de réseaux de neurones sur des accélérateurs hétérogènes (GPU de différents fabricants) est intrinsèquement non déterministe. L'arithmétique à virgule flottante (IEEE-754) n'est pas associative ; les noyaux (kernels) des fournisseurs réorganisent les réductions et fusionnent les opérations, et l'ordonnancement des threads introduit des variations aléatoires.
• Échec des approches existantes :
  • zkML (Preuves à connaissance nulle) : Trop lentes et gourmandes en mémoire pour les modèles flottants réels ; nécessitent souvent une quantification ou une conversion en arithmétique de champ fini.
  • Rejeu déterministe : Nécessite de désactiver les optimisations matérielles natives, ce qui tue les performances.
  • Enclaves de confiance (TEE) : Réintroduisent la confiance envers un seul fournisseur de matériel et souffrent de limitations de performance.
  • Réplication : Coûteuse et peu évolutive pour les grands modèles.

2. Méthodologie : TAO (Tolerance-Aware Optimistic)

TAO propose un protocole de vérification optimiste et tolérant aux erreurs, conçu spécifiquement pour l'arithmétique à virgule flottante. Au lieu d'exiger une égalité bit à bit (impossible sur du matériel hétérogène), TAO vérifie que les résultats se situent dans des régions d'acceptation définies par des seuils d'erreur raisonnables.

A. Double Modèle d'Erreur

TAO combine deux modèles d'erreur complémentaires pour équilibrer rigueur et efficacité :

1. Bornes théoriques IEEE-754 : Des bornes de pire cas calculées pour chaque opérateur (nœud du graphe). Elles sont sûres (sound) mais souvent trop conservatrices (larges) pour les réseaux profonds.
2. Seuils empiriques de percentiles : Des profils d'erreur calibrés hors ligne sur divers matériels (GPU). Ils capturent la distribution réelle des écarts entre matériels pour chaque opérateur. Ces seuils sont beaucoup plus serrés (100 à 1000 fois plus précis que les bornes théoriques).

B. Protocole de Litige Interactif (Dispute Game)

Le système fonctionne en plusieurs phases sur une chaîne de coordination (ex: Ethereum) :

1. Exécution Optimiste : Un "Proposeur" exécute le modèle et publie un engagement (commitment) du résultat. Si aucun défi n'est émis dans une fenêtre de temps, le résultat est finalisé.
2. Localisation du Litige : Si un "Défieur" (Challenger) détecte une divergence dépassant les seuils empiriques, un jeu interactif est lancé.
   • Le graphe de calcul est divisé récursivement (partitionnement N-way) en sous-graphes.
   • Le défi est guidé par les seuils empiriques : le défieur identifie le premier sous-graphe dont la sortie dépasse le seuil toléré.
   • Ce processus réduit le litige de l'ensemble du modèle à un seul opérateur (une feuille du graphe) en $O(\log N)$ tours.
3. Arbitrage au Niveau de l'Opérateur (Adjudication) : Une fois l'opérateur fautif isolé, deux voies de vérification sont possibles :
   • Vérification théorique : Vérification rapide des bornes IEEE-754. Si le résultat est hors de cette borne large, le proposeur est sanctionné.
   • Vote de comité : Si la borne théorique est trop large (inconclusive), un petit comité d'entités honnêtes réexécute l'opérateur et vote en comparant les résultats aux seuils empiriques (plus stricts).

C. Implémentation

• Runtime PyTorch : Instrumente les graphes de calcul, calcule les bornes théoriques en temps réel et gère les traces intermédiaires.
• Contrats Intelligents : Gèrent les engagements, les fenêtres de défi, les dépôts de garantie (bonds) et les pénalités.
• Compatibilité : TAO fonctionne avec les noyaux (kernels) non modifiés des fournisseurs et préserve l'hétérogénéité du matériel.

3. Contributions Clés

1. Sémantique de vérification tolérante : Formalisation de la "correction" pour les programmes tensoriels flottants, remplaçant l'égalité exacte par des régions d'acceptation basées sur les erreurs d'arrondi.
2. Double modèle d'erreur : Introduction de profils de percentiles empiriques calibrés, combinés à des bornes théoriques, permettant une vérification à la fois robuste et précise.
3. Jeu de litige guidé par le seuil : Un protocole de localisation de litige qui réduit la complexité de la vérification d'un modèle entier à un seul opérateur, en utilisant des seuils empiriques pour guider la recherche de la divergence.
4. Système complet et évalué : Implémentation d'un runtime PyTorch compatible et d'une couche de coordination sur Ethereum (testnet Holesky), démontrant la faisabilité pratique.

4. Résultats Expérimentaux

Les évaluations ont été menées sur plusieurs modèles (ResNet-152, BERT-large, Qwen3-8B, Stable Diffusion) et matériels (A100, H100, RTX 4090, RTX 6000).

• Précision des seuils : Les seuils empiriques sont 100 à 1000 fois plus serrés que les bornes théoriques de pire cas pour les modèles de type Transformer.
• Résistance aux attaques :
  • Sous des attaques adverses adaptatives conçues pour contourner les seuils, le taux de réussite de l'attaque (ASR) est de 0% avec les seuils empiriques, même lorsque ceux-ci sont assouplis par un facteur 3.
  • À l'inverse, l'utilisation exclusive des bornes théoriques laisse une vulnérabilité (jusqu'à 2,4% d'ASR sur Qwen3-8B), confirmant que les bornes théoriques sont trop lâches pour détecter des perturbations malveillantes subtiles.
• Performance et Coût :
  • Surcharge négligeable : L'exécution optimiste ajoute seulement 0,3% de latence (sur Qwen3-8B) par rapport à une exécution native.
  • Coût de litige : La résolution d'un litige nécessite un coût de calcul (DCR) équivalent à environ 0,4 à 1,2 fois le coût d'une inférence complète, ce qui reste économiquement viable comparé aux preuves zkML.
  • Pas de surcharge mémoire : Aucun besoin de mémoire supplémentaire au-delà de l'exécution standard des sous-graphes.

5. Signification et Impact

TAO représente une avancée majeure pour la vérifiabilité du ML dans le monde réel :

• Réconciliation Échelle vs Vérifiabilité : Il résout le dilemme entre la nécessité de performances élevées (en utilisant du matériel hétérogène et des noyaux natifs) et la nécessité de confiance (vérification).
• Indépendance vis-à-vis du fournisseur : Il permet aux utilisateurs de déployer des modèles sur n'importe quel matériel du marché sans compromettre l'intégrité des résultats, éliminant le besoin de confiance envers un seul fournisseur de matériel (TEE) ou de logiciels.
• Adaptabilité aux contraintes réelles : En acceptant le non-déterminisme inhérent aux GPU plutôt que de tenter de l'éliminer (ce qui est coûteux), TAO offre une solution pragmatique pour les applications de ML critiques (finance, santé, publicité) où la transparence est requise mais où la précision bit à bit est impossible à garantir.

En résumé, TAO démontre qu'il est possible de construire des systèmes de ML vérifiables, économiques et performants en acceptant et en gérant mathématiquement les erreurs d'arrondi flottant, plutôt qu'en les combattant.