Technisches Resümee: Binäre Spiking Neural Networks als Kausale Modelle

Problemstellung

Die Arbeit adressiert den Zielkonflikt zwischen der Genauigkeit und der Erklärbarkeit von Künstlichen Neuronalen Netzen (ANNs). Während Binarisierte Neuronale Netze (BNNs) und Binäre Spiking Neuronale Netze (BSNNs) Vorteile in Bezug auf Hardware-Effizienz und logische Repräsentierbarkeit bieten, bleiben ihre internen Entscheidungsprozesse opak. Bestehende Methoden der erklärbaren KI (XAI), wie etwa SHAP, behandeln Modelle oft als „Black Boxes“ und berücksichtigen dabei nicht die internen kausalen Strukturen. Folglich können diese Methoden Merkmale als relevant identifizieren, selbst wenn sie keine kausale Verbindung zum Ausgang des Netzwerks aufweisen (z. B. Verbindungen mit Null-Gewicht). Die Autoren zielen darauf ab, diese Lücke zu schließen, indem sie die Dynamik von BSNNs formal auf ein kausales Framework abbilden, was die Generierung rigoroser, logikbasierter Erklärungen ermöglicht, die die kausale Relevanz der eingeschlossenen Merkmale garantieren.

Methodik

1. Formalisierung von BSNNs

Die Autoren definieren eine BSNN-Architektur $S$ als ein Tupel, das aus Input-Neuronen ($I$), Nicht-Input-Neuronen ($L$), Konnektivitätsrelationen ($R$), Gewichtfunktionen ($W$) und Schwellenwerten ($\tau$) besteht. Sie modellieren die Spiking-Dynamik mittels eines Integrate-and-Fire (IF)-Mechanismus ohne Leckage (Leaks), wobei der Feuermodus eines Neurons zum Zeitpunkt $t$ rekursiv von seinem vorherigen Zustand und der gewichteten Summe eingehender Spikes abhängt.

• Gewichtsquantisierung: Die Studie konzentriert sich auf Netzwerke mit Gewichten, die auf die binären Mengen $\{0, 1\}$ oder ternäre Mengen $\{-1, 0, 1\}$ quantisiert sind.
• Spike-Kodierung: In den Experimenten werden Poisson-Rate-Kodierung und Schwellenwert-Binarisierungsschemata verwendet. Die Autoren vermeiden explizit komplexe zeitliche Kodierungen, um die Rechenkomplexität der Generierung von Erklärungen zu bewältigen.

2. Abbildung auf Binäre Kausale Modelle (BCMs)

Ein zentraler methodischer Beitrag ist die Abbildung der Spiking-Dynamik des BSNN auf ein Binäres Kausales Modell (BCM).

• Variablen: Jedem Neuron $X$ zu jedem Zeitschritt $t$ wird eine Boolesche Variable $p_{X,t}$ zugewordnet. Input-Neuronen entsprechen exogenen Variablen, während Nicht-Input-Neuronen endogenen Variablen entsprechen.
• Kausale Abhängigkeiten: Die Feurologik wird in eine Menge von Booleschen Gleichungen (Strukturgleichungen) übersetzt. Damit ein Neuron feuert, muss eine spezifische Kombination von Vorgänger-Spikes die Schwellenwertbedingung erfüllen.
• Äquivalenz: Die Autoren beweisen (Theorem 5.2), dass die Feuermodelle des BSNN genau dann mit dem BCM kompatibel sind, wenn die Boolesche Interpretation alle Gleichungen im Modell erfüllt.

3. Generierung abduktiver Erklärungen (AXp)

Das Paper verwendet Abduktive Erklärungen (AXp), definiert als minimal ausreichende Mengen an Input-Merkmalen (Literalen), die eine spezifische Klassifizierung des Outputs garantieren.

• Definition: Eine AXp $\lambda$ für einen Output $\omega_0$ muss folgendes erfüllen: (i) $\lambda$ ist unter den gegebenen Inputs wahr; (ii) $\lambda$ impliziert logisch $\omega_0$ unter den BCM-Constraints; und (iii) $\lambda$ ist minimal (keine echte Teilmenge impliziert $\omega_0$).
• Algorithmen: Zwei Solver-basierte Ansätze werden implementiert, um AXps zu finden:
  1. SAT-basiert: Kodiert das BCM und die Erklärungsbedingungen in die Aussagenlogik (Propositional Logic).
  2. SMT-basiert: Kodiert das Modell unter Verwendung von Satisfiability Modulo Theories (speziell Linear Integer Arithmetic), was die universelle Quantifizierung über Variablesätze vermeidet und signifikante Geschwindigkeitsverbesserungen bietet.
