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.

In the field of Explainable AI, multiples evaluation metrics have been proposed in order to assess the quality of explanation methods w.r.t. a set of desired properties. In this work, we study the articulation between the stability, correctness and plausibility of explanations based on feature importance for image classifiers. We show that the existing metrics for evaluating these properties do not always agree, raising the issue of what constitutes a good evaluation metric for explanations. Finally, in the particular case of stability and correctness, we show the possible limitations of some evaluation metrics and propose new ones that take into account the local behaviour of the model under test.