Neural networks (NNs) are the core of AI-based technologies. However, the degree of reliability in performing the task is an open problem. The explainability of a central task of NNs, classification, is of immense importance. While at the rise of AI-based reasoning, explainability of the NN classification has mostly been done using statistical methods, nowadays, a more reliable trend of formal logic-based methods is gaining popularity. The advantage of the formal approach is that it gives strict and provable guarantees of the classification. Formal methods are a mature field that has delivered a number of efficient computational solutions already applied in the analysis of software and hardware systems. Formal explainability methods naturally have the ability to reuse existing techniques and tools for a newly emerging field of formal explainability of NN classification.

This tutorial will survey existing efforts to compute explanations of neural network classification based on logical abductive reasoning. The abduction approach is crucial for generalizing the results, capturing the underlying behavior of the classifier. We will present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we will discuss the issue of the quality of explanations, focusing on their key metrics and factors. As an illustrative example, we will also present a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abduction-based explanations for classifying NNs with provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages an SMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation, and is applicable to a wide range of applications.

Using the SpEXplAIn tool and several neural networks from the medical domain and image recognition, we will compute logical explanations and illustrate their interpretations for the user, focusing on various aspects of explanation quality. We will demonstrate that the flexibility of logical reasoning algorithms can be utilized for the benefit of producing explanations of different precision. We will conclude by contrasting the generality and scalability of SpEXplAIn against the state-of-the-art abduction-based XAI tool VeriX.

The tutorial will be presented by experts in formal verification, Prof. Dr. Natasha Sharygina and Dr. Tomáš Kolárik, the director and a senior member of the Formal Verification and Security Lab at the University of Lugano, Switzerland. www.verify.inf.usi.ch