Case-based reasoning networks are machine-learning models that make predictions based on similarity between the input and prototypical parts of training samples, called prototypes. Such models are able to explain each decision by pointing to the prototypes that contributed the most to the final outcome. As the explanation is a core part of the prediction, they are often qualified as "interpretable by design". While promising, we show that such explanations are sometimes misleading, which hampers their usefulness in safety-critical contexts. In particular, several instances may lead to different predictions and yet have the same explanation. Drawing inspiration from the field of formal eXplainable AI (formal XAI), we propose Abductive Latent Explanations (ALEs), a formalism to express sufficient conditions on the intermediate (latent) representation of the instance that imply the prediction. Our approach combines the inherent interpretability of case-based reasoning models and the guarantees provided by formal XAI. We propose a solver-free and scalable algorithm for generating ALEs based on three distinct paradigms, compare them, and present the feasibility of our approach on diverse datasets for both standard and fine-grained image classification.

In the field of explainable Artificial Intelligence (xAI), attribution methods provide off-the-shelf tools to explain the decision of a machine-learning model. However, existing methods usually do not correctly reflect the actual model behaviour, and they are difficult to compare, due to a lack of ground truth and/or consensus on what a correct explanation should be. Meanwhile, existing work leveraging formal verification to attribution methods is promising but suffer from scalability issues. In this study, we propose a Formally Grounded Correctness (FGC) metric to measure the correctness of existing attribution methods using formal verification. FGC can be used to rank popular explanation methods according to their correctness, ensuring that explanations are correct with regards to the model decision. To allow the application of FGC on more challenging datasets, we propose to use sound, incomplete algorithms, that trade accuracy for scalability, with existing work on input segmentation. We extensively benchmark FGC on MNIST, GTSRB and a scaled down version of ImageNet with several state-of-the-art provers and show its practical usefulness. FGC surprisingly shows that the baseline saliency heuristic is a strong baseline with regards to correctness, sheding light on some caveats of other popular explanation techniques.

Abstract Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

International audience