Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparing Neural Network Encodings for Logic-based Explainability

Levi Cordeiro Carvalho, Saulo A. F. Oliveira, Thiago Alves Rocha

TL;DR

This work tackles the challenge of providing correct, minimal explanations for neural network predictions by translating ANN behavior into logic-based constraints solvable via MILP. It compares two encodings: the established fischetti approach using logical implications and an adapted tjeng encoding that avoids implications and reduces variable/constraint counts. Across 12 datasets and varying network depths, both encodings show similar times for explanation generation, with the tjeng-based adaptation delivering up to 18% faster constraint construction and up to 16% faster overall time. The findings advance the scalability of logic-based explainability and include publicly available implementations to support further research and application. The work highlights practical improvements in building explanations for moderate-sized networks and sets directions for evaluating larger architectures and alternative encodings.

Abstract

Providing explanations for the outputs of artificial neural networks (ANNs) is crucial in many contexts, such as critical systems, data protection laws and handling adversarial examples. Logic-based methods can offer explanations with correctness guarantees, but face scalability challenges. Due to these issues, it is necessary to compare different encodings of ANNs into logical constraints, which are used in logic-based explainability. This work compares two encodings of ANNs: one has been used in the literature to provide explanations, while the other will be adapted for our context of explainability. Additionally, the second encoding uses fewer variables and constraints, thus, potentially enhancing efficiency. Experiments showed similar running times for computing explanations, but the adapted encoding performed up to 18\% better in building logical constraints and up to 16\% better in overall time.

Comparing Neural Network Encodings for Logic-based Explainability

TL;DR

This work tackles the challenge of providing correct, minimal explanations for neural network predictions by translating ANN behavior into logic-based constraints solvable via MILP. It compares two encodings: the established fischetti approach using logical implications and an adapted tjeng encoding that avoids implications and reduces variable/constraint counts. Across 12 datasets and varying network depths, both encodings show similar times for explanation generation, with the tjeng-based adaptation delivering up to 18% faster constraint construction and up to 16% faster overall time. The findings advance the scalability of logic-based explainability and include publicly available implementations to support further research and application. The work highlights practical improvements in building explanations for moderate-sized networks and sets directions for evaluating larger architectures and alternative encodings.

Abstract

Providing explanations for the outputs of artificial neural networks (ANNs) is crucial in many contexts, such as critical systems, data protection laws and handling adversarial examples. Logic-based methods can offer explanations with correctness guarantees, but face scalability challenges. Due to these issues, it is necessary to compare different encodings of ANNs into logical constraints, which are used in logic-based explainability. This work compares two encodings of ANNs: one has been used in the literature to provide explanations, while the other will be adapted for our context of explainability. Additionally, the second encoding uses fewer variables and constraints, thus, potentially enhancing efficiency. Experiments showed similar running times for computing explanations, but the adapted encoding performed up to 18\% better in building logical constraints and up to 16\% better in overall time.

Paper Structure

This paper contains 11 sections, 3 theorems, 8 equations, 3 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. First-order Logic over LRA
  4. Mixed Integer Linear Programming
  5. Classification Problems and Artificial Neural Networks
  6. Explanations for ANNs with Logical Implications
  7. Explanations for ANNs without Implications
  8. Experiments
  9. Experimental Setup
  10. Results
  11. Conclusions and future work

Key Result

proposition thmcounterproposition

Let $C$ be an instance predicted as a class $c \in \mathcal{K}$ by an ANN, the formula $C \wedge F \wedge \neg E$ has $n_0 + n_L + 2\sum_{l=1}^{n_{L-1}} n_l$ real variables and $n_L - 1 + \sum_{l=1}^{n_{L-1}} n_l$ binary variables. Also, the formula has $n_0 + 2n_L + 5\sum_{l=1}^{n_{L-1}}$ constrain

Figures (3)

  • Figure 1: Flowchart for calculating explanations.
  • Figure 2: Comparison of average running time for computing explanations, using ANNs with one hidden layer and the voting dataset.
  • Figure 3: Comparison of average running time for computing explanations, using ANNs with two hidden layers and the voting dataset.

Theorems & Definitions (4)

  • proposition thmcounterproposition
  • proposition thmcounterproposition
  • proof
  • proposition thmcounterproposition