FAME: Formal Abstract Minimal Explanation for Neural Networks

Dit paper introduceert FAME, een nieuwe methode voor formele abstracte minimale verklaringen van neurale netwerken die via geavanceerde perturbatiedomeinen en LiRPA-bounds schaalbaar is naar grote netwerken terwijl het de grootte van de verklaringen verkleint en de kwaliteit kwantificeert.

De kern

FAME: De "Mini-Verklaring" voor Neuronale Netwerken

Stel je voor dat een kunstmatige intelligentie (een AI) een foto bekijkt en zegt: "Dit is een stopbord." Maar als je vraagt: "Waarom?", geeft de AI geen antwoord. Het is als een zwarte doos die alleen het eindresultaat toont. In de echte wereld, bijvoorbeeld bij zelfrijdende auto's of medische diagnose, willen we weten waarom de AI die beslissing nam.

Deze paper introduceert FAME (Formal Abstract Minimal Explanation). Laten we dit uitleggen met een paar simpele analogieën.

1. Het Probleem: De Overvolle Koffer

Stel je voor dat je een enorme koffer hebt vol met spullen (de pixels van een foto). De AI kijkt naar deze koffer en zegt: "Dit is een stopbord."
De vraag is: Welke spullen zijn echt nodig om die conclusie te trekken? Misschien heb je alleen het rode kleurtje en de vorm nodig, en zijn de andere 10.000 pixels (de achtergrond, de lucht, de randen) volkomen irrelevant.

Een "minimale verklaring" is dus de kleinste set spullen die je uit de koffer moet houden om de AI nog steeds te laten zeggen: "Ja, dit is een stopbord." Als je één van die cruciale spullen verwijdert, moet de AI twijfelen.

Het probleem: Bestaande methoden om deze minimale set te vinden zijn als een trage, oude sleutel die je één voor één in elke slot van de koffer moet proberen. Ze moeten de pixels in een specifieke volgorde checken. Bij grote foto's (zoals bij ResNet-modellen) duurt dit eeuwen. Het is te traag en te duur.

2. De Oplossing: FAME (De Slimme Verkleiner)

FAME is een nieuwe manier om deze "koffer" te leegmaken, maar dan veel sneller en slimmer. Het werkt in twee fasen:

Fase 1: De Groene Schaar (Abstract Pruning)

Stel je voor dat je in plaats van één voor één te kijken, een magische schaar hebt die veel onnodige spullen tegelijk kan verwijderen.

• Hoe werkt het? FAME gebruikt een wiskundige techniek (Abstract Interpretation) om te berekenen: "Als we deze hele groep pixels veranderen, blijft het stopbord nog steeds een stopbord?"
• De truc: In plaats van te wachten tot je zeker weet dat één pixel onbelangrijk is, kijkt FAME naar groepen. Het zegt: "Deze 500 pixels samen doen niets voor de beslissing. Weg met ze!"
• Analogie: Het is alsof je een grote tuin hebt en in plaats van één voor één onkruid te wieden, je eerst een grote strook maait die je zeker weet dat leeg is. Dit gaat veel sneller.

Fase 2: De Oranje Schuur (Exact Refinement)

Soms is de magische schaar wat te grof. Hij heeft misschien een paar onnodige spullen nog niet verwijderd, of hij heeft per ongeluk iets belangrijks weggegooid (wat hij corrigeert).

• FAME gebruikt nu een heel nauwkeurige, maar langzamere methode (VERIX+) om de laatste restjes op te ruimen. Omdat Fase 1 al 90% van het werk heeft gedaan, is deze laatste stap heel snel.

3. Waarom is dit zo speciaal?

De auteurs van deze paper hebben een groot probleem opgelost: De volgorde.
Vroeger moest je de pixels in een vaste volgorde checken (bijvoorbeeld van links naar rechts). Maar wat als het stopbord rechts staat? Dan ben je veel tijd kwijt aan het checken van de lege linkerkant.

• FAME's innovatie: FAME heeft geen volgorde nodig. Het kijkt naar de hele foto en kiest slim welke groepen het eerst moet verwijderen. Het is alsof je een drone hebt die de hele tuin in één keer scant en direct ziet waar het onkruid zit, in plaats van op je handen en knieën te krabbelen.

4. De Resultaten in het Dagelijkse Leven

De paper toont aan dat FAME:

