The FABRIC Strategy for Verifying Neural Feedback Systems

Ce papier présente la stratégie FaBRIC, qui comble le manque de recherches sur l'analyse de rétro-accessibilité dans les systèmes de feedback neuronal en intégrant de nouveaux algorithmes d'approximation arrière avec les techniques existantes d'analyse avant pour certifier ces systèmes avec une performance supérieure à l'état de l'art.

L'essentiel

🏗️ FABRIC : Le "Double Regard" pour sécuriser les robots intelligents

Imaginez que vous construisez un robot autonome (une voiture sans chauffeur, un drone, ou un bras robotique) qui prend ses propres décisions grâce à un "cerveau" fait de réseaux de neurones (une intelligence artificielle).

Le problème ? Comment être 100 % sûr que ce robot ne va pas faire de bêtise (comme percuter un piéton ou tomber d'une falaise) dans toutes les situations possibles ? C'est ce que les chercheurs appellent la vérification de sécurité.

Jusqu'à présent, les experts utilisaient principalement une méthode pour vérifier ces robots : ils regardaient l'avenir. C'est comme si vous preniez une voiture, vous la mettiez sur une route, et vous regardiez où elle pourrait aller dans les 10 prochaines secondes. C'est la analyse vers l'avant.

Mais il y a un gros hic : pour des systèmes complexes, regarder seulement vers l'avant est lent et imprécis. C'est comme essayer de prédire où atterrira une feuille qui tombe dans le vent en regardant uniquement le sol, sans jamais regarder le ciel.

L'article propose une nouvelle méthode appelée FABRIC (qui signifie Forward and Backward Reachability Integration for Certification). En gros, c'est une stratégie qui combine deux points de vue : l'avenir et le passé.

---

🔄 Le concept : Regarder dans les deux sens

Pour comprendre FABRIC, imaginons que vous devez vous assurer qu'un voyageur peut aller de son point de départ (la maison) à sa destination (le travail) sans jamais passer par une zone de danger (un trou dans la route).

1. La méthode classique (Vers l'avant)

On part de la maison et on imagine tous les chemins possibles que le voyageur pourrait emprunter.

• Le problème : Si le voyageur a des milliers de choix à chaque carrefour, le nombre de chemins possibles explose. On finit par dire "Bon, on ne sait pas trop, ça pourrait être dangereux", même si en réalité, il n'y a pas de danger. C'est trop prudent et ça prend trop de temps.

2. La nouvelle méthode (Vers l'arrière)

Au lieu de partir de la maison, on part du travail (la destination sûre) et on regarde en arrière : "D'où le voyageur a-t-il pu venir pour arriver ici en sécurité ?"

• C'est comme si on traçait un chemin depuis la destination vers le départ.
• Le défi : C'est mathématiquement très difficile à faire avec des "cerveaux" d'IA (réseaux de neurones), un peu comme essayer de remonter le courant d'une rivière très turbulente.

3. La stratégie FABRIC : La réunion des deux

FABRIC dit : "Pourquoi ne pas faire les deux en même temps ?"

• On regarde vers l'avant depuis la maison pendant un certain temps.
• On regarde vers l'arrière depuis le travail pendant un certain temps.
• Si les deux zones de sécurité se rencontrent au milieu, alors c'est gagné ! On a prouvé qu'il existe un chemin sûr.

C'est comme si deux équipes de sauveteurs partaient de deux extrémités d'un tunnel pour se rejoindre au milieu. Si elles se touchent, le tunnel est sûr.

---

🛠️ Comment ça marche techniquement (sans les maths) ?

Les chercheurs ont dû inventer de nouveaux outils pour rendre cette "marche en arrière" possible et rapide. Ils ont utilisé deux types d'outils magiques :

1. Les "Boîtes de sécurité" (Approximations extérieures) :
   Imaginez que vous voulez savoir si un chat (le robot) peut entrer dans une boîte. Pour être sûr qu'il peut entrer, vous dessinez une boîte géante autour de lui. Si la boîte géante ne touche pas le mur, alors le chat est sûr.

   • Les chercheurs ont créé des algorithmes pour dessiner ces boîtes géantes très rapidement, même si le chat fait des mouvements bizarres (non-linéaires).

2. Les "Zones de certitude" (Approximations intérieures) :
   Maintenant, pour être sûr que le chat ne peut pas sortir d'une zone sûre, on dessine une petite boîte à l'intérieur. Si le chat est dedans, on est certain qu'il est en sécurité.

   • Ils ont inventé trois nouvelles façons de trouver cette petite boîte intérieure :
     • SHARP : On prend la grande boîte et on la rétrécit un peu à chaque fois jusqu'à ce qu'elle soit parfaite.
     • CRISP : On lance des milliers de fléchettes (des échantillons) dans la grande boîte. Si une fléchette atterrit dans une zone sûre, on garde cette zone. On essaie de trouver la plus grande forme possible avec ces points sûrs.
     • CLEAN : On cherche la plus grande zone possible qui ne contient aucune fléchette dangereuse.

---

🏆 Les résultats : Pourquoi c'est génial ?

Les chercheurs ont testé leur méthode sur des robots virtuels (une voiture, un drone, un chariot).

• Avant (Méthode ancienne) : Pour vérifier un drone complexe, il fallait des heures, et souvent, l'ordinateur plantait (il ne trouvait pas de réponse).
• Avec FABRIC :
  • C'est beaucoup plus rapide (parfois 10 à 40 fois plus rapide !).
  • C'est plus précis. Au lieu de dire "Ça pourrait être dangereux", ils peuvent dire "Oui, c'est sûr".
  • Sur les cas les plus difficiles, FABRIC a réussi là où les autres échouaient.

💡 En résumé

Imaginez que vous devez traverser une forêt obscure.

• L'ancienne méthode consistait à avancer pas à pas en allumant une lampe torche, mais la forêt était si grande que vous ne voyiez jamais la sortie.
• La méthode FABRIC, c'est comme envoyer deux équipes : une qui avance depuis l'entrée avec une lampe, et une autre qui part de la sortie en traçant des balises vers l'arrière. Quand les deux équipes se rencontrent, vous savez exactement quel chemin est sûr, et vous y êtes arrivé beaucoup plus vite.

C'est une avancée majeure pour rendre les voitures autonomes et les robots plus sûrs, car cela permet de prouver mathématiquement qu'ils ne feront pas de mal, même dans des situations imprévues.

Résumé technique

1. Problématique

Les systèmes dynamiques contrôlés par des réseaux de neurones, appelés systèmes de rétroaction neuronale (NFS), deviennent omniprésents dans la robotique et les systèmes autonomes. Garantir leur sécurité (respect des spécifications de "reach-avoid" : atteindre un objectif tout en évitant les états dangereux) est critique.

La vérification formelle de ces systèmes repose souvent sur l'analyse de reachabilité. Cependant, la majorité des travaux actuels se concentrent sur l'analyse forward (calcul des états futurs à partir d'un état initial). L'analyse backward (calcul des états passés pouvant atteindre un objectif ou une zone interdite) est beaucoup moins exploitée pour les NFS, principalement en raison de :

• La difficulté de propager des ensembles d'états à travers un réseau de neurones (surtout avec des fonctions d'activation non linéaires comme ReLU).
• La complexité accrue lorsque les dynamiques du système sont non linéaires.
• Le manque d'évolutivité (scalabilité) des techniques existantes pour les systèmes non linéaires.

L'objectif de ce travail est de combler ce vide en développant des algorithmes efficaces pour l'analyse backward et en les intégrant dans une stratégie de vérification hybride.

2. Méthodologie

Les auteurs proposent une approche combinant l'analyse forward et backward, baptisée FABRIC (Forward and Backward Reachability Integration for Certification).

A. Approximations des ensembles Backward

Pour les systèmes non linéaires, le calcul exact des ensembles backward est impossible. Les auteurs développent des méthodes pour calculer des sur-approximations (Outer Sets) et des sous-approximations (Inner Sets) :

1. Sur-approximation (Outer Sets / May-BRS) :

   • Utilisation d'enveloppes polyédriques (polyhedral enclosures) pour approximer les dynamiques non linéaires et le contrôleur neuronal.
   • Formulation du problème sous forme de Programmes Linéaires en Nombres Entiers Mixtes (MILP).
   • Extension de la raffinement de domaine (Domain Refinement) : Adaptation de l'algorithme DRIP (initialement pour des systèmes linéaires) aux systèmes non linéaires. L'algorithme DRiPy itère en affinant le domaine de recherche en utilisant les bornes calculées à l'étape précédente, réduisant ainsi la conservatisme des approximations.

2. Sous-approximation (Inner Sets / Must-BRS) :

   • L'objectif est d'identifier le plus grand sous-ensemble de l'ensemble "Outer" qui, une fois propagé vers l'avant, reste entièrement dans l'ensemble cible.
   • Trois algorithmes sont proposés pour résoudre ce problème d'optimisation :
     • SHARP (Scaled Hyperrectangular Approximation) : Réduit un hyperrectangle initial par une recherche linéaire itérative.
     • CRISP (Convex Rectangle Inferred via Sampled Positives) : Utilise un échantillonnage dense pour identifier les points "positifs" (valides) et construit l'hyperrectangle convexe maximal autour d'eux.
     • CLEAN (Constrained Local Exclusion of Aligned Negatives) : Gère les ensembles non convexes en excluant explicitement les points "négatifs" (invalides) via des variables binaires dans un MILP.
   • Ces méthodes sont intégrées dans un algorithme itératif (FITS) pour valider les candidats par des requêtes de reachabilité forward.

B. La Stratégie FABRIC

Au lieu de se fier uniquement à l'analyse forward ou backward, FABRIC divise l'horizon de temps $T$ en deux phases : $F$ étapes forward et $B$ étapes backward ($T = F + B$).

• Pour la propriété "Reach" (Atteindre un but) : On calcule l'ensemble reachable forward à l'étape $F$ et l'ensemble backward must-reachable à partir du but. Si l'ensemble forward est contenu dans l'ensemble backward, la propriété est vérifiée.
• Pour la propriété "Avoid" (Éviter le danger) : On vérifie que les ensembles forward ne croisent jamais l'ensemble des états dangereux, en utilisant l'analyse backward pour affiner les contraintes.
• Cette approche permet de réduire la charge computationnelle, car l'analyse backward est souvent plus coûteuse mais permet de réduire drastiquement l'espace d'états à considérer pour l'analyse forward.

3. Contributions Clés

1. Nouveaux algorithmes pour l'analyse backward : Définition d'algorithmes pour le calcul de sur-approximations (via DRiPy) et de trois nouvelles méthodes pour les sous-approximations (SHARP, CRISP, CLEAN) adaptées aux systèmes non linéaires.
2. Extension du raffinement de domaine : Adaptation de la technique DRIP aux dynamiques non linéaires, permettant de réduire significativement le conservatisme des bornes.
3. Stratégie FABRIC : Intégration novatrice des analyses forward et backward pour la certification des NFS, surpassant les approches unidirectionnelles.
4. Implémentation et Évaluation : Mise en œuvre complète et évaluation sur une suite de benchmarks représentatifs (ARCH Competition).

4. Résultats Expérimentaux

Les auteurs ont évalué leurs méthodes sur trois benchmarks (Carte TORA, Voiture Unicycle, Contrôle d'Attitude d'un avion) avec des contrôleurs de tailles variées.

• Sur-approximation (Outer Sets) :

  • L'algorithme DRiPy (avec raffinement) surpasse l'état de l'art (HyBReach-MILP) en termes de volume de l'ensemble (réduction de 3,5x à plus de 2900x selon le benchmark) et de temps de calcul.
  • Sur les problèmes complexes (Unicycle, Attitude), HyBReach-MILP échoue souvent par dépassement de temps (timeout), tandis que DRiPy fournit des résultats précis et rapides.

• Sous-approximation (Inner Sets) :

  • Les méthodes proposées (SHARP, CRISP, CLEAN) réussissent à trouver des ensembles internes certifiés là où l'outil concurrent BURNS échoue (ne trouve aucun ensemble de volume non nul) sur les benchmarks complexes à haute dimension.
  • CRISP se distingue comme la méthode la plus performante globalement.

• Stratégie FABRIC :

  • Sur les benchmarks difficiles (Unicycle), FABRIC offre un accélération allant jusqu'à 7x par rapport à l'analyse forward seule pour vérifier les propriétés de reach-avoid.
  • Sur les benchmarks simples (TORA), le coût de l'analyse backward peut dominer, rendant FABRIC moins efficace, mais cela reste acceptable.
  • Globalement, FABRIC réduit considérablement l'effort computationnel nécessaire pour la vérification formelle.

5. Signification et Impact

Ce travail est significatif car il adresse l'un des principaux goulots d'étranglement de la vérification des systèmes autonomes basés sur l'IA : la difficulté de l'analyse backward. En démontrant que l'analyse backward peut être rendue scalable et précise pour des systèmes non linéaires, les auteurs ouvrent la voie à des méthodes de vérification plus robustes.

La stratégie FABRIC démontre qu'une approche hybride (forward + backward) est souvent supérieure aux approches unidirectionnelles, offrant un compromis optimal entre précision et évolutivité. Cela renforce la confiance dans le déploiement de systèmes de rétroaction neuronale dans des environnements critiques pour la sécurité.

Les travaux futurs visent à optimiser davantage l'estimation des ensembles internes (pour lutter contre le fléau de la dimensionnalité) et à automatiser le choix du ratio entre les étapes forward et backward.