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.

翻译：验证以图像作为输入的神经网络控制系统的安全性是一个难题，因为对于给定的系统状态，目前尚无已知方法能在数学上建模现实世界中可能出现的图像。我们基于近期一项采用代理验证方法的研究，训练一个条件生成对抗网络（cGAN）作为图像生成器以替代真实世界。这使得对闭环系统进行基于集合的形式化分析成为可能，提供了超越仿真与测试的分析能力。虽然现有方法在小规模示例中有效，但在单个控制周期内及跨多个控制周期内的过度过近似限制了其可扩展性。我们提出了克服这两类误差来源的方法。首先，我们通过组合系统动力学、cGAN及神经网络控制器来克服单步误差，同时避免如系统动力学单调性分析中那样丢失输入状态与控制输出间的依赖关系。其次，我们通过重复单步组合来减少多步误差，本质上将控制循环的多个步骤展开为一个大型神经网络。随后，我们利用现有网络验证工具计算多步的精确可达集，避免每一步抽象误差的累积。我们通过两个案例研究（自主飞机滑行系统与高级紧急制动系统）验证了所提方法在精度与可扩展性方面的有效性。在飞机滑行系统中，使用先前基线方法得到的收敛可达集比我们提出的方法大175%。在紧急制动系统中，当cGAN输出的图像变量数量增加24倍时，基线方法无法证明任何状态是安全的，而我们的改进方法能够实现基于集合的安全性分析。