# Formally Explaining Neural Networks within Reactive Systems

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Builds on 63 of its 113 references that are in the map.
- First posted on arXiv 31 Jul 2023.

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

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [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)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [One pixel attack for fooling deep neural networks](https://mlsanity.com/paper/1710.08864/) (2017)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [Deep Reinforcement Learning: An Overview](https://mlsanity.com/paper/1701.07274/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Metrics for Explainable AI: Challenges and Prospects](https://mlsanity.com/paper/1812.04608/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Explainable Reinforcement Learning Through a Causal Lens](https://mlsanity.com/paper/1905.10958/) (2019)
- [Applications of Deep Reinforcement Learning in Communications and Networking: A Survey](https://mlsanity.com/paper/1810.07862/) (2018)
- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [Explainable Reinforcement Learning: A Survey](https://mlsanity.com/paper/2005.06247/) (2020)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [Survey of Deep Reinforcement Learning for Motion Planning of Autonomous Vehicles](https://mlsanity.com/paper/2001.11231/) (2020)
- [Virtual-to-real Deep Reinforcement Learning: Continuous Control of Mobile Robots for Mapless Navigation](https://mlsanity.com/paper/1703.00420/) (2017)
- [Explainability in Deep Reinforcement Learning](https://mlsanity.com/paper/2008.06693/) (2020)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Model Interpretability through the Lens of Computational Complexity](https://mlsanity.com/paper/2010.12265/) (2020)
- [Introduction to Neural Network Verification](https://mlsanity.com/paper/2109.10317/) (2021)
- [Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay](https://mlsanity.com/paper/2008.05803/) (2020)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [On Guaranteed Optimal Robust Explanations for NLP Models](https://mlsanity.com/paper/2105.03640/) (2021)
- [On Explaining Decision Trees](https://mlsanity.com/paper/2010.11034/) (2020)

## Built on by (most cited first, 24 of 24)

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Local vs. Global Interpretability: A Computational Complexity Perspective](https://mlsanity.com/paper/2406.02981/) (2024)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations](https://mlsanity.com/paper/2506.08505/) (2025)
- [Shield Synthesis for LTL Modulo Theories](https://mlsanity.com/paper/2406.04184/) (2024)
- [Explain Yourself, Briefly! Self-Explaining Neural Networks with Concise Sufficient Reasons](https://mlsanity.com/paper/2502.03391/) (2025)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [SHAP Meets Tensor Networks: Provably Tractable Explanations with Parallelism](https://mlsanity.com/paper/2510.21599/) (2025)
- [Analyzing Adversarial Inputs in Deep Reinforcement Learning](https://mlsanity.com/paper/2402.05284/) (2024)
- [Self-Explaining Neural Networks for Business Process Monitoring](https://mlsanity.com/paper/2503.18067/) (2025)
- [Towards Formal Verification of Deep Neural Networks for Object Detection](https://mlsanity.com/paper/2407.01295/) (2024)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Additive Models Explained: A Computational Complexity Approach](https://mlsanity.com/paper/2510.21292/) (2025)
- [FAME: Formal Abstract Minimal Explanation for Neural Networks](https://mlsanity.com/paper/2603.10661/) (2026)
- [Unifying Formal Explanations: A Complexity-Theoretic Perspective](https://mlsanity.com/paper/2602.18160/) (2026)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Aquatic Navigation: A Challenging Benchmark for Deep Reinforcement Learning](https://mlsanity.com/paper/2405.20534/) (2024)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [Concept-Based Abductive and Contrastive Explanations for Behaviors of Vision Models](https://mlsanity.com/paper/2605.06640/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)

## Abstract (arXiv)

Deep neural networks (DNNs) are increasingly being used as controllers in reactive systems. However, DNNs are highly opaque, which renders it difficult to explain and justify their actions. To mitigate this issue, there has been a surge of interest in explainable AI (XAI) techniques, capable of pinpointing the input features that caused the DNN to act as it did. Existing XAI techniques typically face two limitations: (i) they are heuristic, and do not provide formal guarantees that the explanations are correct; and (ii) they often apply to ``one-shot'' systems, where the DNN is invoked independently of past invocations, as opposed to reactive systems. Here, we begin bridging this gap, and propose a formal DNN-verification-based XAI technique for reasoning about multi-step, reactive systems. We suggest methods for efficiently calculating succinct explanations, by exploiting the system's transition constraints in order to curtail the search space explored by the underlying verifier. We evaluate our approach on two popular benchmarks from the domain of automated navigation; and observe that our methods allow the efficient computation of minimal and minimum explanations, significantly outperforming the state of the art. We also demonstrate that our methods produce formal explanations that are more reliable than competing, non-verification-based XAI techniques.