Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Explanations for Neuro-Symbolic AI

Sushmita Paul, Jinqiang Yu, Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey

TL;DR

Experimental results for a few complex reasoning tasks demonstrate practical efficiency of the proposed approach, in comparison to purely neural systems, from the perspective of explanation size, explanation time, training time, model sizes, and the quality of explanations reported.

Abstract

Despite the practical success of Artificial Intelligence (AI), current neural AI algorithms face two significant issues. First, the decisions made by neural architectures are often prone to bias and brittleness. Second, when a chain of reasoning is required, neural systems often perform poorly. Neuro-symbolic artificial intelligence is a promising approach that tackles these (and other) weaknesses by combining the power of neural perception and symbolic reasoning. Meanwhile, the success of AI has made it critical to understand its behaviour, leading to the development of explainable artificial intelligence (XAI). While neuro-symbolic AI systems have important advantages over purely neural AI, we still need to explain their actions, which are obscured by the interactions of the neural and symbolic components. To address the issue, this paper proposes a formal approach to explaining the decisions of neuro-symbolic systems. The approach hinges on the use of formal abductive explanations and on solving the neuro-symbolic explainability problem hierarchically. Namely, it first computes a formal explanation for the symbolic component of the system, which serves to identify a subset of the individual parts of neural information that needs to be explained. This is followed by explaining only those individual neural inputs, independently of each other, which facilitates succinctness of hierarchical formal explanations and helps to increase the overall performance of the approach. Experimental results for a few complex reasoning tasks demonstrate practical efficiency of the proposed approach, in comparison to purely neural systems, from the perspective of explanation size, explanation time, training time, model sizes, and the quality of explanations reported.

Formal Explanations for Neuro-Symbolic AI

TL;DR

Experimental results for a few complex reasoning tasks demonstrate practical efficiency of the proposed approach, in comparison to purely neural systems, from the perspective of explanation size, explanation time, training time, model sizes, and the quality of explanations reported.

Abstract

Despite the practical success of Artificial Intelligence (AI), current neural AI algorithms face two significant issues. First, the decisions made by neural architectures are often prone to bias and brittleness. Second, when a chain of reasoning is required, neural systems often perform poorly. Neuro-symbolic artificial intelligence is a promising approach that tackles these (and other) weaknesses by combining the power of neural perception and symbolic reasoning. Meanwhile, the success of AI has made it critical to understand its behaviour, leading to the development of explainable artificial intelligence (XAI). While neuro-symbolic AI systems have important advantages over purely neural AI, we still need to explain their actions, which are obscured by the interactions of the neural and symbolic components. To address the issue, this paper proposes a formal approach to explaining the decisions of neuro-symbolic systems. The approach hinges on the use of formal abductive explanations and on solving the neuro-symbolic explainability problem hierarchically. Namely, it first computes a formal explanation for the symbolic component of the system, which serves to identify a subset of the individual parts of neural information that needs to be explained. This is followed by explaining only those individual neural inputs, independently of each other, which facilitates succinctness of hierarchical formal explanations and helps to increase the overall performance of the approach. Experimental results for a few complex reasoning tasks demonstrate practical efficiency of the proposed approach, in comparison to purely neural systems, from the perspective of explanation size, explanation time, training time, model sizes, and the quality of explanations reported.

Paper Structure

This paper contains 17 sections, 1 theorem, 2 equations, 6 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Datalog, Satisfiability and Unsatisfiability.
  4. Classification Problems
  5. Neuro-Symbolic AI
  6. Formal Explainability and Adversarial Robustness.
  7. Hierarchical Explanations
  8. Experimental Results
  9. Evaluated Explanation Methods
  10. Benchmarks and Neural Architectures
  11. Evaluation
  12. Model Training Time Statistics.
  13. On Explanation Sizes.
  14. On Explanation Quality.
  15. Sorting Heuristics for HX-Marabou.
  16. ...and 2 more sections

Key Result

Proposition 1

Let $c=\kappa_\sigma\left(\kappa_\eta(\mathbf{x}_1),\ldots,\kappa_\eta(\mathbf{x}_n)\right)$, $\mathbf{x}_j\in\mathbb{F}$, $j\in[n]$, be a decision made by a neuro-symbolic system involving a neural component $\kappa_\eta:\mathbb{F}\rightarrow\mathbb{Y}$ and a symbolic component $\kappa_\sigma:\prod

Figures (6)

  • Figure 1: Example of a Pacman related puzzle aiming to find a shortest grid path from the actor's location to the target flag. Given an input instance, the model predicts the length of a shortest path.
  • Figure 2: A general setup for explaining neuro-symbolic AI.
  • Figure 3: Hierarchical formal explanations. The system seeks to determine whether a given number handwritten in binary (top row) is greater than the other handwritten binary number (bottom row).
  • Figure 4: Given the two 4-digit binary numbers, explain whether the top number is greater than the bottom number.
  • Figure 5: Explain whether the binary string is a member of the regular language $R_2$.
  • ...and 1 more figures

Theorems & Definitions (6)

  • Example 1
  • Example 2
  • Example 3
  • Definition 1: Hierarchical Abductive Explanation
  • Example 4
  • Proposition 1