Résumé Technique : Vérification Exacte des Réseaux de Neurones à Graphes par Résolution Incrémentale de Contraintes

Énoncé du Problème

Les Réseaux de Neurones à Graphes (GNN) sont de plus en plus déployés dans des domaines à haut risque tels que la détection de fraude, la santé et la conduite autonome. Cependant, comme d'autres architectures neuronales, ils sont vulnérables aux attaques adverses où de légères perturbations des attributs des nœuds ou de la structure du graphe (ajout/suppression d'arêtes) peuvent modifier les prédictions. Bien que la vérification formelle offre une méthode rigoureuse pour prouver la robustesse, les techniques de vérification exacte existantes pour les GNN sont limitées. Plus précisément, les méthodes actuelles ne prennent principalement en charge que l'agrégation par somme et restreignent souvent les perturbations structurelles à la suppression d'arêtes uniquement. Elles ne prennent pas en charge d'autres fonctions d'agrégation courantes (max et moyenne) ni l'ajout d'arêtes, qui sont critiques pour modéliser des scénarios d'attaque réels et qui sont pris en charge par des bibliothèques standard comme GraphSAGE. De plus, les approches existantes ont souvent du mal à passer à l'échelle sur de grands graphes en raison de l'expansion rapide des encodages de contraintes.

Méthodologie

Les auteurs proposent GNNev, un outil de vérification exacte (sain et complet) pour les GNN à passage de messages. La méthode formule la tâche de vérification de la robustesse aux attaques adverses comme un Problème de Satisfaction de Contraintes (CSP) et la résout en utilisant la Programmation Linéaire en Nombres Entiers (MIP) avec des capacités de résolution incrémentale.

1. Encodage CSP

La tâche de vérification est encodée pour déterminer s'il existe une perturbation admissible (dans des budgets d'attributs et structurels spécifiés) qui provoque un changement de prédiction d'un nœud cible.

• Perturbation d'entrée : L'encodage modélise les perturbations d'attributs via des variables à valeurs réelles dans des bornes et les perturbations structurelles via des variables booléennes représentant les ajouts ou suppressions d'arêtes.
• Architecture GNN : Les couches du réseau sont encodées couche par couche. Les auteurs étendent les encodages MIP existants pour prendre en charge trois fonctions d'agrégation :
  • Somme : Encodée via des contraintes linéaires.
  • Max : Encodée en utilisant les capacités natives du solveur ou des contraintes big-M.
  • Moyenne : Encodée en utilisant des contraintes big-M pour gérer la division par le degré variable, qui change en fonction des perturbations d'arêtes.
• Objectif : L'objectif de vérification examine si la marge au pire cas entre la classe prédite et les autres classes peut être non positive (c'est-à-dire si une mauvaise classification est réalisable).

2. Stratégies de Resserrement des Bornes

Pour améliorer l'efficacité du solveur, les auteurs introduisent des stratégies spécialisées de resserrement des bornes pour les agrégations non linéaires (max et moyenne).

• Agrégation Max : La méthode calcule des bornes supérieures et inférieures serrées en analysant les cas où l'attaquant supprime des arêtes existantes ou en ajoute de nouvelles dans le budget. Elle utilise une sélection basée sur un tas (heap) pour identifier efficacement les $k$-ièmes bornes les plus grandes/petites.
• Agrégation Moyenne : Le problème est réduit à des sous-problèmes où les budgets de suppression et d'insertion sont fixés séparément. Les auteurs prouvent que les bornes pour ces sous-problèmes peuvent être calculées via des choix gloutons et exploitent l'unimodalité de la séquence résultante pour atteindre une complexité de $O((s+N)\log s)$, où $s$ est le budget et $N$ le nombre de variables.
• Garantie Théorique : L'article prouve que ces bornes dérivées sont serrées, ce qui signifie qu'il existe des ensembles de perturbations spécifiques qui atteignent ces bornes exactes.

3. Algorithme de Résolution Incrémentale

Pour résoudre le problème de passage à l'échelle où l'encodage du voisinage complet d'un nœud cible entraîne une explosion du nombre de variables, les auteurs emploient une approche de résolution incrémentale (Algorithme 1).

