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 diferent 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 suficient 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 and present the feasibility of our approach on the CUB 200 dataset for the task of fine-grained image classification.
A widely adopted approach to explain neural network decisions is to analyze the decisions of a model
after its training, in a post-hoc fashion [
However, such approaches are not without flaws. They have been shown to be sensitive to malign manipulations [6], raising questions on their usefulness in an adverse setting [7]. Moreover, some attribution methods may not correlate to the actual model behavior [8, 9] - raising questions on what they actually aim to explain - or display irrelevant features [10]. Finally, their usefulness on actual scenarios with actual humans has been questioned [11].
To overcome such limitations, the emerging field of formal explainable AI (FXAI) [ 12, 13, 14, 15, 16] provides a rigorous framework to characterize and build explanations. A particular line of work exemplified by [ 13, 14, 17, 18] builds upon the framework of abductive reasoning: explanations are defined as a subset of features that are suficient to justify the model decision. In particular, it is possible to produce subset-optimal explanations within this framework, such that removing any single feature from such explanations changes the classifier’s decision. FXAI provides strong guarantees on the relevance of features in the explanation, thanks to the use of automated provers that directly query the model. As such, FXAI represents a good compromise between compactness and correctness — which are deemed important characteristics of an explanation [19, 20] — and a stepping stone in line with new regulations. Indeed, to reach compliance with the AI Act (article 86 states "Any afected person subject to a decision which is taken by the deployer on the basis of the output from a high-risk AI [. . . ] shall have the right to obtain [. . . ] clear and meaningful explanations of the role of the AI system [. . . ]), the correctness of explanations is of paramount importance.
Although FXAI is a promising approach, it sufers from two main shortcomings: 1. these approaches rely on expensive prover calls, which limits their scalability on realistic computer vision tasks (the associated problems are generally NP-complete [21]); 2. abductive FXAI provides explanations at the feature-level, which, for typical computer vision applications, is a pixel. We argue that the pixel-level is not the correct level of abstractions for the human final user of the explanation. Pixel-level explanations rely on the model’s perception of the problem, setting a knowledge gap between the human and the machine [20]. Higher-level reasoning like prototypes or concepts allow generalizing facts towards higher-level reasoning [22].
An orthogonal approach involves implementing case-based reasoning. Under this setting, the neural network is designed to justify its decision by exposing examples from its dataset that are similar to the new sample. Such approach is exemplified by prototype learning [ 23, 24, 25, 26, 27, 28] or concept learning [29, 30, 31, 32, 33, 34].
In this paradigm, explanations justify the decision by exposing a certain number of prototypes or concepts to the user. One major drawback is that the presented prototypes are usually not suficient to entail the decision. Indeed, the number of prototypes in the popular architecture ProtoPNet [35] is ifxed as an arbitrary hyperparameter. This produces explanations that may omit relevant prototypes taken for the decision, resulting in misleading explanations.
Table 1 summarizes and qualitatively compares these methods, highlighting how our proposed approach achieves (at least partially) three key properties: interpretability, faithfulness, and suficiency. 1. We propose a generic framework to describe Abductive Latent Explanations (ALE) for prototype-based networks. This formalism can be instantiated for any neural network architecture that relies on identifying concept-rich prototypical parts and reasons on their activations to reach a final decision. 2. We leverage uncertainties on prototype activations to circumvent the need for costly prover calls.
This allows us to produce explanations that are guaranteed to secure the model’s prediction in a computationally eficient manner.
1. an image encoder whose goal is to map the input image to a latent representation space; 2. a prototype layer that measures the distance between the latent representation of the image and learned prototypes, and assigns to them an activation score; 3. a decision layer that gives each class a score and chooses the class with the highest score as its prediction.
In the rest of the paper, we capitalize on the prototype and decision layers as defined in the original ProtoPNet architecture [35] and follow-ups [27] as they represent the state-of-the-art of prototype-based models, and implementations are readily available [36].
To give an intuition on abductive explanations in the latent space, we will provide a running example after introducing the notations used in the paper, further illustrated in Figure 1.
We briefly summarize here the notations used throughout the paper. The predictor function : ℱ → is defined as = argmax ∘ ℎ ∘ a ∘ , where maps inputs to the latent space, a computes prototype activations, and ℎ produces class logits. The similarity matrix sim(z, p), with p = (p )∈P, has entries sim(z, p ) for ∈ L, ∈ P. Explanations ℰ ⊆ P, as detailed in Section 3.
We consider a 2-class classification problem with emperor_penguin and royal_penguin.
During inference, an image input v first goes through an image encoder and is represented as z, i.e. an object in the latent space , which sums up the important concepts locally identified. This latent representation is composed of four (1 × 1) latent vectors, where width 1 = 2, and height 1 = 2 (as shown in Figure 1).
A prototype is a latent vector from a training image that the training procedure has identified as prototypical of some class. In this example, we assume that the training procedure computed ifve prototypes. We further assume that these prototypes can be linked to the following concepts: emperor_beak, emperor_yellow_neck_patch, black_back_white_belly, royal_beak, and royal_yellow_crests (these labels are solely used to make the example comprehensible; they are neither inputs of the training nor produced by it). We use p to refer to the vector of prototypes and p for the th prototype.
Secondly, the prototype layer sim(z, p) computes a similarity score between each latent vector (row) and the prototypes (column):
⎡1. 0. 1. 0. 1.⎤ sim(z, p) = ⎢⎢⎣10.. 13.. 00.. 21.. 12..⎦⎥⎥
0. 0. 1. 8. 0. where higher value means higher similarity. In this example, the fourth prototype (royal_beak, fourth column) has been strongly recognized in the bottom-right part of the image (fourth row), hence a similarity score of 8. Similarly, the second prototype (emperor_yellow_neck_patch) is moderately recognized, because of similarity score of 3., while the other prototypes are absent (score 2 or lower). For each prototype, the ProtoPNet architecture is only interested in the top similarity, and computes the column-wise maximum value of sim(z, p) called the activation vector
a(z) = [︀ 1. 3. 1. 8. 2.]︀ These values mean that the network detected a clear royal beak and what appears to be an emperor yellow neck patch while no other attribute one would expect from a penguin stands out.
Thirdly, in the decision layer, the prototype activation vector is fed to a fully connected linear layer with learned parameters where = ︂[ 10. 10. 7. 0. 0. ]︂
0. 0. 5. 10. 15. Matrix indicates that prototypes 1 and 2 are typical of emperor penguins (weights 10. against 0.) and prototypes 4 and 5 of royal penguins (weights 10. and 15. versus 0.), while prototype 3 can be detected in both classes. The decision layer’s computation returns the final class scores: ℎ(a(z)) = a(z) = [︀ 47. 115.]︀ and the classifier thus outputs the second class: (z) = argmax ℎ(a(z)) = 2, i.e., royal_penguin.
ProtoPNet returns as an explanation the prototypes with highest activation. In the running example, if = 1, the explanation is ℰ = {4} which involves {p4 : 8.}. We highlight that the above explanation implicitly entails that the score of all other prototypes is 8. or below. At the first glance, such an explanation can appear appropriate: the bird on the image is classified as a royal_penguin because a royal beak (typical of royal penguins) has been observed.
However, a closer examination reveals that the explanation is wrong for some instances. Counterexample: let be an image having latent representation z′ such that the activation evaluates to a(z′) = [︀ 6. 7. 1. 8. 2.]︀ The classification is (z) = arg max [︀ 137. 115.]︀ = 1 while the previous explanation is still applicable to emperor_penguin “because it shows a royal beak”. In other words, the explanation is misleading or optimistic as discussed in [37]. Hence, the need for formal guarantees on prototypes explanations abductive latent-based explanations. 3. Abductive explanations in the prototype space An Abductive explanation (AXp) for v is traditionally defined as a condition on the input of a classifier satisfied by the current instance such that all instances that satisfy this condition yield the same output [38]. In other words, an AXP defines preconditions on the inputs of a classifier, yielding a postcondition on the classification of said classifier [ 39]. Formally, given an input space ℱ , a predictor from ℱ to , and an input instance v ∈ ℱ with prediction = (v) ∈ , a formal explanation is a precondition ℰ (x, v) over input x satisfied by v such that this holds:
∀x ∈ ℱ . ℰ (x, v) ⇒ ((x) = ).
In previous works [13], the explanation is represented as a conjunction ℰ of input variables (features), and the precondition simply states that the assignments of these variables should match those of v: ℰ (x, v) = ⋀︁(x = v),
∈ℰ Our main contribution is the extension of the definition of AXps to an arbitrary latent space.
In the case of image recognition, an explanation is a subset of the image pixels (if grayscale, else pixel color channels). While this explanation is correct—i.e., any image that includes these specific pixels will be classified as the input image—its interpretability is questionable.
Since explanations are preconditions on the input space of the classifier, in the context of case-based reasoning, we can define such precondition on the input of the latent classifier: following holds: ℰ ( (x), (v)) over (x) satisfied by (v).
Definition 1 (Abductive Latent Explanation (ALE)). Given an input instance v with latent representation (v), an abductive latent explanation is a subset of (latent) features ℰ that entails a precondition Given an input space ℱ and a predictor = ∘ from ℱ to , the explanation is correct if the ∀x ∈ ℱ . ℰ ( (x), (v)) ⇒ ((x) = ).
Definition 2 (ProtoPNet Explanation). Given a set P of prototype indices, a ProtoPNet explanation ℰ ⊆ P is a subset of indices that implicitly represents the ALE ℰ (z, y) = ︃( ⋀︁ a(z) = a(y) ∈ℰ )︃
⎛ ∧ ⎝
⋀︁ ̸∈ℰ,∈ℰ
⎞ a (z) ≤ a (y)⎠ .
Compared to the pixel-based abductive explanations, we consider that ALEs are more interpretable as they refer to the concepts that humans are able to manipulate. Furthermore, compared to relevancebased explanations, ALEs provide formal guarantees as it is impossible to come up with misleading explanations.
We note however that ProtoPNet explanations (from Definition 2), as will also be the case for the explanations introduced in the next section, implicitly include the clause “under the assumption that function is a proper encoding of the input image into a latent space”. Indeed, some important steps of the procedure for computing the similarity scores are hidden from the user. Nonetheless, we consider that these explanations are an important improvement over the existing work. 4. Building abductive explanations in the prototype space The explanations proposed in the previous section assume that the human agrees with the fact that the activation scores in the returned explanation are the top- elements. However, the explanation does not ‘prove’ that this fact holds. In this section, we propose an extension of the definition of an explanation that relies on the bounds of the final class logits.
Here, explanations will be used to prove bounds over activations. Thus, an explanation will implicitly entail a condition of the form ⎛ =1
⎞ ℰ (z, y) = ⎝ ⋀︁ a (z) ∈ ︀[ aℰ, , aℰ, ⎠ .
︀]
This paradigm is the one used implicitly by the original explanation [35] provided by ProtoPNet. It traverses the prototype activation scores in decreasing order, with the added knowledge that, for that prototype, the similarity scores with the other latent space feature vectors are lesser than the activation score (result of the max function). In that scenario, we obtain aℰ from ℰ by: ∀ ∈ ℰ . aℰ, = aℰ, = a (y) ∀ ∈/ ℰ . aℰ, = 0 and aℰ, = min a(y) ∈ℰ Constructing Abductive Latent Explanations (ALE) Given a candidate explanation ℰ ⊆ P, the constrained prototype activation space is aℰ = [0, max aℰ, ]
Constructing an abductive latent explanation ℰ in the prototype activation space involves defining preconditions on a generic activation vector a ∈ R. These preconditions are derived from ℰ and a(y). Crucially, they must guarantee that any activation vector a satisfying these conditions results in the same predicted class : ∀a ∈ aℰ ⊆ R : a |= ℰ , argmax ℎ(a) = ∈ These preconditions efectively define a constrained region - or set of constraints aℰ within the activation space R - such that a(y) satisfies these constraints, and all vectors within this region yield the prediction . By making Assumption 1, our proposed explanation method can be applied to any prototype-based model that has a Linear layer for its decision head ℎ that links the prototype activations to the class logits in the form of a weighted sum.
Assumption 1 (Linear Logit Diference). For any two classes , , the diference between their logit functions is linear in the prototype activation vector a:
ℎ(a) − ℎ (a) = ∑︁( − ) a + ( − )
=1 for some weights , and biases , .
Definition 3 (Maximally Class-Favoring Element within aℰ ). For a given explanation ℰ , predicted class , and alternative class ̸= , the maximally (/)-favoring prototype activation vector within aℰ is denoted by a*ℰ (, ) and satisfies:
∀a ∈ aℰ . ℎ(a*ℰ (, )) − ℎ (a*ℰ (, )) ≥ ℎ (a) − ℎ (a) Under Assumption 1, its components (a*ℰ (, )) are constructed as: (a*ℰ (, )) = {︃(aℰ ) if ≥
(aℰ ) if <
One way to intuitively understand this item is to view it as the element that satisfies the condition expressed by the explanation, and that causes the most the classifier from reaching the initial prediction (in favor of a specific diferent class).
Definition 4 (Class-wise Prediction Domination within aℰ ). For explanation ℰ , predicted class , and alternative class ̸= , we say dominates within ℰ , denoted ℰ (, ), if the logit of is greater than or equal to the logit of even for the maximally (/)-favoring vector:
ℰ (, ) ⇐⇒ ℎ(a*ℰ (, )) ≥ ℎ (a*ℰ (, )) Definition 5 (Total Prediction Domination within aℰ (Explanation Verification)). A candidate explanation ℰ is considered verified if class dominates all other classes ̸= within the constrained space ℰ :
Verify(ℰ ) ⇐⇒ ∀ ∈ {1, . . . , } ∖ {}, ℰ (, )
In Definition 4 we say that a class (diferent from the predicted class) is verified if its Maximally ClassFavoring Element does not entail a diferent classification. In Definition 5 we say that the explanation verifies the prediction if all classes are verified.
According to Theorem 1, if an explanation ℰ is verified according to Definition 5, it satisfies the original abductive explanation definition (Definition 1).
Theorem 1 (Verified Explanation is Suficient). Let ℰ be a candidate explanation for the decision (v, ). If ℰ is verified according to Definition 5 (i.e., Verify(ℰ ) is true), then ℰ is a valid abductive explanation according to Definition 1.
We present the pseudo-code for Algorithm 1 used to generate an ALE in Section 4. The function NextPrototype we use returns the prototype with the highest activation score among the ones not included already in the explanation ℰ . Following the reasoning used to derive Theorem 1 and the associated definitions 3, 4, 5, we iteratively add the highest remaining activation score until it becomes impossible to create a sample that satisfies the explanation and has a diferent predicted class.
Our experiments were conducted on a SLURM-managed computing cluster, primarily utilizing GPUequipped nodes for computationally intensive tasks, with each node featuring 48 cores at 2.6GHz, 187GB of RAM, four NVIDIA V100 32GB GPUs, and a 1.9TB local SSD.
Our study uses the Case-Based Reasoning Network (CaBRNet) framework [36] to train and manipulate the model. CaBRNet integrates concepts from case-based reasoning into a deep learning framework, leveraging learned prototypes for classification.
We use a model trained by CaBRNet, with a VGG-19 backbone pretrained on ImageNet [40], and 10 prototypes per class (as is the standard for case-based reasoning training). For reference, it obtains 68% accuracy on the test set.
The Caltech-UCSD Birds-200-2011 dataset (CUB200) [41] contains 11,788 images spanning 200 species of North American birds (thus, the total number of prototypes was = 10 × 200 = 2000 ). It is a widely used benchmark for fine-grained image classification, featuring detailed annotations including bounding boxes and part locations. We used the standard train/test splits provided by the dataset creators and followed common preprocessing procedures, such as resizing and cropping and data augmentation techniques, described in [35].
We show that the 10 most activated prototypes are never enough to guarantee the decision. Indeed, in practice 427 similarity scores are required on average to generate an ALE. This result is significant as it entails that (for the model used) all previous ProtoPNet explanations were misleading, or optimistic ; i.e., there exists samples that match the provided explanations and had a distinct classification.
Furthermore, Table 2 shows that, for samples that are incorrectly classified, the average explanation size is much higher. This would mean that information about a sample and the data distribution can be extracted from the computation of ALEs.
However, it would be dishonest to say that an explanation that contains hundreds of prototypes and associated activation scores is interpretable, especially to a human receiver. Indeed, the cardinality of an explanation influences its interpretability and usefulness ; a larger explanation will be harder to follow and understand for the user [20].
We respond to this issue in two ways: first, our proposed method primarily focuses on generating
explanations that are suficient to guarantee the decision, as this is the key property we want in an
explanation. This means that, if there is a trade-of between explanation size and suficiency, we will
always prioritize suficiency. Then, large suficient explanations can be due to the model itself. Although
one of the ProtoPNet’s training objective is to have latent representation vectors of training images far
away from other classes’ prototypes [35], it can have in the end a very “disorganized” latent space, where
the separation between prototypes of diferent classes is unclear. When that is the case, generating small
suficient explanations will not be possible, which questions the self-explainable nature of ProtoPNet.
6. Comparing our methodology and tool with AI Act
Our work can be tied with article 86 of the AI Act [
In this work, we have introduced Abductive Latent Explanations (ALE), a novel framework that formalizes explanations for prototype-based networks as rigorous abductive inferences within the latent space. We proposed a solver-free algorithm for generating ALEs that drastically reduces the computation time. Our analysis, enabled by ALEs, reveals that common prototype-based explanations can be misleading, raising concerns about their reliability in high-stakes decisions.
Furthermore, we investigated the relationship between prediction correctness and ALE size, with ifndings showing that larger ALEs often correlate with incorrect predictions, suggesting ALE size as a potential proxy for model uncertainty.
While our current investigation focused on a specific class of prototypes, a significant direction for future work involves exploring the generalizability of ALEs across the diverse spectrum of prototype definitions and modalities found in the literature.
A primary challenge, and thus a key area for future research, is the considerable size of currently generated ALEs, which can impede human interpretability. Developing methods to compact these formal explanations is crucial. Success in this area would also contribute to more resource-eficient and sustainable XAI.
Enhancing the semantic quality of ALEs hinges on the interpretability of the underlying prototypes. Future work could explore how the formal properties or structures of ALEs might, in turn, inform or guide the learning of more human-aligned and explanatorily efective prototypes, potentially leading to more intrinsically compact ALEs. Exploring other modalities of prototypical parts, such as concept activation vectors lying in a diferent latent space, could result in more interpretable yet formal explanations.
The formal structure of ALEs provides a strong foundation for generating robust and diverse latentspace counterfactuals, ofering a promising avenue for future exploration.
Finally, ALEs could potentially identify non-salient or provably irrelevant latent components. Future work could develop techniques to leverage this information for targeted pruning or deactivation of such components, leading to more focused latent representations and, consequently, more concise ALEs.
Overall, this work bridges formal abductive reasoning with prototype-based networks, advancing XAI by ofering rigorous yet interpretable explanations. ALE not only addresses limitations in existing prototype explanations but also lays a foundation for future innovations in eficient, human-centric AI interpretability.
This publication was made possible by the use of the FactoryIA supercomputer, financially supported by the Ile-De-France Regional Council. This work was 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.
During the preparation of this work, the authors used Google Gemini and ChatGPT in order to: Grammar and spelling check. Further, the authors used the same tools in order to: Improve writing style. [3] M. Sundararajan, A. Taly, Q. Yan, Axiomatic attribution for deep networks, in: D. Precup, Y. W.
Teh (Eds.), Proceedings of the 34th International Conference on Machine Learning, volume 70 of Proceedings of Machine Learning Research, PMLR, 2017, pp. 3319–3328. URL: https://proceedings. mlr.press/v70/sundararajan17a.html. [4] C. L. Choi, A. Duplessis, S. Belongie, Unlearning-based neural interpretations, 2025. URL: https: //arxiv.org/abs/2410.08069. arXiv:2410.08069. [5] G. Montavon, A. Binder, S. Lapuschkin, W. Samek, K.-R. Müller, Layer-wise relevance propagation:
An overview, in: Explainable AI, 2019. [6] A.-K. Dombrowski, M. Alber, C. Anders, M. Ackermann, K.-R. Müller, P. Kessel, Explanations can be manipulated and geometry is to blame, in: Advances in Neural Information Processing Systems, volume 32, Curran Associates, Inc., 2019. [7] S. Bordt, M. Finck, E. Raidl, U. von Luxburg, Post-hoc explanations fail to achieve their purpose in adversarial contexts, in: 2022 ACM Conference on Fairness, Accountability, and Transparency, FAccT ’22, ACM, 2022, p. 891–905. URL: http://dx.doi.org/10.1145/3531146.3533153. doi:10.1145/ 3531146.3533153. [8] J. Adebayo, J. Gilmer, M. Muelly, I. Goodfellow, M. Hardt, B. Kim, Sanity Checks for Saliency Maps, in: Advances in Neural Information Processing Systems 32, 2018, p. 11. [9] A. Hedström, L. Weber, S. Lapuschkin, M. Höhne, A fresh look at sanity checks for saliency maps, 2024. URL: https://arxiv.org/abs/2405.02383. arXiv:2405.02383. [10] J. Marques-Silva, X. Huang, Explainability is not a game, Communications of the ACM 67 (2024) 66–75. doi:10.1145/3635301. [11] J. Colin, T. Fel, R. Cadene, T. Serre, What I Cannot Predict, I Do Not Understand: A Human-Centered Evaluation Framework for Explainability Methods, Technical Report, 2023. URL: http://arxiv.org/ abs/2112.04417. doi:10.48550/arXiv.2112.04417, zSCC: NoCitationData[s0] arXiv:2112.04417 [cs] type: article. [12] G. Audemard, S. Bellart, L. Bounia, F. Koriche, J.-M. Lagniez, P. Marquis, On the explanatory power of decision trees, 2021. URL: https://arxiv.org/abs/2108.05266. arXiv:2108.05266. [13] J. Marques-Silva, A. Ignatiev, Delivering trustworthy ai through formal xai, in: Proceedings of the
AAAI Conference on Artificial Intelligence, 2022, pp. 12342–12350. [14] S. Bassan, G. Katz, Towards formal xai: Formally approximate minimal explanations of neural networks, arXiv preprint arXiv:2210.13915 (2022). [15] W. Shi, A. Shih, A. Darwiche, A. Choi, On tractable representations of binary neural networks, 2020. URL: https://arxiv.org/abs/2004.02082. arXiv:2004.02082. [16] L. Wolf, T. Galanti, T. Hazan, A formal approach to explainability, in: Proceedings of the 2019
AAAI/ACM Conference on AI, Ethics, and Society, 2019, pp. 255–261. [17] A. De Palma, S. Durand, Z. Chihani, F. Terrier, C. Urban, On using certified training towards empirical robustness, 2024. doi:10.48550/ARXIV.2410.01617. [18] M. Wu, H. Wu, C. Barrett, Verix: Towards verified explainability of deep neural networks, 2023.
arXiv:2212.01051. [19] M. Nauta, J. Trienes, S. Pathak, E. Nguyen, M. Peters, Y. Schmitt, J. Schlötterer, M. Van Keulen, C. Seifert, From anecdotal evidence to quantitative evaluation methods: A systematic review on evaluating explainable ai, ACM Computing Surveys 55 (2023) 1–42. [20] T. Miller, Explanation in artificial intelligence: Insights from the social sciences, Artificial
Intelligence 267 (2019) 1–38. [21] G. Katz, C. Barrett, D. L. Dill, K. Julian, M. J. Kochenderfer, Reluplex: An Eficient SMT Solver for Verifying Deep Neural Networks, Springer International Publishing, 2017, pp. 97–117. doi:10. 1007/978-3-319-63387-9_5. [22] B. M. Lake, T. D. Ullman, J. B. Tenenbaum, S. J. Gershman, Building machines that learn and think like people, 2016. URL: https://arxiv.org/abs/1604.00289. arXiv:1604.00289. [23] C. Chen, O. Li, C. Tao, A. J. Barnett, J. Su, C. Rudin, This looks like That: Deep learning for interpretable image recognition, Proceedings of the 33rd International Conference on Neural Information Processing Systems (2019) 8930–8941. [24] A. V. Looveren, J. Klaise, Interpretable counterfactual explanations guided by prototypes, ArXiv abs/1907.02584 (2019). [25] M. Nauta, R. van Bree, C. Seifert, Neural prototype trees for interpretable fine-grained image recognition, 2021 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR) (2021) 14928–14938. doi:10.1109/cvpr46437.2021.01469. [26] D. Rymarczyk, Ł. Struski, M. Górszczak, K. Lewandowska, J. Tabor, B. Zieliński, Interpretable image classification with diferentiable prototypes assignment, in: European Conference on Computer Vision, Springer, 2022, pp. 351–368. [27] F. Willard, L. Mofett, E. Mokel, J. Donnelly, S. Guo, J. Yang, G. Kim, A. J. Barnett, C. Rudin, This looks better than that: Better interpretable models with protopnext, arXiv preprint arXiv:2406.14675 (2024). [28] M. Sacha, B. Jura, D. Rymarczyk, Ł. Struski, J. Tabor, B. Zieliński, Interpretability benchmark for evaluating spatial misalignment of prototypical parts explanations, in: Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, 2024, pp. 21563–21573. [29] B. Kim, M. Wattenberg, J. Gilmer, C. Cai, J. Wexler, F. Viegas, R. Sayres, Interpretability beyond feature attribution: Quantitative testing with concept activation vectors (tcav), 2018. URL: https: //arxiv.org/abs/1711.11279. arXiv:1711.11279. [30] T. Fel, A. Picard, L. Bethune, T. Boissin, D. Vigouroux, J. Colin, R. Cadène, T. Serre, CRAFT: Concept Recursive Activation FacTorization for Explainability, Technical Report, 2023. URL: http: //arxiv.org/abs/2211.10154. doi:10.48550/arXiv.2211.10154, zSCC: 0000057 arXiv:2211.10154 [cs] type: article. [31] F. De Santis, G. Ciravegna, P. Bich, D. Giordano, T. Cerquitelli, V-cem: Bridging performance and intervenability in concept-based models, arXiv preprint arXiv:2504.03978 (2025). [32] P. W. Koh, T. Nguyen, Y. S. Tang, S. Mussmann, E. Pierson, B. Kim, P. Liang, Concept bottleneck models, in: International conference on machine learning, PMLR, 2020, pp. 5338–5348. [33] M. Espinosa Zarlenga, P. Barbiero, G. Ciravegna, G. Marra, F. Giannini, M. Diligenti, Z. Shams, F. Precioso, S. Melacci, A. Weller, et al., Concept embedding models: Beyond the accuracyexplainability trade-of, Advances in Neural Information Processing Systems 35 (2022) 21400– 21413. [34] A. Helbling, T. H. S. Meral, B. Hoover, P. Yanardag, D. H. Chau, Conceptattention: Difusion transformers learn highly interpretable features, arXiv preprint arXiv:2502.04320 (2025). [35] C. Chen, O. Li, D. Tao, A. Barnett, C. Rudin, J. K. Su, This looks like that: deep learning for interpretable image recognition, Advances in neural information processing systems 32 (2019). [36] R. Xu-Darme, A. Varasse, A. Grastien, J. Girard, Z. Chihani, CaBRNet, an open-source library for developing and evaluating Case-Based Reasoning Models, in: Joint Proceedings of the xAI-2024 Late-breaking Work, Demos and Doctoral Consortium co-located with the 2nd World Conference on eXplainable Artificial Intelligence (xAI-2024), Valletta, Malta, 2024, pp. 265–272. URL: https: //cea.hal.science/cea-04688217. [37] A. Ignatiev, N. Narodytska, J. Marques-Silva, On validating, repairing and refining heuristic ml explanations, arXiv preprint arXiv:1907.02509 (2019). [38] A. Ignatiev, N. Narodytska, J. Marques-Silva, Abduction-based explanations for machine learning models, in: Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, 2019, pp. 1511–1519. [39] E. Dijkstra, A discipline of programming, Prentice-Hall series in automatic computation, Prentice
Hall, 1976. [40] O. Russakovsky, J. Deng, H. Su, J. Krause, S. Satheesh, S. Ma, Z. Huang, A. Karpathy, A. Khosla, M. Bernstein, A. C. Berg, L. Fei-Fei, ImageNet Large Scale Visual Recognition Challenge, International Journal of Computer Vision (IJCV) 115 (2015) 211–252. doi:10.1007/ s11263-015-0816-y. [41] C. Wah, S. Branson, P. Welinder, P. Perona, S. Belongie, The caltech-ucsd birds-200-2011 dataset (2011). [42] European Commission. Shaping Europe’s digital future, AI Act, ???? URL: https://digital-strategy. Proof. Assume the explanation ℰ is verified, meaning Verify(ℰ ) holds. By Definition 5, this implies that for all classes ̸= , the condition ℰ (, ) holds. By Definition 4, this means: ∀ ̸= : ℎ(a*ℰ (, )) ≥ ℎ (a*ℰ (, )) (1) where a*ℰ (, ) = argmaxs′∈ℰ (ℎ(s′) − ℎ (s′)).
We want to show that ℰ satisfies Definition 1. This requires showing that for any latent representation z (corresponding to a similarity vector s) such that its components satisfy the constraints imposed by ℰ (i.e., s ∈ ℰ ), the classification is . That is, we need to show:
∀s ∈ ℰ : (z) = Since (z) = argmax′ ℎ′ (s), this is equivalent to showing: ∀s ∈ ℰ , ∀ ̸= : ℎ(s) ≥ ℎ (s)
Let s be an arbitrary similarity vector in the constrained space ℰ . Let ̸= be an arbitrary alternative class.
By the definition of a*ℰ (, ) as the maximizer of (ℎ − ℎ ) within ℰ , we know that for our chosen s ∈ ℰ :
ℎ(a*ℰ (, )) − ℎ (a*ℰ (, )) ≥ ℎ (s) − ℎ (s) From our initial assumption that ℰ is verified, we know from (1) that:
ℎ(a*ℰ (, )) ≥ ℎ (a*ℰ (, )) 0 ≥ ℎ (a*ℰ (, )) − ℎ (a*ℰ (, )) 0 ≥ ℎ (a*ℰ (, )) − ℎ (a*ℰ (, )) ≥ ℎ (s) − ℎ (s) 0 ≥ ℎ (s) − ℎ (s)
ℎ(s) ≥ ℎ (s)
Since s ∈ ℰ was arbitrary and ̸= was arbitrary, we have shown that ℎ(s) ≥ ℎ (s) for all s ∈ ℰ and for all ̸= . Therefore, for any s ∈ ℰ , = argmax′ ℎ′ (s), which means (z) = .
This fulfills the condition required by Definition 1. Thus, if ℰ is verified via Total Prediction Domination within ℰ , it is a suficient abductive explanation.