Technische Samenvatting: Verified SHAP (VERISHAP)

Probleemstelling

Shapley Additive Explanations (SHAP) zijn een standaard post-hoc methode voor uitlegbaarheid om voorspellingen van machine learning-modellen toe te schrijven aan invoerfuncties. Het berekenen van exacte SHAP-waarden voor neurale netwerken wordt echter algemeen beschouwd als computationeel onuitvoerbaar vanwege de exponentiële zoekruimte over functiesubsets ($2^n$). Hoewel exacte berekening haalbaar is voor op bomen gebaseerde en additieve modellen, is het #P-hard voor algemene neurale netwerken. Bijgevolg vertrouwt de literatuur op statistische schatters (bijv. KERNELSHAP, FASTSHAP, LEVERAGESHAP). Deze schatters staan voor twee fundamentele beperkingen:

1. Onnauwkeurigheid: Ze leveren benaderingen op die onbetrouwbaar kunnen zijn in sterk niet-lineaire modellen of scenario's met sterke functie-interacties.
2. Gebrek aan Grondwahrheid: Omdat exacte SHAP-waarden voor neurale netwerken te duur zijn om te berekenen, worden schatters doorgaans geëvalueerd op modellen van speelgoedgrootte waar exacte berekening mogelijk is. Deze settings generaliseren vaak niet naar realistische, hoogdimensionale neurale netwerken.

Methodologie: Verified SHAP (VERISHAP)

Het artikel introduceert VERISHAP, het eerste algoritme dat gebruikmaakt van recente vooruitgang in verificatie van neurale netwerken om exacte SHAP-waarden en bewijsbare grenzen te berekenen voor neurale netwerken. De aanpak past verificatietechnieken op basis van branch-and-bound aan aan het discrete, probabilistische en sommatie-intensieve karakter van SHAP.

Kernalgoritme

VERISHAP hanteert een incrementele branch-and-bound-strategie om de functieruimte (de verzameling van alle coalities $S_i$ voor een functie $i$) recursief te partitioneren.

1. Partitionering: Het algoritme definieert takken $B$ op basis van verzamelingen van opgenomen ($I$) en uitgesloten ($E$) functies. Een tak vertegenwoordigt een subset van coalities waarbij functies in $I$ aanwezig zijn en functies in $E$ afwezig zijn.
2. Grenzen via Propagatie: Voor elke tak berekent het algoritme onder- en bovengrenzen voor de marginale bijdrage $\Delta_i(S) = v(S \cup \{i\}) - v(S)$.
   • Om continue grenspropagatie (bijv. CROWN, IBP) toe te passen op discrete verzamelingen, verontacht het algoritme Booleaanse functiemaskers $m \in \{0, 1\}^n$ naar het continue domein $[0, 1]^n$.
   • Het maakt gebruik van Lineaire Grenspropagatie (LBP) (specifiek CROWN-IBP) om strakke grenzen af te leiden voor de waardenfunctie $v(S)$ over het verontachte domein.
3. Aggregatie: De totale SHAP-waardegrenzen worden berekend door de gewogen grenzen van alle takken op te tellen:
   $$\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)}$$
   waarbij $\Lambda_B$ de gesloten-vorm som is van Shapley-gewichten voor de coalities in tak $B$, combinatorisch afgeleid.
4. Verfijning: Het algoritme selecteert iteratief takken om te splitsen (met strategieën zoals MAXDIAM) en functies om op te splitsen (met strategieën zoals SMEARS), en verfijnt de grenzen totdat ze convergeren naar de exacte waarde of een gewenste precisie.

Belangrijkste Theoretische Eigenschappen

• Terminatie: Het algoritme garandeert dat het na een eindig aantal iteraties (maximaal $2^{n-1}$) termineert met exacte SHAP-waarden, aangezien de partitionering uiteindelijk enkele coalities isoleert.
• Vroege Terminatie voor Lineaire Modellen: Voor lineaire modellen terminateert het algoritme in de eerste iteratie omdat de marginale bijdrage constant is, en LBP geen benaderingsfout introduceert voor lineaire composities.
• Gedeeltelijke Lineariteit: Voor netwerken geactiveerd met ReLU kan het algoritme vroegtijdig termineren als de partitionering de zoektocht beperkt tot regio's waar het netwerk lineair gedraagt.