• Au lieu d'encoder l'ensemble du réseau de $K$ couches d'un coup, l'algorithme commence par l'objectif de vérification (couche finale) et ajoute itérativement des contraintes pour les couches précédentes ($K-1, K-2, \dots$).
• Il exploite les capacités de résolution incrémentale des solveurs MIP modernes (spécifiquement Gurobi), en réutilisant l'état de recherche et les coupes (contraintes redondantes) générées lors des itérations précédentes.
• Cette approche réduit considérablement la taille de l'encodage initial, en particulier pour les tâches de classification de nœuds où le nombre de voisins croît de manière exponentielle avec la profondeur.

Contributions Clés

1. Première Vérification Exacte pour les Agrégations Max/Moyenne : L'article introduit la première méthode de vérification exacte pour les GNN prenant en charge les fonctions d'agrégation max et moyenne, ainsi que la somme. Il conçoit des stratégies spécialisées de propagation de bornes resserrées pour ces fonctions non linéaires.
2. Résolution Incrémentale de Contraintes : Les auteurs proposent un algorithme qui encode les couches GNN à l'envers et utilise la résolution incrémentale pour accélérer les performances tout en maintenant l'exactitude. Cela est particulièrement efficace pour les tâches de classification de nœuds avec de grands voisinages.
3. Vérificateur Polyvalent (GNNev) : L'implémentation de GNNev, qui prend en charge à la fois la classification de nœuds et de graphes, gère les perturbations d'attributs et structurelles (y compris l'ajout d'arêtes) et s'intègre à PyTorch Geometric.
4. Évaluation Complète : L'outil est évalué sur des réseaux de citation standard (Cora, CiteSeer), des ensembles de données réels de fraude (Amazon, Yelp) et des ensembles de données biochimiques (MUTAG, ENZYMES).

Résultats Expérimentaux

• Comparaison avec les Baselines : Sur les GNN agrégés par somme avec suppression d'arêtes, GNNev surpasse SCIP-MPNN (le seul vérificateur exact basé sur MIP connu pour ce réglage) en temps d'exécution et en nombre de tâches résolues sur divers ensembles de données et budgets de perturbation. Par exemple, sur CiteSeer, GNNev a résolu des tâches difficiles pour lesquelles SCIP-MPNN a dépassé le temps limite.
• Performance d'Agrégation : GNNev vérifie avec succès les GNN avec agrégations max et moyenne. Les expériences montrent que, bien que l'agrégation max devienne plus difficile à calculer avec des budgets plus grands (en raison des défis de l'encodage big-M), l'outil reste efficace.
• Insights sur la Robustesse : L'évaluation révèle que les GNN agrégés par moyenne sont significativement plus vulnérables aux perturbations adverses que les variantes somme ou max. Dans les ensembles de données de détection de fraude, la perturbation d'une seule dimension d'attribut a conduit à des mauvaises classifications dans jusqu'à 75,8 % des tâches pour les modèles agrégés par moyenne.
• Études d'Ablation : La suppression de l'algorithme de résolution incrémentale ou des stratégies de resserrement des bornes a entraîné des temps d'exécution nettement plus élevés et moins de tâches résolues, confirmant l'efficacité de ces composants.

Importance et Revendications

L'article revendique que GNNev fournit une méthode déterministe et exacte pour vérifier la robustesse aux attaques adverses des GNN, offrant des garanties plus fortes que les méthodes approximatives ou probabilistes. En prenant en charge les agrégations max et moyenne ainsi que l'ajout d'arêtes, il comble des lacunes critiques dans le paysage actuel de la vérification, permettant l'analyse des GNN utilisés dans des bibliothèques standard comme GraphSAGE.

Les auteurs soulignent que leur méthode est particulièrement précieuse pour les applications à haut risque (par exemple, fraude financière, diagnostic médical) où des résultats de vérification non concluants sont insuffisants. La capacité d'identifier des vulnérabilités spécifiques (par exemple, la susceptibilité des modèles agrégés par moyenne) fournit des informations exploitables pour les développeurs et les déploiements de modèles. L'article reconnaît une limitation : la complexité computationnelle croît avec la taille de l'ensemble d'arêtes fragiles, suggérant un travail futur sur la recherche heuristique et les frameworks distribués pour améliorer le passage à l'échelle.