# Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 35 references that are in the map.
- First posted on arXiv 28 May 2024.

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

- [CARLA: An Open Urban Driving Simulator](https://mlsanity.com/paper/1711.03938/) (2017)
- [Conditional Generative Adversarial Nets](https://mlsanity.com/paper/1411.1784/) (2014)
- [Self-Attention Generative Adversarial Networks](https://mlsanity.com/paper/1805.08318/) (2018)
- [MoCoGAN: Decomposing Motion and Content for Video Generation](https://mlsanity.com/paper/1707.04993/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Learning Hand-Eye Coordination for Robotic Grasping with Deep Learning and Large-Scale Data Collection](https://mlsanity.com/paper/1603.02199/) (2016)
- [DeepDriving: Learning Affordance for Direct Perception in Autonomous Driving](https://mlsanity.com/paper/1505.00256/) (2015)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Rebooting ACGAN: Auxiliary Classifier GANs with Stable Training](https://mlsanity.com/paper/2111.01118/) (2021)
- [Real-time Out-of-distribution Detection in Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2001.10494/) (2020)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Attacking Vision-based Perception in End-to-End Autonomous Driving Models](https://mlsanity.com/paper/1910.01907/) (2019)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Conditional GANs with Auxiliary Discriminative Classifier](https://mlsanity.com/paper/2107.10060/) (2021)
- [Reachability Analysis and Safety Verification for Neural Network Control Systems](https://mlsanity.com/paper/1805.09944/) (2018)
- [Detecting Adversarial Examples in Learning-Enabled Cyber-Physical Systems using Variational Autoencoder for Regression](https://mlsanity.com/paper/2003.10804/) (2020)
- [Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets](https://mlsanity.com/paper/2209.09321/) (2022)

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

- [Four Principles for Physically Interpretable World Models](https://mlsanity.com/paper/2503.02143/) (2025)
- [Designing Latent Safety Filters using Pre-Trained Vision Models](https://mlsanity.com/paper/2509.14758/) (2025)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [Learning Ensembles of Vision-based Safety Control Filters](https://mlsanity.com/paper/2412.02029/) (2024)
- [Deterministic World Models for Closed-loop Reachability Analysis of End-to-End Vision-based Control](https://mlsanity.com/paper/2512.08991/) (2025)
- [Pre-Trained Vision Models as Perception Backbones for Safety Filters in Autonomous Driving](https://mlsanity.com/paper/2410.22585/) (2024)
- [Learning Vision-Based Neural Network Controllers with Semi-Probabilistic Safety Guarantees](https://mlsanity.com/paper/2503.00191/) (2025)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

Verifying safety of neural network control systems that use images as input is a difficult problem because, from a given system state, there is no known way to mathematically model what images are possible in the real-world. We build on recent work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. This enables set-based formal analysis of the closed-loop system, providing analysis beyond simulation and testing. While existing work is effective on small examples, excessive overapproximation both within a single control period and across multiple control periods limits its scalability. We propose approaches to overcome these two sources of error. First, we overcome one-step error by composing the system's dynamics along with the cGAN and neural network controller, without losing the dependencies between input states and the control outputs as in the monotonic analysis of the system dynamics. Second, we reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network. We then leverage existing network verification tools to compute accurate reachable sets for multiple steps, avoiding the accumulation of abstraction error at each step. We demonstrate the effectiveness of our approach in terms of both accuracy and scalability using two case studies: an autonomous aircraft taxiing system and an advanced emergency braking system. On the aircraft taxiing system, the converged reachable set is 175% larger using the prior baseline method compared with our proposed approach. On the emergency braking system, with 24x the number of image output variables from the cGAN, the baseline method fails to prove any states are safe, whereas our improvements enable set-based safety analysis.