# Formal Methods with a Touch of Magic

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 May 2020.

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

- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [Shielding Atari Games with Bounded Prescience](https://mlsanity.com/paper/2101.08153/) (2021)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report)](https://mlsanity.com/paper/2112.09655/) (2021)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [Composing Reinforcement Learning Policies, with Formal Guarantees](https://mlsanity.com/paper/2402.13785/) (2024)
- [Interactive Explanations for Reinforcement-Learning Agents](https://mlsanity.com/paper/2504.05393/) (2025)
- [ASQ-IT: Interactive Explanations for Reinforcement-Learning Agents](https://mlsanity.com/paper/2301.09941/) (2023)
- [Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees](https://mlsanity.com/paper/2303.12558/) (2023)

## Abstract (arXiv)

Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the em wizard, we extract from it a decision-tree based model, which we refer to as the em magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, combining a magic book in a synthesis procedure. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training.