Abstract
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 (FXAI), 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.
Methodology: Formal Abduction in Latent Space
We propose a framework to generate Abductive Latent Explanations (ALEs). Unlike pixel-based methods which are often NP-complete, our approach operates on the latent manifold $\mathcal{Z}$, leveraging the fixed positions of prototypes to generate solver-free guarantees.
1. Formal Definition (ALE)
Given an input $v$ and a predictor $\kappa$, an ALE is a subset of latent features $\mathcal{E} \subseteq P \times L$ that entails a precondition $\phi_{\mathcal{E}}$ satisfied by the input. The explanation is valid if it logically entails the prediction $c$:
$$ \forall x \in \mathcal{F}, \quad \phi_{\mathcal{E}}(f(x), f(v)) \Rightarrow (\kappa(x) = c) $$We specifically seek subset-minimal explanations, ensuring that removing any single feature-prototype pair $(z_l, p_j)$ from $\mathcal{E}$ breaks the sufficiency guarantee.
2. Verification via Class Domination
To verify an explanation $\mathcal{E}$ without a solver, we construct the Maximally Class-Favoring Element $a^*_{\mathcal{E}}$. We verify if the predicted class $c$ dominates an alternative class $k$ even under the worst-case bounds:
$$ h_k(a_{\mathcal{E}}^*(k,c)) - h_c(a_{\mathcal{E}}^*(k,c)) \le 0 $$If this holds for all $k \neq c$, the explanation is formally verified (Theorem 2). This turns the verification problem into a polynomial-time check rather than an expensive logical search.
Visualizing the Latent Bounds
To certify an explanation without a solver, we must bound the location of the latent vector $z$. We compare our two paradigms below. The Hypersphere Intersection (Right) yields potentially tighter bounds (blue dashed line) than the Triangle Inequality (Center), approximating the true distances (Left) more accurately.
Ground Truth
True distances $d(P, z)$ and $d(P, z')$ in the latent space.
Ref: 0.846 | 1.364
Paradigm 1:
Triangle Inequality
Loose bounds derived from distances between prototypes.
Range: [0.656, 1.600]
Paradigm 2:
Hypersphere Intersection
Tighter bounds by intersecting constraints.
Range: [0.839, 1.368]
Experimental Results
We evaluated our approach on diverse datasets (CIFAR-10, MNIST, Oxford Flowers, etc.). The table below summarizes the average explanation sizes. Note that Spatial ALEs frequently yields more compact explanations or tighter bounds compared to the top-$k$ heuristic.
Framework
Our models were trained using CaBRNet (Case-Based Reasoning Network), an open-source library designed for developing and evaluating prototype-based models.
BibTeX
@inproceedings{Soria2026formal,
title={Formal Abductive Latent Explanations for Prototype-Based Networks},
author={Soria, Jules and Chihani, Zakaria and Girard-Satabin, Julien and Grastien, Alban and Xu-Darme, Romain and Cancila, Daniela},
booktitle={Proceedings of the AAAI Conference on Artificial Intelligence},
volume={40},
number={30},
pages={25590--25598},
year={2026}
}Acknowledgements
This publication was made possible by the use of the FactoryIA supercomputer, financially supported by the Ile-De-France Regional Council. This work was also supported by the SAIF project, funded by the "France 2030" government investment plan managed by the French National Research Agency, under the reference ANR-23-PEIA-0006.
This work has been extended in our ECML PKDD 2026 paper, Beyond $L_2$: Generalizing Abductive Latent Explanations to Diverse Prototype-Based Architectures.