# Towards Verified and Targeted Explanations through Formal Methods

arXiv: https://arxiv.org/abs/2604.14209 · HTML: https://mlsanity.com/paper/2604.14209/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 47 of its 71 references that are in the map.
- First posted on arXiv 5 Apr 2026.

## Builds on (most cited first, 30 of 47)

- [Grad-CAM: Visual Explanations from Deep Networks via Gradient-based Localization](https://mlsanity.com/paper/1610.02391/) (2016)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- ["Why Should I Trust You?": Explaining the Predictions of Any Classifier](https://mlsanity.com/paper/1602.04938/) (2016)
- [Axiomatic Attribution for Deep Networks](https://mlsanity.com/paper/1703.01365/) (2017)
- [Deep Inside Convolutional Networks: Visualising Image Classification Models and Saliency Maps](https://mlsanity.com/paper/1312.6034/) (2013)
- [Visualizing and Understanding Convolutional Networks](https://mlsanity.com/paper/1311.2901/) (2013)
- [Learning Important Features Through Propagating Activation Differences](https://mlsanity.com/paper/1704.02685/) (2017)
- [Explanation in Artificial Intelligence: Insights from the Social Sciences](https://mlsanity.com/paper/1706.07269/) (2017)
- [Striving for Simplicity: The All Convolutional Net](https://mlsanity.com/paper/1412.6806/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Interpretation of Neural Networks is Fragile](https://mlsanity.com/paper/1710.10547/) (2017)
- [Methods for Interpreting and Understanding Deep Neural Networks](https://mlsanity.com/paper/1706.07979/) (2017)
- [Not Just a Black Box: Learning Important Features Through Propagating Activation Differences](https://mlsanity.com/paper/1605.01713/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithmic Recourse: from Counterfactual Explanations to Interventions](https://mlsanity.com/paper/2002.06278/) (2020)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [On The Reasons Behind Decisions](https://mlsanity.com/paper/2002.09284/) (2020)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [On Generating Plausible Counterfactual and Semi-Factual Explanations for Deep Learning](https://mlsanity.com/paper/2009.06399/) (2020)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [SAT-Based Rigorous Explanations for Decision Lists](https://mlsanity.com/paper/2105.06782/) (2021)
- [Formalising the Robustness of Counterfactual Explanations for Neural Networks](https://mlsanity.com/paper/2208.14878/) (2022)

## Abstract (arXiv)

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.