FAME: Formal Abstract Minimal Explanation for Neural Networks

Ce papier propose FAME, une nouvelle méthode d'explications abductives formelles basée sur l'interprétation abstraite qui permet d'obtenir des explications minimales plus concises et plus rapides pour les grands réseaux de neurones, tout en offrant une procédure pour évaluer la qualité de ces explications par rapport à la solution optimale.

L'essentiel

🕵️‍♂️ FAME : Le Détective qui Révèle les Vrais Motifs de l'IA

Imaginez que vous avez un génie très intelligent (une Intelligence Artificielle ou IA) qui regarde une photo et dit : « C'est un chat ! ». Mais si vous lui demandez « Pourquoi ? », il reste silencieux. Il ne vous donne pas de raisons. C'est frustrant, surtout si cette décision est importante (comme pour une voiture autonome ou un diagnostic médical).

Le problème, c'est que l'IA a des milliards de « neurones » qui travaillent ensemble. Pour comprendre sa décision, on doit savoir quels pixels de l'image sont vraiment importants et lesquels sont du bruit inutile.

C'est là qu'intervient FAME (Formal Abstract Minimal Explanations). C'est une nouvelle méthode pour expliquer les IA, mais avec une approche révolutionnaire.

🧩 L'Analogie du Puzzle et du Tri

Pour comprendre comment FAME fonctionne, imaginons que l'image est un énorme puzzle de 10 000 pièces.

• Le but : Trouver le plus petit nombre de pièces possible qui suffit à dire « C'est un chat ».
• L'ancien problème : Les méthodes précédentes (comme VERIX+) étaient comme un détective qui enlève les pièces du puzzle une par une, dans un ordre précis.
  • Le problème : Si vous avez 10 000 pièces, et que vous devez les tester une par une, cela prend une éternité ! De plus, l'ordre dans lequel vous les testez change le résultat. C'est comme chercher une aiguille dans une botte de foin en la touchant pièce par pièce.

🚀 La Magie de FAME : Le Tri de Masse

FAME change la donne en utilisant deux astuces géniales :

1. Le « Tri de Masse » (Batch Freeing)

Au lieu de tester les pièces une par une, FAME utilise une loupe mathématique (appelée Interprétation Abstraite) capable de regarder des milliers de pièces en même temps.

• L'analogie : Imaginez que vous avez un tamis géant. Au lieu de vérifier chaque grain de sable, vous secouez le tamis. Si le tamis vous dit « Ces 5 000 grains ne servent à rien pour reconnaître le chat », vous les jetez tous d'un coup !
• FAME peut ainsi éliminer des centaines de pixels inutiles en une seule fraction de seconde, là où les anciennes méthodes mettraient des heures.

2. Le « Rétrécissement de la Zone de Chasse » (Domain Refinement)

Parfois, le tamis est un peu trop gros et laisse passer des pièces inutiles. FAME est malin : il rétrécit la zone de recherche.

• L'analogie : Imaginez que vous cherchez un trésor sur une plage. D'abord, vous cherchez sur toute la plage. Si vous ne trouvez rien, vous vous dites : « Bon, le trésor est probablement dans cette petite zone de 10 mètres ». Vous vous concentrez là-dessus, et votre « loupe » devient beaucoup plus précise.
• En réduisant la zone de perturbation, FAME affine sa recherche et trouve des explications encore plus petites et précises.

⚖️ Pourquoi est-ce si important ?

1. Vitesse Éclair : Sur des réseaux de neurones complexes (comme ceux qui reconnaissent des visages ou des voitures), FAME est des fois plus rapide que les méthodes actuelles. C'est comme passer de la marche à pied à un avion à réaction.
2. Explications Plus Courtes : FAME donne des explications plus concises. Au lieu de dire « Ce sont les pixels 1, 5, 12, 45, 89... », il dit « Ce sont juste les pixels 12 et 45 ». C'est plus facile à comprendre pour un humain.
3. Fiabilité Totale : Contrairement à d'autres méthodes qui donnent juste une « bonne idée » (statistique), FAME utilise des preuves mathématiques. Elle garantit à 100 % que si vous enlevez les pixels qu'elle a gardés, l'IA changera d'avis. C'est une certitude, pas une supposition.

