# Formal Verification of Neural Network Controlled Autonomous Systems

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

## Key facts

- Cited by 41 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Oct 2018.

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

- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Scalable Verification of GNN-based Job Schedulers](https://mlsanity.com/paper/2203.03153/) (2022)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Verification-Aided Deep Ensemble Selection](https://mlsanity.com/paper/2202.03898/) (2022)
- [Towards Sparsification of Graph Neural Networks](https://mlsanity.com/paper/2209.04766/) (2022)
- [Minimal Multi-Layer Modifications of Deep Neural Networks](https://mlsanity.com/paper/2110.09929/) (2021)
- [Verification-Guided Shielding for Deep Reinforcement Learning](https://mlsanity.com/paper/2406.06507/) (2024)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Certification of Iterative Predictions in Bayesian Neural Networks](https://mlsanity.com/paper/2105.10134/) (2021)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Neuro-Symbolic AI for Military Applications](https://mlsanity.com/paper/2408.09224/) (2024)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [Provably Correct Training of Neural Network Controllers Using Reachability Analysis](https://mlsanity.com/paper/2102.10806/) (2021)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)
- [Probabilistic Reach-Avoid for Bayesian Neural Networks](https://mlsanity.com/paper/2310.01951/) (2023)
- [Certifying Robustness of Learning-Based Keypoint Detection and Pose Estimation Methods](https://mlsanity.com/paper/2408.00117/) (2024)
- [Local Repair of Neural Networks Using Optimization](https://mlsanity.com/paper/2109.14041/) (2021)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [Formal Verification of Stochastic Systems with ReLU Neural Network Controllers](https://mlsanity.com/paper/2103.05142/) (2021)
- [Verifying the Generalization of Deep Learning to Out-of-Distribution Domains](https://mlsanity.com/paper/2406.02024/) (2024)
- [EnergyShield: Provably-Safe Offloading of Neural Network Controllers for Energy Efficiency](https://mlsanity.com/paper/2302.06572/) (2023)
- [ECLipsE-Gen-Local: Efficient Compositional Local Lipschitz Estimates for Deep Neural Networks](https://mlsanity.com/paper/2510.05261/) (2025)

## Abstract (arXiv)

In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial conditions such that a robot trajectory starting from these initial conditions is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of the safe initial states. The first technical problem in computing the finite state abstraction is to mathematically model the imaging function that maps the robot position to the LiDAR image. To that end, we introduce the notion of imaging-adapted sets as partitions of the workspace in which the imaging function is guaranteed to be affine. We develop a polynomial-time algorithm to partition the workspace into imaging-adapted sets along with computing the corresponding affine imaging functions. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) nonlinearity, the second technical challenge is to analyze the behavior of the neural network. To that end, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible segments of different ReLUs. SMC solvers then use a Boolean satisfiability solver and a convex programming solver and decompose the problem into smaller subproblems. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space feasible ReLU segments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with increasing complexity of the neural network controller.