Causal Models of Convolutional Binary Spiking Neural Networks for Explanation

We propose a novel logic-based causal approach to explaining convolutional binary spiking neural networks (C-BSNNs). Specifically, we provide an SMT (Satisfiability Modulo Theories) encoding of the binary causal model (BCM) underlying a C-BSNN and use it to compute formally correct abductive explanations for its outputs. We demonstrate that our SMT-based causal analysis extends beyond static inputs, preserving the recurrent temporal dependencies of spiking dynamics to support formal explanations of complex event-based DVS-Gesture data alongside static MNIST. To enable training of our networks with Batch Normalization while preserving the Boolean activations of neuronal units required for mapping them to BCMs and subsequent SMT encoding, we introduce a novel Batch Normalization absorption procedure. Finally, we compare our logic-based causal approach with SHAP with respect to the relevance of the elements included in an explanation. While our approach provides a formal guarantee that all such elements are relevant, SHAP provides no such guarantee.