🏁 En Résumé

FAME, c'est comme avoir un assistant de détective ultra-rapide qui ne perd pas de temps à tester chaque pièce du puzzle une par une. Il utilise des outils mathématiques puissants pour éliminer des milliers de pièces inutiles en un clin d'œil, puis affine sa recherche pour ne garder que l'essentiel.

Grâce à FAME, nous pouvons enfin comprendre pourquoi une IA prend une décision, même sur des modèles très complexes, et ce, beaucoup plus vite et plus simplement qu'auparavant. C'est un pas de géant vers des IA plus transparentes et dignes de confiance.

Résumé technique

Voici un résumé technique détaillé du papier de recherche "FAME: Formal Abstract Minimal Explanation for Neural Networks", publié à la conférence ICLR 2026.

1. Problématique

L'explicabilité des réseaux de neurones (XAI) repose souvent sur des méthodes statistiques ou heuristiques qui manquent de garanties formelles. À l'inverse, les méthodes d'explication formelle, basées sur la logique et la vérification (comme les explications abductives ou AXp), offrent des garanties mathématiques rigoureuses : un sous-ensemble de caractéristiques (features) est suffisant pour garantir la prédiction du modèle sous n'importe quelle perturbation dans un domaine défini.

Cependant, l'application de ces méthodes formelles aux grands réseaux de neurones se heurte à deux obstacles majeurs :

1. Coût computationnel prohibitif : La recherche d'explications minimales exactes nécessite des solveurs complexes (SAT, SMT, MILP) qui ne sont pas évolutifs (scalables) pour des architectures profondes.
2. Goulot d'étranglement séquentiel : Les méthodes existantes (comme VERIX+) dépendent d'un ordre de parcours (traversal order) des caractéristiques. Elles libèrent les caractéristiques irrelevantes une par une ou par petits groupes séquentiels, ce qui empêche une parallélisation efficace et rend le processus lent. De plus, déterminer un ordre optimal nécessite une connaissance préalable de l'importance des caractéristiques, créant une dépendance circulaire.

2. Méthodologie : Le Framework FAME

FAME (Formal Abstract Minimal Explanations) propose une nouvelle classe d'explications abductives fondées sur l'interprétation abstraite (Abstract Interpretation) pour surmonter ces limitations. L'approche repose sur deux phases principales illustrées dans la Figure 1 du papier :

A. Élagage Abstrait (Phase 1)

Au lieu de parcourir les caractéristiques séquentiellement, FAME introduit des domaines de perturbation dédiés et des certificats de lot (batch certificates).

• Certificat de Lot Abstrait (Abstract Batch Certificate) : Utilisant l'analyse de perturbation basée sur la relaxation linéaire (LiRPA), FAME calcule une borne supérieure conjointe sur la contribution d'un ensemble de caractéristiques. Si cette borne indique que l'ensemble peut varier sans changer la prédiction, tout le lot est libéré simultanément. Cela élimine le besoin d'un ordre de parcours.
• Formulation du Sac à Dos (Knapsack Formulation) : Le problème de sélection du plus grand ensemble de caractéristiques à libérer est formulé comme un problème de sac à dos multidimensionnel (MKP). Pour des raisons d'efficacité, FAME utilise une heuristique gloutonne (Greedy Heuristic) qui sélectionne itérativement les caractéristiques ayant le coût normalisé le plus faible par rapport aux contraintes de robustesse.
• Domaine de Perturbation Contraint par la Cardinalité : FAME introduit un domaine de perturbation $\Omega_m(x; A)$ qui limite le nombre de caractéristiques pouvant varier simultanément ($\ell_0$-norme). Ce domaine est raffiné de manière récursive : après avoir libéré un lot de caractéristiques, le domaine se resserre, permettant d'obtenir des bornes LiRPA plus précises et de libérer davantage de caractéristiques dans les itérations suivantes.

