💻 computer science

Differential Zonotopes for Verifying Global Robustness of DNNs

Cet article introduit TwoSafe, un nouvel outil d'analyse statique utilisant des zonotopes de halo différentiels pour vérifier efficacement la robustesse globale des réseaux de neurones profonds, surpassant de manière significative les techniques de pointe existantes tant en précision qu'en extensibilité.

Auteurs originaux : Anagha Athavale, Samuel Teuber, Matteo Maffei, Ezio Bartocci, Dejan Nickovic, Georg Weissenbacher

Publié 2026-06-23

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Anagha Athavale, Samuel Teuber, Matteo Maffei, Ezio Bartocci, Dejan Nickovic, Georg Weissenbacher

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous ayez construit un robot très intelligent (un réseau de neurones profonds) qui prend des décisions importantes, comme identifier des particules dans une expérience de physique ou reconnaître si une personne marche ou est debout à partir de données de capteurs. Vous voulez être absolument certain que ce robot ne sera pas confus si les données d'entrée sont légèrement « bruitées » ou imparfaites — comme un bug de capteur ou une tache sur l'objectif d'une caméra.

Ce document traite d'une nouvelle façon super efficace de tester si ces robots sont assez « robustes » pour gérer ce bruit sans commettre d'erreur.

Voici la décomposition de leur travail en utilisant des analogies simples :

1. Le Problème : Vérifier chaque scénario possible

Habituellement, lorsque nous testons un robot, nous vérifions s'il fonctionne pour une image spécifique, puis nous vérifions s'il fonctionne pour cette même image avec un peu de bruit ajouté. C'est ce qu'on appelle la Robustesse Locale. C'est comme vérifier si un pont tient le coup lorsqu'une seule voiture passe dessus.

Mais les auteurs voulaient vérifier la Robustesse Globale. C'est beaucoup plus difficile. C'est comme demander : « Si n'importe quelles deux voitures passent sur le pont en même temps, et qu'elles sont proches l'une de l'autre, le pont tiendra-t-il toujours ? »

Le Défi : Vérifier chaque paire possible d'entrées, c'est comme essayer de compter chaque grain de sable sur une plage. Cela demande tellement de puissance de calcul que les outils plus anciens ne pouvaient gérer que de tout petits robots simples (avec très peu de « neurones »).

2. L'Ancienne Méthode vs La Nouvelle Méthode

L'Ancienne Méthode (L'approche par « Force Brute ») :
Les outils précédents essayaient de résoudre cela en vérifiant deux robots séparément, puis en soustrayant leurs résultats. Imaginez essayer de mesurer la différence entre deux coureurs en chronométrant leurs performances séparément, puis en faisant le calcul plus tard. Le problème est que la partie « calcul » introduit des erreurs, rendant le résultat trop vague pour être utile pour les grands robots.

