As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations that are interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features but offer no mathematical guarantees about decision boundaries, while formal methods verify robustness yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, not all misclassifications carry equal consequences; confusing a "Stop" sign for a "60 kph" sign is far more dangerous than confusing it with a "No Passing" sign. We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that generates targeted semifactual explanations with mathematical guarantees. For a given input (class y) and a user-specified critical alternative (class t), ViTaX: (1) identifies the minimal feature subset most sensitive to the y->t transition, and (2) applies formal reachability analysis to guarantee that perturbing these features by epsilon cannot flip the classification to t. We formalize this through Targeted epsilon-Robustness, certifying whether a feature subset remains robust under perturbation toward a specific target class. ViTaX is the first method to provide formally guaranteed explanations of a model's resilience against user-identified alternatives. Evaluations on MNIST, GTSRB, EMNIST, and TaxiNet demonstrate over 30% fidelity improvement with minimal explanation cardinality.
Figures & tables
Figure 1. The Necessity of Targeted Verification: Prioritizing Critical Boundaries over Nearest Boundaries. All methods use the same base model (GTSRB CNN). Formal verification is expensive and must be deployed strategically. (A) Scenario: A model correctly classifies ’Stop’ (Class 14). The decision space has asymmetric risks: Class 10 (‘No Pass’) is the nearest boundary (low risk), while Class 5 (‘60 kph’) is the critical boundary (high risk). Risk levels are defined by the application domain (e.g., traffic safety regulations) and provided by the user; ViTaX then directs verification resources toward the user-specified critical boundary. (B) HNMAS (Formal Instance-level) ( Leofante and Lomuscio, 2023 ) : Provides instance-level semifactual explanations via robustness for multi-agent systems. The analysis is constrained by local geometry, and the evaluation drifts (arrow) towards the nearest boundary (Class 10). (C) VeriX (Untargeted Formal) ( Wu et al., 2023 ) : Provides feature-level explanations of general resilience. The analysis is constrained by the nearest boundary, resulting in a broad explanation and evaluation drift (arrow) towards Class 10. (D) ViTaX (Targeted Formal): Provides feature-level explanations of targeted resilience. ViTaX focuses resources (arrow) on the critical boundary, resulting in a precise explanation and evaluation drift towards Class 5. In safety-critical deployment, understanding resilience against high-risk alternatives (Class 5, ‘60 kph’) is essential, even when other boundaries (Class 10, ‘No Pass’) are closer but less dangerous. ViTaX provides guarantees where they matter most.
Figure 2. ViTaX takes an initial input image of ‘7’, a target class t of ‘2’, a perturbation ϵ , and a norm p . Using a heuristic ranking, ViTaX identifies a subset of input pixels to be ϵ -perturbed, generating a subset of important input features.
Figure 3. Computing the explanation towards one particular class using reachability solver for a simple input x=[1,..16] . Green is the current set of features that solver is evaluating. Gray denotes the irrelevant feature and white is undetermined features.
Algorithm 1 ViTaX (Reachability eXplanation)
Figure 4. Qualitative comparison of explanations for an MNIST sample (original ‘4’, target ‘9’ for ViTaX ). All methods use the same base model (MNIST MLP). ViTaX highlights the critical feature set A . Note that this visualization shows the sensitive features (a semifactual insight), not a counterfactual instance that successfully flips the class.
MNIST (MLP)
GTSRB (CNN)
Method
Fid. ↑
Rob. (NE) ↑
Time (s) ↓
Card. ↓
Fid. ↑
Rob. (NE) ↑
Time (s) ↓
Card. ↓
Heuristic/Probabilistic Methods
LIME (Adapted)
0.09
0.93
3.42
44.27
0.32
0.60
4.65
47.11
Anchors (Adapted)
0.11
0.94
4.06
41.59
0.57
0.56
8.73
75.11
TSA
0.52
0.97
0.01
514.37
0.10
0.92
0.02
621.47
Prototype
0.15
0.93
0.00
214.44
0.33
1.00
0.00
782.59
Table 1. Comprehensive Evaluation Results. ↑ indicates higher is better; ↓ indicates lower is better. Best results among heuristic/probabilistic methods are underlined; best results among formal methods are bolded.
Method
Mechanism
Example (HELOC)
Nature of Guarantee
LIME/Anchors (Adapted)
Local Surrogate + Probabilistic Sampling. Identifies features that ensure prediction persistence with high probability.
“Maintaining the current ‘ExternalRiskEstimate’ and ‘AverageMInFile’ is sufficient to keep the ‘Good Risk’ status with 95% probability.”
Probabilistic & Empirical.
Prototype / TSA
Example-based search or iterative optimization. Finds specific instances or perturbations that do not cross the boundary.
“Even when ‘NumInqLast6M’ was increased by 2, the status remained ‘Good Risk’.”
Heuristic / Best Effort.
VeriX
Formal Verification (MILP/SMT). Finds features that guarantee the prediction regardless of other feature values (Sufficiency).
“It’s guaranteed that as long as ‘ExternalRiskEstimate’ < 65, the loan is always ‘Good Risk’.”
Deterministic & Formal (Untargeted).
ViTaX
Formal Reachability + Efficient Search. Proves perturbation of critical features (A) by ϵ is insufficient to cross the boundary towards a specific target (t).
For a ‘Good Risk’ applicant, it’s guaranteed that if you change ‘ExternalRiskEstimate’ and ‘AverageMInFile’ by up to 10% in any combination, the result will not change to ‘Bad Risk’.
Deterministic & Formal (Targeted).
Table 2. Conceptual Comparison of Semifactual Explanation Generation Methods, illustrated with HELOC dataset ( FICO Community, 2019 ) . ViTaX uniquely combines targeted insights with formal guarantees and scalability.
Model
# Params
Acc (%)
Fid. ↑
Rob. (NE) ↑
Time (s) ↓
Card. ↓
ϵ≈0.10
ϵ≈0.22
ϵ≈0.10
ϵ≈0.22
ϵ≈0.10
ϵ≈0.22
ϵ≈0.10
ϵ≈0.22
CNN
15,634
99.0
0.39
0.55
0.99
0.97
56.89
55.24
476.4
237.5
ResNet-Tiny
10,738
97.1
0.30
0.37
0.77
0.82
58.52
57.65
270.3
68.6
ResNet-Small
173,850
99.4
0.27
0.39
0.97
0.92
60.80
58.73
463.3
177.2
ResNet-Large
693,802
99.1
0.29
0.34
0.94
0.86
63.74
61.83
421.1
90.5
Inception
490,954
84.1
0.16
0.16
0.93
0.92
66.71
66.40
124.8
55.2
Table 3. ViTaX Performance on Complex Architectures (MNIST) for two perturbation budgets, ϵ≈0.10 (25/255) and ϵ≈0.22 (55/255), using the CP-Star Verification Backend. (Averages over 10 samples).
Figure 5. Scalability analysis on MLP models with varying input image sizes (MNIST 28x28, 56x56, 78x78). Runtime increases with input dimensions, with Approx-Star showing superior efficiency over CP-Star for MLP architectures.
Figure 6. Application of ViTaX to the TaxiNet regression task. Top row: original input images. Bottom row: ViTaX explanations highlighting features relevant to the predicted steering angle (values shown as Ground Truth (Model Prediction)). Green indicates positive perturbations, red indicates negative, relative to their influence on the output.
Figure 7. GTSRB Targeted Explanations. The first row shows the original “Straight” sign and various targets. The second row shows the ViTaX semifactual explanations (Feature Set A) critical for the resilience of “Straight” against each specific target.
Figure 8. EMNIST Targeted Explanations. ViTaX identifies the semifactual explanation relevant to specific character transitions.
Figure 9. ViTaX ’s targeted explanation for transitioning MNIST ‘3’ (original) towards ‘8’ (target) at different perturbation magnitudes ϵ . As ϵ increases, the minimal set A satisfying Targeted ϵ -Robustness tends to become smaller and more focused.
Figure 10. Comparison of explanation cardinality (Number of Pixels, x-axis) resulting from different heuristic ranking functions across classes (y-axis). Lower cardinality is better. Sensitivity consistently yields the most minimal explanations. (GTSRB shows the first nine classes for readability).
Solver Method
Time (s) ↓
Card. ↓
Fidelity ↑
Rob. (NE) ↑
Exact Star
30.71
129.66
0.220
0.60
Approx Star
2.04
111.46
0.218
0.59
Relax Star 50%
2.06
111.46
0.218
0.59
Relax Star 75%
2.03
109.91
0.217
0.59
Relax Star 85%
2.00
109.91
0.217
0.59
CP Star
52.18
130.28
0.211
0.59
Table 4. Comparison of Different Reachability Solver Methods within ViTaX (on a smaller MNIST model).
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 11. Empirical evaluation on input space projected into one dimensional space (in output space). As shown in both of the subfigures, it shows the empirical evaluation of Lemma 3.1 and Remark 1 , which satisfies what we claim. We evaluated on both approx star and exact star reachability method.
Figure 12. Soundness and inclusiveness visualization on a toy example. We evaluate the feature space projected into 2 dimension output space. The individual subcaptions show the vector of features perturbed.
Figure 13. An example of potentially not robust to other classes k in projected range of logits. Green box is label y , red box is target t , and yellow box is other classes k . In this case, we are arguing, given our Equation 1 and 2 , there are potentially cases in (c) and (d). The yellow box k could cross the boundary while the subset of feature is robust to t .
Figure 14. GTSRB Explanation on 50 to Speed Limit 80 End
Figure 15. X-axis represents the class from 0 to 9 and y-axis represents the mean cardinality value as percentage as shown in 15(a) and mean time in 15(b) .
Figure 16. ViTaX with different heuristic functions. For each pair, the left side shows the output of the heuristic function, and the right side shows the corresponding ViTaX explanations generated using the heuristic function’s output.
Target Class t
Class y
0
1
2
3
4
5
6
7
8
9
0
-
26.4%
21.3%
22.1%
26.8%
24.9%
21.4%
21.8%
24.5%
22.6%
1
11.0%
-
9.6%
7.6%
8.6%
8.7%
7.4%
5.8%
8.3%
8.4%
2
16.0%
13.3%
-
12.7%
18.8%
18.9%
18.0%
11.8%
17.1%
18.8%
3
17.1%
20.6%
14.6%
-
20.9%
13.3%
20.0%
19.7%
14.2%
14.5%
4
16.2%
17.7%
16.2%
17.5%
-
16.2%
14.9%
15.5%
17.0%
9.6%
Appendix
Table 5. The table presents the average percentage of cardinality, illustrating the proportion of features that significantly contribute to class transitions under ϵ -perturbation. The columns represent the original sample classes y , while the rows indicate the target explanation classes t . Notably, the ’-’ symbol denotes cases where the target class is the same as the original class, which are purposefully excluded as they do not necessitate an explanation.
Explainable Artificial Intelligence (XAI) is increasingly rec ognized as essential for deploying machine learning systems in safety critical environments. In Automatic Target Recognition (ATR), where models operate on image, video, radar, and multisensor data, high pre dictive performance alone is insufficient. Model decisions must also be interpretable, reliable, and suitable for validation. This paper presents a structured evaluation of explainability methods in the context of safety-critical ATR systems: We identify major XAI paradigms, including saliency-based, attention-based, and surrogate ap proaches, as well as recent detection-aware extensions. Based on this, we formalize explainability as an assurance-oriented assessment problem, introduce a taxonomy, and assess these methods with respect to four key dimensions: interpretability, robustness, vulnerability to manipula tion, and suitability for validation and verification. The analysis identifies systematic limitations of current post-hoc explanation methods. In par ticular, we derive critical failure modes such as spurious explanations, instability under perturbations, and overtrust induced by visually con vincing outputs. These findings indicate that widely used XAI techniques may be insufficient for safety-critical deployment. Finally, we discuss implications for ATR systems and outline directions toward more robust, causally grounded, and physically informed explain ability methods. Our results emphasize the need to move beyond visually plausible explanations toward approaches that support reliable decision making and system-level assurance.
Vanessa Buhrmester, David Muench, Dimitri Bulatov +1
Explainable AI (XAI) techniques are increasingly important for the validation and responsible use of modern deep learning models, but are difficult to evaluate due to the lack of good ground-truth to compare against. We propose a framework that serves as a quantifiable metric for the quality of XAI methods, based on continuous input perturbation. Our metric formally considers the sufficiency and necessity of the attributed information to the model's decision-making, and we illustrate a range of cases where it aligns better with human intuitions of explanation quality than do existing metrics. To exploit the properties of this metric, we also propose a novel XAI method, considering the case where we fine-tune a model using a differentiable approximation of the metric as a supervision signal. The result is an adapter module that can be trained on top of any black-box model to output causal explanations of the model's decision process, without degrading model performance. We show that the explanations generated by this method outperform those of competing XAI techniques according to a number of quantifiable metrics.
Amritpal Singh, Andrey Barsky, Mohamed Ali Souibgui +2
Computer Vision Center, Barcelona, Spain · Autonomous University of Barcelona, Spain
We propose FAME (Formal Abstract Minimal Explanations), a new class of abductive explanations grounded in abstract interpretation. FAME is the first method to scale to large neural networks while reducing explanation size. Our main contribution is the design of dedicated perturbation domains that eliminate the need for traversal order. FAME progressively shrinks these domains and leverages LiRPA-based bounds to discard irrelevant features, ultimately converging to a formal abstract minimal explanation. To assess explanation quality, we introduce a procedure that measures the worst-case distance between an abstract minimal explanation and a true minimal explanation. This procedure combines adversarial attacks with an optional VERIX+ refinement step. We benchmark FAME against VERIX+ and demonstrate consistent gains in both explanation size and runtime on medium- to large-scale neural networks.
Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe +2
Airbus SAS, France · IRT Saint-Exupery, France · The Hebrew University of Jerusalem, Israel