Technical Summary: Binary Spiking Neural Networks as Causal Models

Problem Statement

The paper addresses the trade-off between the accuracy and explainability of Artificial Neural Networks (ANNs). While Binarized Neural Networks (BNNs) and Binary Spiking Neural Networks (BSNNs) offer advantages in terms of hardware efficiency and logical representability, their internal decision-making processes remain opaque. Existing explainable AI (XAI) methods, such as SHAP, often treat models as "black boxes," failing to account for internal causal structures. Consequently, these methods may identify features as relevant even when they have no causal connection to the network's output (e.g., zero-weight connections). The authors aim to bridge this gap by formally mapping the dynamics of BSNNs to a causal framework, enabling the generation of rigorous, logic-based explanations that guarantee the causal relevance of included features.

Methodology

1. Formalization of BSNNs

The authors define a BSNN architecture $S$ as a tuple comprising input neurons ($I$), non-input neurons ($L$), connectivity relations ($R$), weight functions ($W$), and firing thresholds ($\tau$). They model the spiking dynamics using an Integrate-and-Fire (IF) mechanism without leaks, where the firing state of a neuron at time $t$ depends recursively on its previous state and the weighted sum of incoming spikes.

• Weight Quantization: The study focuses on networks with weights quantized to binary $\{0, 1\}$ or three-valued $\{-1, 0, 1\}$ sets.
• Spike Encoding: Experiments utilize Poisson rate coding and threshold-binarized schemes. The authors explicitly avoid complex temporal coding to manage the computational complexity of explanation generation.

2. Mapping to Binary Causal Models (BCMs)

A core methodological contribution is the mapping of the BSNN's spiking dynamics to a Binary Causal Model (BCM).

• Variables: Each neuron $X$ at each time step $t$ is assigned a Boolean variable $p_{X,t}$. Input neurons correspond to exogenous variables, while non-input neurons correspond to endogenous variables.
• Causal Dependencies: The firing logic is translated into a set of Boolean equations (structural equations). For a neuron to fire, a specific combination of predecessor spikes must satisfy the threshold condition.
• Equivalence: The authors prove (Theorem 5.2) that the firing functions of the BSNN are compatible with the BCM if and only if the Boolean interpretation satisfies all equations in the model.

3. Abductive Explanation (AXp) Generation

The paper employs Abductive Explanations (AXp), defined as minimally sufficient sets of input features (literals) that guarantee a specific output classification.

• Definition: An AXp $\lambda$ for an output $\omega_0$ must satisfy: (i) $\lambda$ is true given the input; (ii) $\lambda$ logically implies $\omega_0$ under the BCM constraints; and (iii) $\lambda$ is minimal (no proper subset implies $\omega_0$).
• Algorithms: Two solver-based approaches are implemented to find AXps:
  1. SAT-based: Encodes the BCM and the explanation conditions into Propositional Logic.
  2. SMT-based: Encodes the model using Satisfiability Modulo Theories (specifically Linear Integer Arithmetic), which avoids universal quantification over variable sets, offering significant speed improvements.
• Search Strategy: The algorithm starts with a complete term representing the full input and iteratively removes literals while verifying that the implication to the output remains valid.

4. Experimental Setup

The methodology was tested on the MNIST dataset for handwritten digit recognition.

• Architectures: Fully connected networks with varying hidden layer sizes ($k \in \{8, 16, 32, 64, 128\}$) and weight quantizations (binary and ternary).
• Tasks: Classification of 3-digit subsets and the full 10-digit set.
• Validation: Achieved high accuracy (up to ~95% for 3-digit tasks) using binary and ternary quantized networks.

Key Contributions

1. First Causal Mapping of BSNNs: The paper presents the first formal mapping of a Binary Spiking Neural Network onto a Binary Causal Model, capturing temporal causal dependencies between neural units.
2. Logic-Based Explanation Framework: It demonstrates that the Boolean nature of BSNNs allows for the use of SAT and SMT solvers to compute abductive explanations directly from the causal model.
3. Guarantee of Causal Relevance: A critical theoretical contribution is Proposition 6.2, which proves that any feature included in an abductive explanation derived from this framework must have a non-zero weight connection to the network's hidden layer. This ensures that the explanation contains no completely irrelevant features.
4. Comparative Analysis with SHAP: The paper provides a rigorous comparison with SHAP (SHapley Additive exPlanations), highlighting SHAP's tendency to assign relevance to features with zero-weight connections due to its model-agnostic nature.

Results

• Computational Efficiency: The SMT-based approach significantly outperformed the SAT-based approach. For binary weight networks ($S^{bin}_k$), SMT reduced search times from hours (SAT) to seconds (e.g., ~11 hours vs. ~12 seconds for $k=32$). For ternary weight networks ($S^{tern}_k$), SMT search times ranged from 0.27 to 1.0 hours.
• Explanation Quality: The generated explanations were minimal sets of active or inactive pixels sufficient to trigger the classification.
• SHAP Comparison:
  • SHAP incorrectly identified features with zero-weight connections as relevant in approximately 47% of cases (averaged across sample sizes).
  • Increasing the sample size for SHAP reduced this error rate but drastically increased computation time (e.g., 173 seconds for 1M samples).
  • In contrast, the proposed logic-based method mathematically guarantees that no zero-weight features are included in the explanation.

Significance and Claims

The authors position this work as a foundational step in making BSNNs interpretable through formal logic. They claim that by leveraging the causal structure inherent in BSNNs, it is possible to generate explanations that are not only efficient but also formally guaranteed to be free of irrelevant features—a property that statistical or model-agnostic methods like SHAP cannot provide.

The paper modestly notes that current work focuses exclusively on abductive explanations (AXp) and fully connected architectures. The authors suggest that the framework is extensible to more complex causal concepts (such as actual cause and NESS causes) and other architectures, such as Convolutional BSNNs (C-BSNNs) and networks trained on language datasets, though these are identified as directions for future research rather than current achievements.