La Nouvelle Méthée (L'approche « Pas à Pas ») :
Les auteurs ont créé un nouvel outil appelé TwoSafe. Au lieu d'exécuter les deux vérifications séparément, ils les exécutent ensemble, côte à côte, en parfaite synchronisation.

L'Analogie : Imaginez deux jumeaux participant à une course. Au lieu de les chronométrer séparément et de comparer les temps plus tard, vous les faites courir en se tenant la main (ou reliés par une corde). Vous mesurez la distance entre leurs mains pendant qu'ils courent.
L'Innovation : Ils utilisent une forme mathématique appelée Zonotope (pensez à un ballon flexible et multidimensionnel) pour suivre les jumeaux. Ils ont inventé une version spéciale appelée Zonotope à Halo Différentiel (Differential Halo Zonotope).
- Le « Halo » est comme une bulle de sécurité autour des jumeaux. Il leur permet de s'écarter légèrement (simulant le bruit/la perturbation) tout en maintenant une emprise serrée sur la distance exacte qu'ils peuvent parcourir. Cela évite les erreurs de « calcul vague » de l'ancienne méthode.

3. Une Règle plus Intelligente : La Faille de la « Confiance »

Le document introduit également une nouvelle règle pour définir ce qui constitue un « échec ».

La Règle Stricte (Asymétrique) : Si le robot voit une image claire d'un « Chien » (99 % sûr), et qu'un léger bruit le fait dire « Chat » (même s'il n'est sûr qu'à 10 %), la règle stricte dit : ÉCHEC. Peu importe que le robot soit incertain quant au label « Chat » ; il a changé d'avis, donc il est défaillant.
La Règle plus Intelligente (Symétrique) : Les auteurs disent : « Attendez une minute. » Si le robot voit un « Chien » (99 % sûr) et que le bruit le fait dire « Chat » (10 % de confiance), c'est en réalité acceptable ! Le robot dit essentiellement : « Je pense que c'est un Chien, mais si vous me forcez à deviner, je suis vraiment incertain concernant le Chat. »
- L'Analogie : Imaginez un agent de sécurité. S'il est sûr à 99 % qu'une personne est un employé, mais qu'un peu de brouillard le fait hésiter et dire « Peut-être un étranger ? » (avec une faible confiance), il ne devrait pas être licencié. Il ne devrait avoir des problèmes que s'il crie avec assurance « ÉTRANGER ! » alors qu'il s'agit en fait d'un employé.
- Cette nouvelle règle Symétrique permet de vérifier des robots beaucoup plus complexes car elle ignore les erreurs de « faible confiance » que les humains identifieraient ou ignoreraient naturellement.

4. Les Résultats : Monter en Échelle

Les auteurs ont testé leur nouvel outil, TwoSafe, sur des robots du monde réel utilisés dans :

La Physique des Particules (LHC) : Trier des particules dans un collisionneur massif.
La Reconnaissance de l'Activité Humaine (HAR) : Déterminer si une personne marche ou est assise à l'aide de capteurs portables.
Le Contrôle du Trafic Aérien (ACAS) : Prévenir les collisions d'avions.

Le Résultat :

Vitesse : TwoSafe était nettement plus rapide que les meilleurs outils précédents.
Taille : Alors que les anciens outils ne pouvaient gérer que de petits robots (environ 15 neurones), TwoSafe a vérifié avec succès des robots possédant 500 neurones et des entrées de 561 dimensions. C'est comme passer de la vérification d'un vélo à celle d'un énorme cargo.
Précision : Les anciens outils déclenchaient souvent des « Fausses Alertes » (pensant qu'un robot était cassé alors qu'il ne l'était pas) parce que leur mathématiques étaient trop imprécises. TwoSafe est beaucoup plus précis, prouvant la sécurité là où les autres échouaient.

Résumé

Le document présente un nouveau « harnais de sécurité » mathématique (les Zonotopes à Halo Différentiel) qui permet de tester si des systèmes d'IA complexes sont robustes face au bruit sur l'ensemble de leur plage de fonctionnement. En exécutant les tests de manière synchronisée et en adoptant une définition plus réaliste de la « confiance », ils ont réussi à vérifier des systèmes d'IA qui étaient auparavant trop grands et trop complexes à contrôler.

Résumé technique : Zonotopes différentiels pour la vérification de la robustesse globale des DNN

1. Énoncé du problème

Les réseaux de neurones profonds (DNN) sont de plus en plus déployés dans des domaines critiques pour la sécurité tels que les transports et la santé, où leur robustesse face aux perturbations d'entrée est essentielle. Bien que la robustesse locale (garantir que les prédictions ne changent pas pour de petites perturbations autour d'une entrée spécifique) soit une propriété de sécurité bien étudiée, la robustesse globale est une exigence nettement plus forte. La robustesse globale exige que pour toutes les paires d'entrées dans une certaine distance, les prédictions du modèle restent cohérentes.

Formellement, la robustesse globale est une propriété de 2-sécurité, nécessant la vérification d'une relation entre deux traces d'exécution universellement quantifiées plutôt qu'une seule trace. Cette complexité rend la vérification globale nettement plus difficile que la vérification locale. Les méthodes existantes pour la robustesse globale basée sur la confiance (qui restreignent les garanties aux prédictions à haute confiance pour éviter les frontières de décision) reposent sur des solveurs de satisfaisabilité spécialisés mais souffrent d'une faible scalabilité, étant actuellement limitées à des réseaux de seulement quelques dizaines de neurones.

2. Méthodologie

Le papier propose un nouveau cadre d'analyse statique basé sur les zonotopes à halo différentiel pour vérifier efficacement la robustesse globale.

2.1 Zonotopes à halo différentiel

L'innovation technique centrale est l'extension du domaine abstrait des zonotopes. Les zonotopes standards représentent des ensembles de points via un centre et une matrice de générateurs. Pour vérifier la robustesse globale, les auteurs doivent suivre simultanément deux exécutions du même DNN avec des entrées différentes.

Défi : Les adaptations naïves des zonotopes différentiels (utilisés précédemment pour la vérification d'équivalence de DNN où les entrées sont identiques) échouent pour la robustesse globale. L'initialisation des entrées comme étant identiques ou l'utilisation de générateurs entièrement indépendants conduit soit à l'imprécision (unsoundness), soit à une sur-approximation excessive (perte de précision).
Solution : Les auteurs introduisent des formes affines à halo différentiel. Ce codage distribue la borne de perturbation $\epsilon$ $ϵ$ sur deux générateurs :
1. Un générateur primaire partagé entre les deux exécutions pour maintenir la corrélation.
2. Des générateurs secondaires qui sont indépendants pour chaque exécution afin de modéliser la perturbation.
Mécanisme : Cette structure en « halo » permet d'encoder de manière saine et précise la condition selon laquelle deux entrées $x$ et $y$ se situent dans une boîte englobante $[l, u]$ et satisfont $|x - y| \le \epsilon$ . Le zonotope différentiel $\mathcal{Z}_\Delta$ suit la différence entre les exécutions en synchronisation, produisant des bornes plus serrées sur la divergence que la simple soustraction de zonotopes individuels.

2.2 Robustesse globale symétrique basée sur la confiance

Le papier identifie une limitation dans la définition existante de la robustesse globale basée sur la confiance (la variante asymétrique), qui exige qu'une entrée à haute confiance $x$ ne puisse pas être perturbée vers une classe différente $y$ , quel que soit le niveau de confiance de $y$ . Les auteurs soutiennent que cela est trop restrictif, car une perturbation menant à une prédiction différente à faible confiance est pratiquement acceptable (par exemple, déclenchant une révision manuelle).

Ils proposent une variante symétrique :

Définition : Pour toute paire d'entrées $x, y$ à une distance $\epsilon$ , si les deux sont classées avec une confiance supérieure à un seuil $\tau$ , elles doivent appartenir à la même classe.
Avantage : Cette relaxation admet une classe plus large de réseaux comme étant « robustes » tout en restant pertinente pour les applications de sécurité critique où les sorties à faible confiance sont gérées via des mécanismes de repli.

2.3 Algorithme de vérification

Le processus de vérification (implémenté dans l'outil TwoSafe) suit ces étapes :

Initialisation : Construction d'un zonotope à halo différentiel représentant l'espace d'entrée et les contraintes de perturbation.
Propagation : Propagation du zonotope à travers les couches du DNN. Pour les activations ReLU, la méthode introduit de nouveaux générateurs pour sur-approximer la non-linéarité, tout en maintenant la structure différentielle.
Vérification de la propriété : À la sortie, le système formule un problème de programmation linéaire (LP) pour vérifier s'il existe des paires de sorties où les classes diffèrent alors que les deux satisfont le seuil de confiance $\tau$ .
Raffinement : Si le contrôle est non concluant (en raison de la sur-approximation), l'algorithologie effectue une division de générateurs (generator splitting). Contraênment à la division d'entrées standard, celle-ci divise les générateurs du zonotope à halo différentiel pour affiner l'approximation sans perdre la couverture de l'espace de perturbation.

3. Contributions clés

Zonotopes à halo différentiel : Un nouveau domaine abstrait qui étend les zonotopes pour propager conjointement des paires d'entrées perturbées en synchronisation, encadrant étroitement leur divergence. Cela permet la vérification de propriétés de 2-sécurité avec une précision supérieure à l'analyse individuelle.
Robustesse globale symétrique basée sur la confiance : Une nouvelle définition de la robustesse globale qui n'exige la cohérence qu'entre les prédictions à haute confiance. Cette définition est strictement moins restrictive que la variante asymétrique et permet une vérification efficace au sein du cadre proposé.
Preuve de correction (Soundness) : Une preuve formelle de la correction de l'analyse statique basée sur les zonotopes différentiels, avec les résultats centraux formalisés dans Isabelle.
Outil TwoSafe et évaluation : Implémentation de l'approche dans un nouvel outil, TwoSafe, qui surpasse significativement l'état de l'art (baseline CGR) en termes de précision et de scalabilité.

4. Résultats expérimentaux

Les auteurs ont évalué TwoSafe sur quatre benchmarks : Law (petit), LHC (classification de particules), ACAS Xu (évitement de collision) et HAR (reconnaissance d'activités humaines).

Scalabilité : TwoSafe a vérifié avec succès la robustesse globale sur des réseaux comprenant jusqu'à 500 neurones ReLU et 561 dimensions d'entrée (benchmark HAR). En revanche, la baseline (CGR) a subi des dépassements de temps (timeout) ou l'épuisement de la mémoire sur ces réseaux plus larges.
Précision : La baseline a fréquemment rapporté des contre-exemples spécieux dus à des approximations grossières de la fonction softmax, particulièrement sur des réseaux avec de nombreuses classes de sortie. TwoSafe a évité ces faux positifs.
Performance : TwoSafe a démontré des accélérations significatives. Par exemple, sur le benchmark LHC, il a vérifié la robustesse en moins de 3 secondes là où la baseline s'est bloquée après 2 heures.
Symétrique vs Asymétrique : La propriété symétrique a permis une vérification réussie dans des régimes de paramètres où la propriété asymétrique était non concluante ou échouait. Par exemple, sur le benchmark HAR avec $\epsilon=0.01$ , la propriété symétrique était vérifiable tandis que la variante asymétrique s'arrêtait par timeout.

5. Signification et affirmations

Le papier affirme résoudre la tension inhérente entre la force des garanties de robustesse et la scalabilité des outils de vérification. En passant de la vérification de la robustesse locale à la globale et en utilisant des zonotopes à halo différentiel, les auteurs démontrent qu'il est possible de vérifier des réseaux nettement plus larges et profonds que ce qui était possible auparavant.

L'introduction de la robustesse globale symétrique basée sur la confiance est présentée comme une avancée pratique, offrant une « notion de robustesse significative » qui s'applique à une classe plus large de réseaux en reconnaissant que les prédictions à faible confiance sont souvent gérées différemment dans les systèmes réels. Ce travail établit que la vérification différentielle, lorsqu'elle est adaptée aux propriétés de 2-sécurité, peut passer à l'échelle pour des réseaux d'un ordre de grandeur plus grands que ceux traités par les techniques précédentes, rendant la certification de la robustesse globale réalisable pour des modèles déployés dans le monde réel.