# An Inductive Synthesis Framework for Verifiable Reinforcement Learning

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

## Key facts

- Cited by 39 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jul 2019.

## Built on by (most cited first, 30 of 39)

- [A Review of Safe Reinforcement Learning: Methods, Theory and Applications](https://mlsanity.com/paper/2205.10330/) (2022)
- [A Survey on Interpretable Reinforcement Learning](https://mlsanity.com/paper/2112.13112/) (2021)
- [Learning to Synthesize Programs as Interpretable and Generalizable Policies](https://mlsanity.com/paper/2108.13643/) (2021)
- [Interpretable and Explainable Logical Policies via Neurally Guided Symbolic Abstraction](https://mlsanity.com/paper/2306.01439/) (2023)
- [Provable Repair of Deep Neural Networks](https://mlsanity.com/paper/2104.04413/) (2021)
- [A Survey on AI Assurance](https://mlsanity.com/paper/2111.07505/) (2021)
- [GALOIS: Boosting Deep Reinforcement Learning via Generalizable Logic Synthesis](https://mlsanity.com/paper/2205.13728/) (2022)
- [Dynamic Model Predictive Shielding for Provably Safe Reinforcement Learning](https://mlsanity.com/paper/2405.13863/) (2024)
- [Synthesizing Programmatic Reinforcement Learning Policies with Large Language Model Guided Search](https://mlsanity.com/paper/2405.16450/) (2024)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [SyReNN: A Tool for Analyzing Deep Neural Networks](https://mlsanity.com/paper/2101.03263/) (2021)
- [Programmatic Reward Design by Example](https://mlsanity.com/paper/2112.08438/) (2021)
- [A Hierarchical Bayesian Approach to Inverse Reinforcement Learning with Symbolic Reward Machines](https://mlsanity.com/paper/2204.09772/) (2022)
- [SEVerA: Verified Synthesis of Self-Evolving Agents](https://mlsanity.com/paper/2603.25111/) (2026)
- [On the Safety of Interpretable Machine Learning: A Maximum Deviation Approach](https://mlsanity.com/paper/2211.01498/) (2022)
- [Verified Probabilistic Policies for Deep Reinforcement Learning](https://mlsanity.com/paper/2201.03698/) (2022)
- [Model-free Neural Lyapunov Control for Safe Robot Navigation](https://mlsanity.com/paper/2203.01190/) (2022)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (2024)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [EXPIL: Explanatory Predicate Invention for Learning in Games](https://mlsanity.com/paper/2406.06107/) (2024)
- [Self-Correcting Neural Networks For Safe Classification](https://mlsanity.com/paper/2107.11445/) (2021)
- [Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning](https://mlsanity.com/paper/2106.06931/) (2021)
- [Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking](https://mlsanity.com/paper/2109.06523/) (2021)
- [Guiding Safe Exploration with Weakest Preconditions](https://mlsanity.com/paper/2209.14148/) (2022)
- [A Survey on Explainable Reinforcement Learning: Concepts, Algorithms, Challenges](https://mlsanity.com/paper/2211.06665/) (2022)
- [Inductive Generalization in Reinforcement Learning from Specifications](https://mlsanity.com/paper/2406.03651/) (2024)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [Toward Neural-Network-Guided Program Synthesis and Verification](https://mlsanity.com/paper/2103.09414/) (2021)

## Abstract (arXiv)

Despite the tremendous advances that have been made in the last decade on developing useful machine-learning applications, their wider adoption has been hindered by the lack of strong assurance guarantees that can be made about their behavior. In this paper, we consider how formal verification techniques developed for traditional software systems can be repurposed for verification of reinforcement learning-enabled ones, a particularly important class of machine learning systems. Rather than enforcing safety by examining and altering the structure of a complex neural network implementation, our technique uses blackbox methods to synthesizes deterministic programs, simpler, more interpretable, approximations of the network that can nonetheless guarantee desired safety properties are preserved, even when the network is deployed in unanticipated or previously unobserved environments. Our methodology frames the problem of neural network verification in terms of a counterexample and syntax-guided inductive synthesis procedure over these programs. The synthesis procedure searches for both a deterministic program and an inductive invariant over an infinite state transition system that represents a specification of an application's control logic. Additional specifications defining environment-based constraints can also be provided to further refine the search space. Synthesized programs deployed in conjunction with a neural network implementation dynamically enforce safety conditions by monitoring and preventing potentially unsafe actions proposed by neural policies. Experimental results over a wide range of cyber-physical applications demonstrate that software-inspired formal verification techniques can be used to realize trustworthy reinforcement learning systems with low overhead.