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

TL;DR

This work tackles safety verification for image-based NNCS by replacing the real perception with a cGAN-based surrogate and addressing two primary sources of overapproximation: one-step and multi-step errors. The authors propose two complementary improvements—composition of the discrete-time dynamics with the surrogate network to preserve state-output dependencies, and unrolling multiple control steps into a single verification target—to enable more accurate and scalable reachability analysis. Through two case studies, autonomous aircraft taxiing and advanced emergency braking, the approach substantially reduces overapproximation (e.g., a 175% reduction in the taxiing case) and enables verification where prior baselines fail, even with higher-dimensional perception outputs and modern architectures. The results demonstrate practical gains in safety certification for image-based NNCS while also highlighting remaining scalability challenges related to network size and higher-resolution perceptual inputs.

Abstract

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.

Figures (10)

• Figure 1: Simplified architecture of an image-based neural network control system and its surrogate system.
• Figure 2: Computation flowcharts for the baseline (first row), $1$-step (second row), and $2$-step (third row) methods.
• Figure 3: Illustrations of reachable sets using three different methods. In this illustrative example, assume the initial exact reachable set $R_0$ only contains one cell $c$, $R_0 = \mathcal{C}_0 = \{c\}$.
• Figure 4: Reachable sets computed using baseline (first row), $1$-step (second row), and $2$-step (third row) methods in the taxiing system. The initial set only contains one cell.
• Figure 5: Reachable sets over time using three different methods when starting from $p\in[-\qty{10}{\meter}, \qty{10}{\meter}]$ and $\theta\in[-\qty{10}{\degree}, \qty{10}{\degree}]$ in taxiing system. The colors black, teal, blue, and brown represent simulations, baseline, $1$-step, and $2$-step methods, respectively.

Theorems & Definitions (4)

• Definition 1: System Model
• Definition 2: System Evolution
• Definition 3: Reachable Set
• Definition 4: Surrogate System Model