• Suchstrategie: Der Algorithmus beginnt mit einem vollständigen Term, der den gesamten Input repräsentiert, und entfernt iterativ Literale, während er verifiziert, dass die Implikation zum Output weiterhin gültig bleibt.

4. Experimenteller Aufbau

Die Methodik wurde auf dem MNIST-Datensatz zur Erkennung handgeschriebener Ziffern getestet.

• Architekturen: Vollvernetzte Netzwerke mit variierenden Größen der verborgenen Schichten ($k \in \{8, 16, 32, 64, 128\}$) und Gewichtsquantisierungen (binär und ternär).
• Aufgaben: Klassifizierung von 3-Ziffern-Teilmengen und des vollen 10-Ziffern-Sets.
• Validierung: Erzielte eine hohe Genauigkeit (bis zu ca. 95 % bei 3-Ziffern-Aufgaben) unter Verwendung von binär und ternär quantisierten Netzwerken.

Zentrale Beiträge

1. Erste kausale Abbildung von BSNNs: Das Paper präsentiert die erste formale Abbildung eines Binären Spiking Neuronalen Netzes auf ein Binäres Kausales Modell, welche die zeitlichen kausalen Abhängigkeiten zwischen neuronalen Einheiten erfasst.
2. Logikbasierter Erklärungsrahmen: Es zeigt, dass die boolesche Natur von BSNNs die Verwendung von SAT- und SMT-Solvern ermöglicht, um abduktive Erklärungen direkt aus dem kausalen Modell zu berechnen.
3. Garantie der kausalen Relevanz: Ein entscheidender theoretischer Beitrag ist Proposition 6.2, die beweist, dass jedes Merkmal, das in einer aus diesem Framework abgeleiteten abduktiven Erklärung enthalten ist, eine Verbindung mit einem Nicht-Null-Gewicht zur verborgenen Schicht des Netzwerks haben muss. Dies stellt sicher, dass die Erklärung keine völlig irrelevanten Merkmale enthält.
4. Vergleichsanalyse mit SHAP: Das Paper bietet einen rigorosen Vergleich mit SHAP (SHapley Additive exPlanations) und hebt hervor, dass SHAP dazu neigt, Merkmale mit Null-Gewicht-Verbindungen als relevant einzustufen, was auf dessen modellagnostische Natur zurückzuführen ist.

Ergebnisse

• Recheneffizienz: Der SMT-basierte Ansatz übertraf den SAT-basierten Ansatz signifikant. Für Netzwerke mit binären Gewichten ($S^{bin}_k$) reduzierte SMT die Suchzeiten von Stunden (SAT) auf Sekunden (z. B. ~11 Stunden vs. ~12 Sekunden für $k=32$). Für Netzwerke mit ternären Gewichten ($S^{tern}_k$) lagen die SMT-Suchzeiten zwischen 0,27 und 1,0 Stunden.
• Qualität der Erklärungen: Die generierten Erklärungen waren minimale Mengen aktiver oder inaktiver Pixel, die ausreichten, um die Klassifizierung auszulösen.
• SHAP-Vergleich:
  • SHAP identifizierte Merkmale mit Null-Gewicht-Verbindungen in etwa 47 % der Fälle fälschlicherweise als relevant (gemittelt über die Stichprobengrößen).
  • Eine Erhöhung der Stichprobengröße für SHAP reduzierte diese Fehlerrate, steigerte jedoch drastisch die Rechenzeit (z. B. 173 Sekunden für 1 Mio. Stichproben).
  • Im Gegensatz dazu garantiert die vorgeschlagene logikbasierte Methode mathematisch, dass keine Merkmale mit Null-Gewicht in die Erklärung aufgenommen werden.

Bedeutung und Ansprüche

Die Autoren positionieren diese Arbeit als einen grundlegenden Schritt, um BSNNs durch formale Logik interpretierbar zu machen. Sie behaupten, dass durch die Nutzung der in BSNNs inhärenten kausalen Struktur Erklärungen generiert werden können, die nicht nur effizient, sondern auch formal garantiert frei von irrelevanten Merkmalen sind – eine Eigenschaft, die statistische oder modellagnostische Methoden wie SHAP nicht bieten können.

Das Paper merkt bescheiden an, dass sich die aktuelle Arbeit ausschließlich auf abduktive Erklärungen (AXp) und vollvernetzte Architekturen konzentriert. Die Autoren legen nahe, dass das Framework auf komplexere kausale Konzepte (wie „Actual Cause“ und „NESS Cause“) sowie auf andere Architekturen wie Convolutional BSNNs (C-BSNNs) und Netzwerke, die auf Sprachdatensätzen trainiert wurden, erweiterbar ist, wenngleich diese als Richtungen für zukünftige Forschung und nicht als aktuelle Errungenschaften identifiziert wurden.