🤖 machine learning

Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

Cet article propose une suite d'algorithmes automatisés pour la découverte de circuits dans les réseaux de neurones, fondée sur des techniques de vérification formelle, qui garantissent de manière prouvable la robustesse, l'alignement et la minimalité des circuits découverts sur des domaines d'entrée continus.

Auteurs originaux : Itamar Hadad, Guy Katz, Shahaf Bassan

Publié 2026-02-20

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Itamar Hadad, Guy Katz, Shahaf Bassan

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 essayez de comprendre comment fonctionne une voiture de course très complexe, disons une Formule 1. Vous savez qu'elle va très vite, mais vous ne savez pas exactement pourquoi. Est-ce le moteur ? Les pneus ? Le système d'injection ? Ou une combinaison subtile de tout cela ?

Dans le monde de l'intelligence artificielle, les réseaux de neurones sont comme ces voitures de course. Ils sont incroyablement performants, mais souvent, personne ne sait exactement quelles pièces du moteur sont responsables de la prise de décision. C'est ce qu'on appelle l'interprétabilité mécanique.

Les chercheurs ont essayé de trouver ces "pièces clés" (appelées circuits) en faisant des expériences : ils éteignent aléatoirement certaines pièces (comme si on enlevait un boulon) et regardent si la voiture continue de rouler. Le problème ? Ces méthodes actuelles sont comme des tests de conduite sur un circuit de karting : elles fonctionnent bien sur un jour précis, mais si la météo change un tout petit peu (une petite perturbation), la voiture peut s'arrêter net. Les résultats ne sont pas fiables à 100 %.

Voici ce que propose cette nouvelle recherche, expliquée simplement :

1. Le Problème : Des cartes imprécises

Jusqu'à présent, les scientifiques dessinaient des cartes de ces circuits en se basant sur des échantillons. C'est comme essayer de dessiner la carte d'un pays en regardant seulement quelques photos prises par un drone. Si vous vous déplacez d'un mètre, la photo ne correspond plus. Les circuits trouvés sont fragiles : une petite variation dans l'entrée (une image légèrement floue, un mot mal orthographié) peut faire planter le circuit.

2. La Solution : Un GPS avec "Garantie de Trajectoire"

Les auteurs de cette paper utilisent une technologie appelée vérification formelle. Imaginez que vous ne cherchez plus à deviner le chemin, mais que vous utilisez un super-GPS mathématique capable de prouver, avec une certitude absolue, que votre voiture restera sur la route, peu importe les petits virages ou les trous de la route.

Ils proposent trois types de garanties (comme trois ceintures de sécurité) :

Robustesse aux entrées (La route) : Le circuit fonctionne non pas juste sur une photo, mais sur toutes les photos possibles qui ressemblent à l'originale (même si elles sont un peu floues ou déformées). C'est comme dire : "Ce circuit est le moteur, et il fonctionnera même si la route est un peu cahoteuse."
Robustesse aux patchs (Le carburant) : Souvent, pour tester une pièce, on remplace le reste du moteur par du "carburant moyen" ou du "carburant nul". Les chercheurs disent : "Non, on ne veut pas de carburant moyen ! On veut prouver que le circuit fonctionne même si le reste du moteur reçoit n'importe quel carburant possible dans une fourchette réaliste." C'est une garantie beaucoup plus forte.
Minimalité (La légèreté) : Ils veulent trouver le circuit le plus petit possible. Imaginez que vous vouliez enlever le plus de pièces possible de la voiture tout en gardant la capacité de rouler. Ils ont créé des algorithmes pour trouver le "cœur" exact, sans aucune pièce superflue.

3. La Magie : Le "Jumeau Numérique" (Siamese Encoding)

Comment prouver tout cela sans tester des milliards de fois ? Ils utilisent une astuce géniale appelée encodage siamois.

Imaginez que vous avez deux jumeaux identiques :

Le Jumeau Original : La voiture complète.
Le Jumeau Circuit : La voiture avec seulement les pièces que vous suspectez d'être importantes.