B. Raffinement Exact (Phase 2)

La phase d'élagage abstrait produit une explication minimale abstraite ($wAXp^A$), qui est une sous-estimation de la vérité (conservative) due à la sur-approximation de LiRPA.

• Pour garantir la minimalité exacte, FAME utilise une étape de raffinement final. Elle peut utiliser des attaques adverses pour identifier rapidement les caractéristiques nécessaires, suivie d'une vérification exacte (optionnellement via VERIX+ avec le solveur Marabou) uniquement sur les caractéristiques restantes.
• Une procédure mesure la "distance" entre l'explication abstraite et l'explication minimale vraie, quantifiant ainsi la qualité de l'approximation.

3. Contributions Clés

1. Première classe d'explications abductives abstraites : Introduction d'explications basées sur l'interprétation abstraite, permettant de traiter des réseaux de neurones haute dimension.
2. Élimination de l'ordre de parcours : Conception de domaines de perturbation et d'une procédure récursive qui libèrent simultanément de multiples caractéristiques irrelevantes via des certificats LiRPA, brisant le goulot d'étranglement séquentiel.
3. Garanties de qualité prouvables : Introduction d'une procédure pour mesurer le pire écart entre une explication abstraite minimale et une explication minimale réelle, combinant recherche adversaire et raffinement exact.
4. Évolutivité (Scalability) : Démonstration de la capacité de FAME à générer des explications formelles pour des architectures complexes (ex: ResNet sur CIFAR-10) là où les méthodes exactes échouent par timeout ou manque de mémoire.

4. Résultats Expérimentaux

Les auteurs ont évalué FAME sur des modèles Fully Connected (FC) et Convolutionnels (CNN) des datasets MNIST et GTSRB, ainsi que sur un modèle ResNet-2B (CIFAR-10), en comparaison avec l'état de l'art VERIX+.

• Taille des explications : FAME produit des explications plus compactes que VERIX+. Par exemple, sur MNIST-CNN, la taille de l'explication passe de ~160 (VERIX+) à ~122 (FAME raffiné).
• Temps d'exécution : FAME est considérablement plus rapide. Sur le modèle GTSRB-CNN, FAME génère une explication en 7,4 secondes contre 185 secondes pour VERIX+ (un gain de facteur ~25x).
• Performance de l'heuristique gloutonne : Comparée à la résolution exacte du problème de sac à dos (MILP), l'heuristique gloutonne offre un gain de vitesse de 9x à 12x pour une perte de qualité négligeable (écart moyen de moins de 9 caractéristiques).
• Évolutivité sur ResNet-2B : Sur l'architecture ResNet-2B (1024 pixels), les méthodes exactes ont échoué (timeout/mémoire). FAME a réussi à libérer en moyenne 476 pixels (environ 46% de l'image) grâce au raffinement récursif, démontrant sa capacité à gérer des modèles profonds.

5. Signification et Impact

Ce travail représente une avancée majeure pour l'explicabilité formelle des réseaux de neurones profonds.

• Bridging the Gap : Il comble le fossé entre les garanties formelles rigoureuses et la nécessité pratique d'évolutivité sur des modèles industriels.
• Changement de paradigme : En passant d'une approche séquentielle dépendante d'un ordre de parcours à une approche par lots (batch) basée sur l'interprétation abstraite et la contrainte de cardinalité, FAME ouvre la voie à l'application de la XAI formelle dans des environnements à haut risque (sécurité, régulation) où les modèles sont complexes.
• Généralité : Le framework est conçu pour être généralisable à d'autres tâches (régression, stabilité locale) et gère nativement les variables discrètes via des bornes d'intervalle.

En résumé, FAME démontre qu'il est possible d'obtenir des explications formelles, minimales et fiables pour des réseaux de neurones à grande échelle en combinant intelligemment l'approximation abstraite rapide et la vérification exacte ciblée.