Neuron Activation-based Computation of Logical Explanations for Deep Neural Networks
Authors: Tomáš Kolárik, Faezeh Labbaf, Fabrizio Leopardi, Grigory Fedyukovich, Michael Wand, Natasha Sharygina
Organizations: University of Lugano (USI), Lugano, Switzerland · Florida State University, United States of America · SUPSI, IDSIA, Lugano, Switzerland
Formal explainability of classifying neural networks (NNs) is an active area of research, providing explanations with provable guarantees of the classification within continuous regions of the input feature space. However, the existing techniques are either limited to individual input features without guarantees on their relations or the provided solutions fail to scale to deep architectures. This paper addresses these issues by introducing a flexible symbolic framework for an efficient, guided computation of explanations of the NN behavior, parametrized by the activations of internal neurons, and using logical engines such as SMT solvers. Unlike prior methods that rely on specialized NN verifiers, our method yields explanations that are not restricted in shape. Our algorithm is implementable on top of a general-purpose logical solver, isolating the NN-specific encoding from the algorithmic framework. We experimented with a wide range of benchmarks from the domains of image recognition and medicine, illustrating the advantages of the new method, particularly in computational efficiency. Notably, our approach enables logical explanation of deep networks not amenable to prior logic-based methods.
Figures & tables
Figure 1: Neuron activation-based framework for automated computation of logical explanations, which takes as input a sample point, NN, the classification, and configurations of internal neurons, and outputs a logical explanation.
Figure 2: Performance comparison of our methods and interpolation algorithms. In medical datasets, it shows PAR-2 only up to 40 to make methods other than Direct visible.
Figure 4: Visual comparison of selected 2D snapshots of explanation spaces of the heart-attack dataset (with two classes: high and low risk) produced by different methods.
Figure 6: Performance of an enumerative invariant discovery with/without fixing.
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 7: A simple neural network example
Figure 8: Performance comparison with VeriX on networks with 200 neurons per layer.
Logic-based methods for explaining neural network decisions offer formal guarantees of correctness and non-redundancy, but they often suffer from high computational costs, especially for large networks. In this work, we improve the efficiency of such methods by combining bound propagation with constraint simplification. These simplifications, derived from the propagation, tighten neuron bounds and eliminate unnecessary binary variables, making the explanation process more efficient. Our experiments suggest that combining these techniques reduces explanation time by up to 89.26%, particularly for larger neural networks.
Ronaldo Gomes, Jairo Ribeiro, Luiz Queiroz +1
Department of Computer Science, Instituto Federal do Ceará (IFCE), Maracanaú, Brazil
Neural networks (NNs) are pervasive across various domains but often lack interpretability. To address the growing need for explanations, logic-based approaches have been proposed to explain predictions made by NNs, offering correctness guarantees. However, scalability remains a concern in these methods. This paper proposes an approach leveraging domain slicing to facilitate explanation generation for NNs. By reducing the complexity of logical constraints through slicing, we decrease explanation time by up to 40% less time, as indicated through comparative experiments. Our findings highlight the efficacy of domain slicing in enhancing explanation efficiency for NNs.
Luiz Fernando Paulino Queiroz, Carlos Henrique Leitão Cavalcante, Thiago Alves Rocha
Instituto Federal do Ceará (IFCE), Maracanaú, Ceará, Brazil
We propose FAME (Formal Abstract Minimal Explanations), a new class of abductive explanations grounded in abstract interpretation. FAME is the first method to scale to large neural networks while reducing explanation size. Our main contribution is the design of dedicated perturbation domains that eliminate the need for traversal order. FAME progressively shrinks these domains and leverages LiRPA-based bounds to discard irrelevant features, ultimately converging to a formal abstract minimal explanation. To assess explanation quality, we introduce a procedure that measures the worst-case distance between an abstract minimal explanation and a true minimal explanation. This procedure combines adversarial attacks with an optional VERIX+ refinement step. We benchmark FAME against VERIX+ and demonstrate consistent gains in both explanation size and runtime on medium- to large-scale neural networks.
Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe +2
Airbus SAS, France · IRT Saint-Exupery, France · The Hebrew University of Jerusalem, Israel