Vous les faites rouler côte à côte sur la même route. Le but est de prouver mathématiquement que, peu importe la route (les perturbations) ou le carburant injecté dans le reste du moteur, les deux jumeaux arrivent exactement à la même destination en même temps. Si le jumeau "Circuit" suit parfaitement le jumeau "Original" dans toutes les conditions, alors vous avez la preuve absolue que ce circuit est le vrai moteur de la décision.

4. Le Résultat : Des circuits indestructibles

En utilisant cette méthode sur des modèles de vision par ordinateur (qui reconnaissent des images), les chercheurs ont montré que :

Les circuits trouvés par les anciennes méthodes (basées sur des échantillons) tombaient en panne dès qu'on changeait légèrement l'image.
Les circuits trouvés par leur méthode ne tombent jamais en panne dans les conditions testées. Ils sont 100 % fiables.
Ils sont aussi souvent plus petits et plus épurés, car l'algorithme a éliminé tout ce qui n'était pas strictement nécessaire.

En résumé

Cette recherche est comme passer d'une intuition de mécanicien ("Je pense que c'est ce boulon qui fait le bruit") à une preuve d'ingénieur ("Je vous garantis mathématiquement que ce boulon est la seule pièce nécessaire, et que la voiture roulera même si vous la secouez").

C'est une étape majeure pour rendre l'Intelligence Artificielle plus sûre, plus transparente et plus digne de confiance, car on ne se contente plus de deviner comment elle fonctionne, on le prouve.

1. Problématique

L'interprétabilité mécanistique (MI) vise à décomposer les réseaux de neurones en composants fonctionnels compréhensibles par l'humain, appelés circuits. Une tâche centrale est la découverte de ces circuits : identifier les sous-graphes du réseau responsables de comportements spécifiques.

Cependant, les méthodes actuelles souffrent de limitations majeures :

