Verification of Image-Based Neural Network Controllers Using Generative Models

Abstract

Although neural networks are effective tools for processing information from image-based sensors to produce control actions, their complex nature limits 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. This work proposes a method to address these challenges by training a generative adversarial network to map states to plausible input images. Concatenating the generator network with the control network results in a network with a low-dimensional input space, which allows for the use of existing closed-loop verification tools to obtain formal guarantees on the performance of image-based controllers. This approach is applied to provide safety guarantees for an image-based neural network controller for an autonomous aircraft taxi problem. The resulting guarantees are with respect to the set of input images modeled by the generator network, and so a recall metric is provided to evaluate how well the generator captures the space of plausible images.