1. Veel sneller is: Het kan verklaringen geven voor complexe foto's (zoals verkeersborden of gezichten) in seconden, terwijl oude methoden uren of dagen nodig hebben.
2. Kleinere verklaringen geeft: De "minimale set" die FAME vindt, is vaak compacter dan die van andere methoden. Het is een korter, bondiger antwoord op de vraag "Waarom?".
3. Schaalbaar is: Voor het eerst kunnen ze dit doen op heel complexe modellen (zoals ResNet), die eerder te groot waren voor dit soort nauwkeurige uitleg.

Samenvatting

FAME is als een slimme, snelle editor voor AI-beslissingen. In plaats van de hele tekst (de foto) te lezen om te begrijpen wat er staat, snijdt FAME direct alle overbodige woorden weg en laat alleen de kernzin over. Het doet dit niet door één voor één te zoeken, maar door slimme groepen te verwijderen, waardoor het mogelijk wordt om zelfs de grootste en complexste AI-systemen te begrijpen.

Dit is een enorme stap voorwaarts om AI niet alleen slim, maar ook vertrouwbaar en begrijpelijk te maken voor mensen.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "FAME: Formal Abstract Minimal Explanation for Neural Networks", gepresenteerd in het Nederlands.

Titel: FAME: Formele Abstracte Minimale Uitleg voor Neuronale Netwerken

Auteurs: Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe, Shahaf Bassan en Guy Katz.
Publicatie: ICLR 2026 (Conference Paper).

---

1. Het Probleem

Neuronale netwerken worden steeds vaker ingezet in kritieke toepassingen, maar hun besluitvormingsprocessen blijven vaak een "black box". Hoewel er methoden bestaan om uitleg te geven (XAI), zijn formele methoden die wiskundig bewezen correcte uitleggen leveren (zoals Abductive Explanations of AXp), vaak niet schaalbaar naar grote netwerken.

De kernuitdagingen zijn:

