Towards Verified and Targeted Explanations through Formal Methods

Hanchen David Wang; Diego Manzanas Lopez; Preston K. Robinette; Ipek Oguz; Taylor T. Johnson; Meiyi Ma

cs.LGApr 5, 2026

Towards Verified and Targeted Explanations through Formal Methods

Authors: Hanchen David Wang, Diego Manzanas Lopez, Preston K. Robinette, Ipek Oguz, Taylor T. Johnson, Meiyi Ma

Organizations: Vanderbilt University, Nashville, Tennessee, USA

Abstract

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 $\mathbf{t}$ of ‘2’, a perturbation $\epsilon$ , and a norm $p$ . Using a heuristic ranking, ViTaX identifies a subset of input pixels to be $\epsilon$ -perturbed, generating a subset of important input features.

Panel of Figure 3 — 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.

Panel of Figure 4 — Algorithm 1 ViTaX (Reachability eXplanation)

Heuristic/Probabilistic Methods
	MNIST (MLP)				GTSRB (CNN)
Method	Fid. $\uparrow$	Rob. (NE) $\uparrow$	Time (s) $\downarrow$	Card. $\downarrow$	Fid. $\uparrow$	Rob. (NE) $\uparrow$	Time (s) $\downarrow$	Card. $\downarrow$
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.

\uparrow

indicates higher is better;

\downarrow

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 $\epsilon$ 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. $\uparrow$		Rob. (NE) $\uparrow$		Time (s) $\downarrow$		Card. $\downarrow$
			$\epsilon\approx 0.10$	$\epsilon\approx 0.22$	$\epsilon\approx 0.10$	$\epsilon\approx 0.22$	$\epsilon\approx 0.10$	$\epsilon\approx 0.22$	$\epsilon\approx 0.10$	$\epsilon\approx 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,

\epsilon\approx 0.10

(25/255) and

\epsilon\approx 0.22

(55/255), using the CP-Star Verification Backend. (Averages over 10 samples).

Panel of Figure 5 — 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.

Panel of Figure 6 — 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.

Panel of Figure 7 — 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.

Panel of Figure 8 — Figure 8. EMNIST Targeted Explanations. ViTaX identifies the semifactual explanation relevant to specific character transitions.

Panel of Figure 9 — Figure 9. ViTaX ’s targeted explanation for transitioning MNIST ‘3’ (original) towards ‘8’ (target) at different perturbation magnitudes $\epsilon$ . As $\epsilon$ increases, the minimal set $A$ satisfying Targeted $\epsilon$ -Robustness tends to become smaller and more focused.

Panel of Figure 10 — 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) $\downarrow$	Card. $\downarrow$	Fidelity $\uparrow$	Rob. (NE) $\uparrow$
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

Panel of Figure 11 — 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.

Panel of Figure 12 — 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.

Panel of Figure 13 — Figure 13. An example of potentially not robust to other classes $k$ in projected range of logits. Green box is label $\mathbf{y}$ , red box is target $\mathbf{t}$ , and yellow box is other classes $\mathbf{k}$ . In this case, we are arguing, given our Equation 1 and 2 , there are potentially cases in (c) and (d). The yellow box $\mathbf{k}$ could cross the boundary while the subset of feature is robust to $\mathbf{t}$ .

Panel of Figure 14 — Figure 14. GTSRB Explanation on 50 to Speed Limit 80 End

Panel of Figure 15 — 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) .

Panel of Figure 16 — 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 $\mathbf{t}$
Class $\mathbf{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

\epsilon

-perturbation. The columns represent the original sample classes

\mathbf{y}

, while the rows indicate the target explanation classes

\mathbf{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.

Table 23

Table 24

Table 25

Type	Parameters	Activation
Input	$h\times w\times c$	-
Convolution	$3\times 3\times 4$	ReLU
Convolution	$3\times 3\times 4$	ReLU
Flatten	-	-
Fully Connected	20	ReLU
Fully Connected	# classes	softmax

Appendix

Table 12. Structure of the CNN Dense

Explainable Artificial Intelligence

Explainable artificial intelligence develops ways to make AI decisions understandable, testable, and useful to people.

See all 326 papers

Evaluating Explainability in Safety-Critical ATR Systems: Limitations of Post-Hoc Methods and Paths Toward Robust XAI
May 7, 2026Vanessa Buhrmester, David Muench, Dimitri Bulatov +1Explainable Artificial Intelligence Explanation Stability
IOSB, Ettlingen, Germany
Learning Quantifiable Visual Explanations Without Ground-Truth
May 18, 2026Amritpal Singh, Andrey Barsky, Mohamed Ali Souibgui +2Perturbation-Based Feature Attribution Causal Interpretability
Computer Vision Center, Barcelona, Spain · Autonomous University of Barcelona, Spain
FAME: Formal Abstract Minimal Explanation for Neural Networks
Mar 11, 2026Ryma Boumazouza, Raya Elsaleh, Melanie Ducoffe +2Abstract Interpretation Neural Network Interpretability
Airbus SAS, France · IRT Saint-Exupery, France · The Hebrew University of Jerusalem, Israel

May 7, 2026J/K move · Enter open · S save

Evaluating Explainability in Safety-Critical ATR Systems: Limitations of Post-Hoc Methods and Paths Toward Robust XAI

Vanessa Buhrmester, David Muench, Dimitri Bulatov, Michael Arens

IOSB, Ettlingen, Germany

Explainable Artificial Intelligence Explanation Stability Explainability Evaluation

Open paper AskPDF arXiv

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.

Abstract

Explainable Artificial Intelligence

Explore similar work

Evaluating Explainability in Safety-Critical ATR Systems: Limitations of Post-Hoc Methods and Paths Toward Robust XAI

Learning Quantifiable Visual Explanations Without Ground-Truth

FAME: Formal Abstract Minimal Explanation for Neural Networks