# Formal Verification of Stochastic Systems with ReLU Neural Network Controllers

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 22 references that are in the map.
- First posted on arXiv 8 Mar 2021.

## Builds on (most cited first, 14 of 14)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Certified Adversarial Robustness with Additive Noise](https://mlsanity.com/paper/1809.03113/) (2018)
- [Socially Aware Motion Planning with Deep Reinforcement Learning](https://mlsanity.com/paper/1703.08862/) (2017)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Learning from Untrusted Data](https://mlsanity.com/paper/1611.02315/) (2016)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Variational End-to-End Navigation and Localization](https://mlsanity.com/paper/1811.10119/) (2018)
- [Verification for Machine Learning, Autonomy, and Neural Networks Survey](https://mlsanity.com/paper/1810.01989/) (2018)
- [Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller](https://mlsanity.com/paper/1910.11309/) (2019)
- [Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming](https://mlsanity.com/paper/1910.04249/) (2019)
- [Statistical Verification of Hyperproperties for Cyber-Physical System](https://mlsanity.com/paper/1906.07253/) (2019)
- [Specification-Guided Verification and Abstraction Refinement of Mixed Monotone Stochastic Systems](https://mlsanity.com/paper/1903.02191/) (2019)

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

- [Certifying Robustness of Learning-Based Keypoint Detection and Pose Estimation Methods](https://mlsanity.com/paper/2408.00117/) (2024)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)

## Abstract (arXiv)

In this work, we address the problem of formal safety verification for stochastic cyber-physical systems (CPS) equipped with ReLU neural network (NN) controllers. Our goal is to find the set of initial states from where, with a predetermined confidence, the system will not reach an unsafe configuration within a specified time horizon. Specifically, we consider discrete-time LTI systems with Gaussian noise, which we abstract by a suitable graph. Then, we formulate a Satisfiability Modulo Convex (SMC) problem to estimate upper bounds on the transition probabilities between nodes in the graph. Using this abstraction, we propose a method to compute tight bounds on the safety probabilities of nodes in this graph, despite possible over-approximations of the transition probabilities between these nodes. Additionally, using the proposed SMC formula, we devise a heuristic method to refine the abstraction of the system in order to further improve the estimated safety bounds. Finally, we corroborate the efficacy of the proposed method with simulation results considering a robot navigation example and comparison against a state-of-the-art verification scheme.