• Computationele complexiteit: Het vinden van een minimale set van invoerfeatures die de voorspelling van het model garandeert, is een NP-hard probleem. Bestaande methoden (zoals VERIX+) gebruiken vaak exacte verifiers (zoals SAT/SMT-solvers) die traag zijn en niet schalen naar grote netwerken (bijv. CNN's of ResNets).
• Afhankelijkheid van traversie-ordening: Bestaande methoden moeten features sequentieel verwerken (één voor één toevoegen of verwijderen). De volgorde waarin dit gebeurt, beïnvloedt sterk de kwaliteit van de uitleg en de rekentijd. Het vinden van een optimale volgorde vereist echter kennis die de uitleg juist moet onthullen (een circulaire afhankelijkheid).
• Schaalbaarheid: Exacte methoden zijn vaak onuitvoerbaar voor moderne, diepe netwerken, waardoor er een behoefte is aan methoden die een compromis sluiten tussen nauwkeurigheid en snelheid zonder de formele garanties volledig op te geven.

2. Methodologie: Het FAME Framework

FAME (Formal Abstract Minimal Explanations) introduceert een hybride aanpak die abstracte interpretatie combineert met geavanceerde perturbatie-domeinen om de sequentiële bottleneck te doorbreken.

Kernconcepten:

• Abductive Explanations (AXp): Een subset van invoerfeatures die, als ze op hun nominale waarde worden gefixeerd, garanderen dat het model dezelfde voorspelling maakt binnen een bepaald perturbatie-domein.
• Abstracte Interpretatie (LiRPA): FAME gebruikt Linear Relaxation-based Perturbation Analysis (LiRPA) om conservatieve boven- en ondergrenzen te berekenen voor de netwerkoutput. Dit maakt het mogelijk om grote batches van features tegelijkertijd te analyseren in plaats van één voor één.

De FAME Pipeline (Twee Fasen):

Fase 1: Abstract Pruning (Schaalbare Reductie)
In plaats van features sequentieel te testen, gebruikt FAME een Abstract Batch Certificate om grote sets van irrelevante features gelijktijdig te identificeren en te "bevrijden" (d.w.z. te toestaan dat ze variëren zonder de voorspelling te beïnvloeden).

• Asymmetrie van Feature-selectie: Het paper stelt dat het onveilig is om meerdere features tegelijk te bevrijden op basis van individuele checks (Propositie 4.1). FAME lost dit op met een gezamenlijke bovengrens berekening.
• Abstract Batch Certificate ($\Phi$): Een wiskundig bewijsobject (gebaseerd op CROWN/LiRPA) dat garandeert dat een hele set features $A$ tegelijkertijd kan worden vrijgegeven zonder dat de eigenschap $P$ (bijv. correcte classificatie) wordt geschonden.
• Greedy Knapsack Formule: Het vinden van de maximale set van vrij te geven features wordt gemodelleerd als een 0/1 Multidimensionale Knapsack-probleem. FAME gebruikt een efficiënt greedy-heuristisch algoritme (in plaats van een dure MILP-oplosser) om deze set te selecteren.
• Cardinality-Constrained Perturbation Domain: Een innovatie is het gebruik van een domein $\Omega_m(x; A)$ waarbij maximaal $m$ features tegelijk mogen variëren. Door dit domein recursief te verkleinen (naarmate meer features vrijgegeven worden), worden de abstracte grenzen strakker, waardoor meer features kunnen worden vrijgegeven. Dit elimineert de noodzaak van een vooraf bepaalde traversie-ordening.

Fase 2: Exact Refinement (Garantie van Minimale Uitleg)
De output van Fase 1 is een abstracte minimale uitleg. Omdat abstracte interpretatie conservatief is, kan deze uitleg nog niet-minimale features bevatten.

• FAME gebruikt een Exact Refinement stap om de uitleg te minimaliseren.
• Dit gebeurt via een combinatie van adversarial attacks (om snel noodzakelijke features te identificeren) en optionele calls naar een exacte verifier (zoals VERIX+ met Marabou) voor de laatste verfijning.
• Dit resulteert in een formele, gegarandeerde minimale uitleg.

3. Belangrijkste Bijdragen

1. Eerste schaalbare abstracte uitleg: FAME is de eerste methode die abstracte interpretatie gebruikt om abductieve uitleggen te genereren voor grote, high-dimensional neuronale netwerken.
2. Eliminatie van traversie-ordening: Door gebruik te maken van LiRPA-bases en een recursief verkleinend perturbatie-domein, hoeft FAME geen volgorde van features voor te schrijven. Dit doorbreekt de sequentiële bottleneck van eerdere werken.
3. Wiskundig bewezen kwaliteitsgarantie: De auteurs introduceren een procedure om de "worst-case distance" tussen de abstracte uitleg en de ware minimale uitleg te meten, gecombineerd met een optionele exacte verfijning.
4. Schaalbaarheid op grote netwerken: FAME produceert de eerste formele abductieve uitleggen voor een ResNet-architectuur op CIFAR-10, een taak waarvoor exacte methoden onuitvoerbaar (intractable) zijn.

4. Resultaten en Experimenten

De auteurs hebben FAME geëvalueerd op MNIST en GTSRB datasets (FC en CNN modellen) en vergeleken met de state-of-the-art methode VERIX+.

• Snelheid: FAME is aanzienlijk sneller dan VERIX+. Op de GTSRB-CNN was FAME tot 25x sneller (7.4s vs 185s) terwijl het een kleinere of vergelijkbare uitleg leverde.
• Grootte van de uitleg: FAME levert consistent kleinere uitleggen (kleinere cardinaliteit) dan VERIX+. De iteratieve verfijning in FAME reduceerde de uitleggrootte met tot 36% vergeleken met een enkele ronde.
• Greedy vs. Exact: Het gebruik van de greedy-heuristiek voor het batch-vrijgeven van features levert bijna identieke resultaten op als de optimale MILP-oplosser (gemiddeld < 9 features verschil), maar met een snelheidswinst van 9x tot 12x.
• ResNet-2B (CIFAR-10): Op dit diepe netwerk faalden exacte methoden (time-outs/geheugenoverschrijding). FAME slaagde erin om geldige abstracte uitleggen te genereren, waarbij het iteratieve proces de grootte van de vrijgegeven features van ~5 (enkele ronde) naar ~476 (iteratief) bracht.

5. Betekenis en Conclusie

FAME vertegenwoordigt een doorbraak in het veld van Formele XAI. Het bewijst dat het mogelijk is om formele, wiskundig gegarandeerde uitleggen te genereren voor complexe, moderne neurale netwerken door slimme combinaties van abstracte interpretatie en heuristieken.

• Praktische impact: Het maakt formele verificatie toegankelijk voor netwerken die eerder te groot waren voor deze analyse, wat essentieel is voor de inzet van AI in veiligheidskritieke domeinen (zoals luchtvaart, waar de auteurs vandaan komen).
• Methodologische verschuiving: Het paper verschuift de focus van sequentiële, exacte zoektochten naar parallelle, abstracte filtering, wat de weg vrijmaakt voor schaalbare en betrouwbare AI-explainability.

Kortom, FAME biedt een oplossing voor het "schaalbaarheidsprobleem" in formele XAI zonder in te leveren op de wiskundige geldigheid van de uitleg.