Résumé technique : SHAP Vérifié (VERISHAP)

Énoncé du problème

Les Explications Additives de Shapley (SHAP) constituent une méthode standard d'explicabilité a posteriori pour attribuer les prédictions des modèles d'apprentissage automatique aux caractéristiques d'entrée. Cependant, le calcul exact des valeurs SHAP pour les réseaux de neurones est largement considéré comme intraitable sur le plan computationnel en raison de l'espace de recherche exponentiel sur les sous-ensembles de caractéristiques ($2^n$). Bien que le calcul exact soit réalisable pour les modèles basés sur des arbres et les modèles additifs, il est #P-difficile pour les réseaux de neurones généraux. Par conséquent, la littérature s'appuie sur des estimateurs statistiques (par exemple, KERNELSHAP, FASTSHAP, LEVERAGESHAP). Ces estimateurs font face à deux limitations fondamentales :

1. Inexactitude : Ils fournissent des approximations qui peuvent être peu fiables dans des modèles hautement non linéaires ou des scénarios présentant de fortes interactions entre caractéristiques.
2. Absence de vérité terrain : Comme le calcul exact des valeurs SHAP est prohibitivement coûteux pour les réseaux de neurones, les estimateurs sont généralement évalués sur des modèles de taille réduite où le calcul exact est possible. Ces configurations échouent souvent à se généraliser aux réseaux de neurones réels de haute dimension.

Méthodologie : SHAP Vérifié (VERISHAP)

L'article présente VERISHAP, le premier algorithme exploitant les récentes avancées en vérification de réseaux de neurones pour calculer les valeurs SHAP exactes et des bornes prouvables pour les réseaux de neurones. L'approche adapte les techniques de vérification par branch-and-bound à la nature discrète, probabiliste et lourde en sommes de SHAP.

Algorithme central

VERISHAP emploie une stratégie incrémentale de branch-and-bound pour partitionner récursivement l'espace des caractéristiques (l'ensemble de toutes les coalitions $S_i$ pour une caractéristique $i$).

1. Partitionnement : L'algorithme définit des branches $B$ basées sur des ensembles de caractéristiques incluses ($I$) et exclues ($E$). Une branche représente un sous-ensemble de coalitions où les caractéristiques de $I$ sont présentes et les caractéristiques de $E$ sont absentes.
2. Bornage par propagation : Pour chaque branche, l'algorithme calcule des bornes inférieure et supérieure sur la contribution marginale $\Delta_i(S) = v(S \cup \{i\}) - v(S)$.
   • Pour appliquer la propagation de bornes continues (par exemple, CROWN, IBP) à des ensembles discrets, l'algorithme relâche les masques de caractéristiques booléens $m \in \{0, 1\}^n$ vers le domaine continu $[0, 1]^n$.
   • Il utilise la Propagation de Bornes Linéaires (LBP) (spécifiquement CROWN-IBP) pour dériver des bornes serrées sur la fonction de valeur $v(S)$ sur le domaine relâché.
3. Agrégation : Les bornes totales de la valeur SHAP sont calculées en sommant les bornes pondérées de toutes les branches :
   $$\phi_i^{(t)} = \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B \leq \phi_i \leq \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B = \bar{\phi}_i^{(t)}$$
   où $\Lambda_B$ est la somme sous forme fermée des poids de Shapley pour les coalitions dans la branche $B$, dérivée de manière combinatoire.
4. Raffinement : L'algorithme sélectionne itérativement des branches à diviser (en utilisant des stratégies comme MAXDIAM) et des caractéristiques sur lesquelles diviser (en utilisant des stratégies comme SMEARS), affinant les bornes jusqu'à ce qu'elles convergent vers la valeur exacte ou une précision souhaitée.

Propriétés théoriques clés

• Terminaison : L'algorithme est garanti de terminer avec des valeurs SHAP exactes après un nombre fini d'itérations (au plus $2^{n-1}$), car la partition isole éventuellement des coalitions uniques.
• Terminaison précoce pour les modèles linéaires : Pour les modèles linéaires, l'algorithme termine à la première itération car la contribution marginale est constante, et la LBP n'introduit aucune erreur d'approximation pour les compositions linéaires.
• Linéarité par morceaux : Pour les réseaux activés par ReLU, l'algorithme peut terminer prématurément si la partition restreint la recherche à des régions où le réseau se comporte de manière linéaire.

