Towards Verified and Targeted Explanations through Formal Methods

Abstract

As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations of model behavior that are not only interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short of this requirement: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features for individual predictions but offer no mathematical guarantees about decision boundaries, while formal explanation methods verify robustness properties yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, however, 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.  Practitioners therefore lack a principled way to answer a fundamental safety question: how resilient is a model’s classification against a specific, high-risk alternative?  We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that addresses this gap by generating targeted semifactual explanations with mathematical guarantees.  For a given input (class y) and a user-specified critical alternative (class t), ViTaX performs two key steps: (1) it identifies the minimal feature subset most sensitive to the y → t transition using class-specific sensitivity heuristics, and (2) it applies formal reachability analysis to guarantee that perturbing these features by ε is insufficient to flip the classification to t. This guarantee constitutes a verified semifactual: “even if these critical features change by ε classification y persists against t." We formalize this reasoning through Targeted ε-Robustness, a formal property that certifies whether an identified feature subset remains robust under perturbation toward a specific target class. By unifying semifactual explanations, class-specific targeting, and formal verification, ViTaX is the first method to provide formally guaranteed explanations of a model’s resilience against specific, user-identified alternatives. Our evaluations on image classification (MNIST, GTSRB, EMNIST) and regression (TaxiNet) demonstrate that ViTaX achieves significantly higher fidelity (e.g., over 30% improvement) and minimal explanation cardinality compared to existing methods. These results establish ViTaX as a scalable and trustworthy foundation for verifiable, targeted XAI.