Belangrijkste Bijdragen

1. Eerste Exacte SHAP voor Neurale Netwerken: VERISHAP is het eerste algoritme dat exacte SHAP-waarden berekent voor algemene neurale netwerken, schaalbaar tot zoekruimtes die ordes van grootte groter zijn dan eerdere exacte methoden.
2. Bewijsbare Grenzen: De methode levert willekeurig strakke onder- en bovengrenzen op SHAP-waarden, wat betrouwbare uitlegbaarheidsinzichten mogelijk maakt zelfs voordat volledige convergentie is bereikt.
3. Grondwahrheid-Baseline: Het vestigt een principieel kader voor het evalueren van statistische SHAP-schatters op grotere, realistischere zoekruimtes waar grondwahrheid voorheen onbereikbaar was.
4. Efficiëntie via Verificatie: Door gebruik te maken van de decompositie van neurale netwerken in bijna-lineaire regio's, vermijdt het algoritme in veel praktische gevallen het enumereren van alle $2^n$ coalities.

Experimentele Resultaten

De auteurs hebben VERISHAP geëvalueerd op tabulaire (UCI-datasets) en visuele (MNIST, FashionMNIST, CIFAR10, GTSRB) benchmarks.

• Schaalbaarheid versus ExactSHAP: VERISHAP presteert aanzienlijk beter dan de state-of-the-art exacte methode (EXACTSHAP). Waar EXACTSHAP de GPU-geheugenlimiet bereikt voor zoekruimtes groter dan $2^{20}$, berekent VERISHAP exacte waarden voor instanties tot $2^{25}$ ($\approx 3 \times 10^7$ coalities) en levert strakke grenzen voor ruimtes tot $2^{60}$ ($\approx 10^{18}$ coalities).
• Vergelijking met Schatters: Bij vergelijking met statistische schatters (KERNELSHAP, TREEMSR, LEVERAGESHAP) toont VERISHAP aan dat schatters vaak niet dezelfde nauwkeurigheid bereiken binnen geheugenbeperkingen. Bovendien onthult VERISHAP dat de prestaties van schatters aanzienlijk variëren tussen datasets (bijv. TREEMSR vertoont vluchtige prestaties op neurale netwerken in vergelijking met op bomen gebaseerde modellen).
• Architectuurveelzijdigheid: Het algoritme berekent succesvol exacte SHAP-waarden voor diverse architecturen, waaronder volledig verbonden netwerken met ReLU-, tanh- en Swish-activaties, evenals ResNets.
• Convergentie: In experimenten (bijv. MNIST) worden de grenzen informatief (waaronder toewijzingspatronen) lang voordat de exacte waarde is berekend, vaak binnen seconden, terwijl exacte berekening tientallen seconden kan duren.

Betekenis en Claims

Het artikel positioneert VERISHAP als een eerste stap naar het schalen van exacte SHAP-berekening voor neurale netwerken. De betekenis ligt op drie gebieden:

1. Schaalbaarheid: Het overbrugt de kloof tussen de theoretische onuitvoerbaarheid van exacte SHAP en praktische toepassing door gebruik te maken van verificatie van neurale netwerken.
2. Betrouwbaarheid: Het biedt een methode om "grondwahrheid"-uitleg te verkrijgen met bewijsbare garanties, waarmee de onzekerheid inherent aan statistische benaderingen wordt aangepakt.
3. Evaluatiekader: Het levert een rigoureuze benchmark voor het evalueren en verbeteren van SHAP-schatters op grotere zoekruimtes, verder dan modellen van speelgoedgrootte.

De auteurs erkennen dat het berekenen van exacte SHAP-waarden #P-hard blijft en dat VERISHAP voor bepaalde complexe netwerken nog steeds traag kan zijn. Ze betogen echter dat het vermogen om bewijsbare grenzen te berekenen en het potentieel voor verdere verbeteringen in de verificatie van neurale netwerken dit een fundamentele doorbraak maken voor betrouwbare AI-uitlegbaarheid.