Contributions clés

1. Premier SHAP exact pour les réseaux de neurones : VERISHAP est le premier algorithme à calculer des valeurs SHAP exactes pour des réseaux de neurones généraux, évoluant vers des espaces de recherche d'ordres de grandeur supérieurs aux méthodes exactes précédentes.
2. Bornes prouvables : La méthode fournit des bornes inférieures et supérieures arbitrairement serrées sur les valeurs SHAP, permettant des insights explicatifs fiables même avant la convergence complète.
3. Référence de vérité terrain : Elle établit un cadre principiel pour évaluer les estimateurs statistiques SHAP sur des espaces de recherche plus grands et plus réalistes où la vérité terrain était auparavant inaccessible.
4. Efficacité via la vérification : En exploitant la décomposition des réseaux de neurones en régions quasi-linéaires, l'algorithme évite d'énumérer toutes les $2^n$ coalitions dans de nombreux cas pratiques.

Résultats expérimentaux

Les auteurs ont évalué VERISHAP sur des benchmarks tabulaires (ensembles de données UCI) et de vision (MNIST, FashionMNIST, CIFAR10, GTSRB).

• Évolutivité par rapport à ExactSHAP : VERISHAP surpasse nettement la méthode exacte de l'état de l'art (EXACTSHAP). Alors qu'EXACTSHAP épuise la mémoire GPU pour des espaces de recherche supérieurs à $2^{20}$, VERISHAP calcule des valeurs exactes pour des instances allant jusqu'à $2^{25}$ ($\approx 3 \times 10^7$ coalitions) et fournit des bornes serrées pour des espaces allant jusqu'à $2^{60}$ ($\approx 10^{18}$ coalitions).
• Comparaison avec les estimateurs : Comparé aux estimateurs statistiques (KERNELSHAP, TREEMSR, LEVERAGESHAP), VERISHAP démontre que les estimateurs échouent souvent à atteindre la même précision dans les contraintes de mémoire. De plus, VERISHAP révèle que la performance des estimateurs varie considérablement selon les ensembles de données (par exemple, TREEMSR montre des performances volatiles sur les réseaux de neurones par rapport aux modèles basés sur des arbres).
• Versatilité architecturale : L'algorithme calcule avec succès des valeurs SHAP exactes pour diverses architectures, y compris des réseaux entièrement connectés avec des activations ReLU, tanh et Swish, ainsi que des ResNets.
• Convergence : Dans les expériences (par exemple, MNIST), les bornes deviennent informatives (révélant des schémas d'attribution) bien avant que la valeur exacte ne soit calculée, souvent en quelques secondes, tandis que le calcul exact peut prendre plusieurs dizaines de secondes.

Importance et affirmations

L'article positionne VERISHAP comme une première étape vers la mise à l'échelle du calcul exact de SHAP pour les réseaux de neurones. Son importance réside dans trois domaines :

1. Évolutivité : Il comble le fossé entre l'intraitabilité théorique de SHAP exact et l'application pratique en exploitant la vérification de réseaux de neurones.
2. Fiabilité : Il offre une méthode pour obtenir des explications de « vérité terrain » avec des garanties prouvables, répondant à l'incertitude inhérente aux approximations statistiques.
3. Cadre d'évaluation : Il fournit un benchmark rigoureux pour évaluer et améliorer les estimateurs SHAP sur des espaces de recherche plus vastes, dépassant les modèles de taille réduite.

Les auteurs reconnaissent que le calcul exact de SHAP reste #P-difficile et que VERISHAP peut encore être lent pour certains réseaux complexes. Cependant, ils soutiennent que la capacité à calculer des bornes prouvables et le potentiel d'améliorations continues en matière de vérification de réseaux de neurones en font une avancée fondamentale pour l'explicabilité fiable de l'IA.