# Verification of Image-based Neural Network Controllers Using Generative Models

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

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 40 references that are in the map.
- First posted on arXiv 14 May 2021.

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

- [A Style-Based Generator Architecture for Generative Adversarial Networks](https://mlsanity.com/paper/1812.04948/) (2018)
- [Unsupervised Representation Learning with Deep Convolutional Generative Adversarial Networks](https://mlsanity.com/paper/1511.06434/) (2015)
- [Spectral Normalization for Generative Adversarial Networks](https://mlsanity.com/paper/1802.05957/) (2018)
- [Context Encoders: Feature Learning by Inpainting](https://mlsanity.com/paper/1604.07379/) (2016)
- [Improved Precision and Recall Metric for Assessing Generative Models](https://mlsanity.com/paper/1904.06991/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Generative Adversarial Networks: An Overview](https://mlsanity.com/paper/1710.07035/) (2017)
- [Adversarial Attacks and Defences: A Survey](https://mlsanity.com/paper/1810.00069/) (2018)
- [GAN-based Synthetic Medical Image Augmentation for increased CNN Performance in Liver Lesion Classification](https://mlsanity.com/paper/1803.01229/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Neural Photo Editing with Introspective Adversarial Networks](https://mlsanity.com/paper/1609.07093/) (2016)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Global Optimization of Objective Functions Represented by ReLU Networks](https://mlsanity.com/paper/2010.03258/) (2020)
- [Validation of Image-Based Neural Network Controllers through Adaptive Stress Testing](https://mlsanity.com/paper/2003.02381/) (2020)
- [Robustness Certification of Generative Models](https://mlsanity.com/paper/2004.14756/) (2020)
- [Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems](https://mlsanity.com/paper/1802.03557/) (2018)
- [Correctness Verification of Neural Networks](https://mlsanity.com/paper/1906.01030/) (2019)
- [Manifold for Machine Learning Assurance](https://mlsanity.com/paper/2002.03147/) (2020)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study](https://mlsanity.com/paper/2302.04634/) (2023)
- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [How Generalizable Is My Behavior Cloning Policy? A Statistical Approach to Trustworthy Performance Evaluation](https://mlsanity.com/paper/2405.05439/) (2024)
- [Four Principles for Physically Interpretable World Models](https://mlsanity.com/paper/2503.02143/) (2025)
- [How Safe Am I Given What I See? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2308.12252/) (2023)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Zero-shot Safety Prediction for Autonomous Robots with Foundation World Models](https://mlsanity.com/paper/2404.00462/) (2024)
- [Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2211.02736/) (2022)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Risk-Driven Design of Perception Systems](https://mlsanity.com/paper/2205.10677/) (2022)
- [Detecting and Mitigating System-Level Anomalies of Vision-Based Controllers](https://mlsanity.com/paper/2309.13475/) (2023)
- [System Safety Monitoring of Learned Components Using Temporal Metric Forecasting](https://mlsanity.com/paper/2405.13254/) (2024)
- [Physically Interpretable World Models via Weakly Supervised Representation Learning](https://mlsanity.com/paper/2412.12870/) (2024)
- [Scenario-based Compositional Verification of Autonomous Systems with Neural Perception](https://mlsanity.com/paper/2504.20942/) (2025)
- [ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs](https://mlsanity.com/paper/2106.05325/) (2021)
- [Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles](https://mlsanity.com/paper/2501.14009/) (2025)
- [Assumption Generation for the Verification of Learning-Enabled Autonomous Systems](https://mlsanity.com/paper/2305.18372/) (2023)
- [Pre-Trained Vision Models as Perception Backbones for Safety Filters in Autonomous Driving](https://mlsanity.com/paper/2410.22585/) (2024)
- [How Safe Will I Be Given What I Saw? Calibrated Prediction of Safety Chances for Image-Controlled Autonomy](https://mlsanity.com/paper/2508.09346/) (2025)
- [Certifying Safety in Reinforcement Learning under Adversarial Perturbation Attacks](https://mlsanity.com/paper/2212.14115/) (2022)
- [From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications](https://mlsanity.com/paper/2603.05604/) (2026)
- [Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement](https://mlsanity.com/paper/2605.14294/) (2026)
- [Perron--Frobenius Operator Matching for Generative Modeling](https://mlsanity.com/paper/2606.17465/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

Neural networks are often used to process information from image-based sensors to produce control actions. While they are effective for this task, the complex nature of neural networks makes their output difficult to verify and predict, limiting their use in safety-critical systems. For this reason, recent work has focused on combining techniques in formal methods and reachability analysis to obtain guarantees on the closed-loop performance of neural network controllers. However, these techniques do not scale to the high-dimensional and complicated input space of image-based neural network controllers. In this work, we propose a method to address these challenges by training a generative adversarial network (GAN) to map states to plausible input images. By concatenating the generator network with the control network, we obtain a network with a low-dimensional input space. This insight allows us to use existing closed-loop verification tools to obtain formal guarantees on the performance of image-based controllers. We apply our approach to provide safety guarantees for an image-based neural network controller for an autonomous aircraft taxi problem. We guarantee that the controller will keep the aircraft on the runway and guide the aircraft towards the center of the runway. The guarantees we provide are with respect to the set of input images modeled by our generator network, so we provide a recall metric to evaluate how well the generator captures the space of plausible images.