Towards Verified and Targeted Explanations through Formal Methods

TL;DR

ViTaX is a formal XAI framework that provides targeted, mathematically guaranteed explanations for neural network decisions, especially in safety-critical applications, by identifying sensitive features and certifying robustness against specific class transitions.

Contribution

It introduces ViTaX, the first method to generate formally guaranteed, targeted explanations with mathematical robustness guarantees for specific class transitions in neural networks.

Findings

Achieved over 30% fidelity improvement on multiple datasets.

Generated minimal feature subsets sensitive to class transitions.

Provided formal reachability analysis to certify robustness against targeted perturbations.

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.