Nature heuristique : Elles reposent souvent sur des approximations ou des méthodes d'échantillonnage (sampling).
Absence de garanties formelles : La fidélité d'un circuit (c'est-à-dire sa capacité à reproduire le comportement du modèle complet) n'est généralement vérifiée que sur un ensemble discret de points d'entrée.
Fragilité : De petites perturbations continues (dans l'espace d'entrée ou lors de l'opération de "patching" des activations non-circulaires) peuvent briser la fidélité du circuit découvert.
Minimalité floue : Les notions de "circuit minimal" (le plus petit ensemble de composants suffisant) sont souvent mal définies ou non garanties.

L'objectif de cet article est de combler ce vide en proposant un cadre pour la découverte de circuits avec garanties prouvables sur des domaines continus.

2. Méthodologie

Les auteurs proposent un cadre algorithmique novateur qui intègre les avancées récentes en vérification formelle des réseaux de neurones (utilisant des solveurs comme $\alpha$ - $\beta$ -CROWN) pour certifier les propriétés des circuits.

A. Encodage Siamese pour la Certification

Pour vérifier la robustesse d'un circuit $C$ par rapport au modèle complet $G$ , l'article introduit une technique d'encodage Siamese :

Robustesse à l'entrée (Input-robustness) : Le modèle $G$ et le circuit $C$ (avec les composants non-circulaires fixés à une valeur de patching $\alpha$ ) sont dupliqués et empilés pour former un modèle combiné $G \sqcup C'$ . Cela permet de vérifier formellement que la différence entre les sorties de $G$ et $C$ reste inférieure à un seuil $\delta$ sur tout un domaine continu d'entrée $Z$ .
Robustesse au patching (Patching-robustness) : Une variante de l'encodage Siamese est utilisée où les activations du circuit sont patchées avec les activations réelles du modèle complet générées par un domaine d'entrée perturbé. Cela garantit que le circuit reste fidèle même si les activations non-circulaires varient continûment dans des limites réalistes.

B. Hiérarchie de Garanties de Minimalité

L'article formalise quatre notions de minimalité, de la plus faible à la plus forte, et propose des algorithmes pour les atteindre :

Quasi-minimalité : Le circuit est fidèle, et il existe au moins un composant dont la suppression brise la fidélité.
Minimalité locale : Le circuit est fidèle, et la suppression de n'importe quel composant individuel brise la fidélité.
Minimalité par sous-ensemble (Subset-minimalité) : Le circuit est fidèle, et la suppression de n'importe quel sous-ensemble de composants brise la fidélité.
Minimalité cardinale (Cardinally-minimalité) : Le circuit est fidèle et possède le nombre absolu de composants le plus faible possible (optimum global).

C. Propriété de Monotonie et Dualité

Un apport théorique clé est l'établissement de la propriété de monotonie du prédicat de fidélité $\Phi$ . Si $\Phi$ est monotone (ajouter des composants ne brise jamais la fidélité), les algorithmes de recherche gloutonne convergent vers des circuits à minimalité par sous-ensemble.
Pour atteindre la minimalité cardinale (NP-difficile), les auteurs exploitent une dualité entre les circuits et les "ensembles bloquants" (blocking-sets). Ils utilisent des solveurs de Minimum Hitting Set (MHS) pour approximer ou trouver exactement les circuits cardinaux minimaux.

3. Contributions Clés

Contributions Théoriques :

Définition formelle de garanties de robustesse pour l'entrée et le patching sur des domaines continus infinis.
Preuve de liens théoriques profonds entre la robustesse (entrée/patching) et la monotonie, garantissant la convergence des algorithmes vers des circuits minimaux par sous-ensemble.
Établissement d'une dualité entre circuits et ensembles bloquants, permettant l'approximation efficace de circuits cardinaux minimaux via des solveurs MHS.

Contributions Empiriques :

Développement d'algorithmes automatisés (Algorithmes 1, 2, 3, 4) qui préservent les invariants de robustesse.
Implémentation d'un cadre d'évaluation utilisant l'encodage Siamese pour certifier les propriétés via des vérificateurs d'état de l'art ( $\alpha$ - $\beta$ -CROWN).
Expérimentation sur des modèles de vision (MNIST, CIFAR-10, GTSRB, TaxiNet) démontrant la supériorité de la méthode par rapport aux approches basées sur l'échantillonnage.

4. Résultats Expérimentaux

Les expériences comparent la méthode proposée ("Provably Robust") avec des approches standards basées sur l'échantillonnage ("Sampling-based") :

Robustesse de l'entrée : La méthode prouvée atteint 100% de robustesse sur les domaines continus testés, tandis que les méthodes par échantillonnage montrent des taux de robustesse très faibles (ex: 46,5% sur CIFAR-10, 19,2% sur MNIST). Les circuits prouvés sont légèrement plus grands mais garantissent une fidélité inébranlable face aux perturbations infinitésimales.
Robustesse du patching : De même, la méthode certifiée maintient une fidélité de 100% même lorsque les activations non-circulaires sont perturbées continûment, là où les méthodes classiques échouent (taux de robustesse < 60%).
Minimalité : L'analyse montre que les algorithmes itératifs convergent vers des circuits de taille raisonnable, tandis que la méthode MHS (Algorithm 2) permet d'approcher la taille minimale cardinale, offrant un compromis entre coût computationnel et optimalité.
Coût computationnel : La méthode prouvée est plus lente (plusieurs milliers de secondes contre quelques dixièmes de seconde pour l'échantillonnage) en raison de la complexité des requêtes de vérification, mais elle fournit des garanties que l'échantillonnage ne peut offrir.

5. Signification et Impact

Cet article marque une étape fondamentale dans l'interprétabilité mécanistique en passant d'une approche empirique et heuristique à une approche formelle et rigoureuse.

Sécurité et Fiabilité : En garantissant que les circuits découverts restent fidèles sur des domaines continus, l'article renforce la confiance dans l'utilisation de l'interprétabilité pour des applications critiques (sécurité, détection de biais).
Nouveau Paradigme : Il établit un pont solide entre la vérification formelle des réseaux de neurones et l'interprétabilité, ouvrant la voie à des méthodes d'explication "formellement vérifiables".
Fondation Théorique : La caractérisation des différentes notions de minimalité et leur lien avec la monotonie offre un cadre théorique solide pour les recherches futures, permettant de mieux comprendre les compromis entre la complexité computationnelle et la qualité des circuits découverts.

En résumé, ce travail démontre qu'il est possible de découvrir des circuits de réseaux de neurones avec des garanties mathématiques strictes, transformant l'interprétabilité mécanistique d'un outil d'observation en un outil de vérification fiable.