Formal Verification of Neural Network Controllers for Collision-Free Flight
D. Genin, I. Papusha, J. Brulé, T. Young, G. Mullins, Y. Kouskoulas, R. Wu, and A. Schmidt
Abstract
We investigate a method for formally verifying the absence of adversarial examples in a neural network controller. Our approach applies to networks with piecewise affine activation units, which may be encoded symbolically as a piecewise affine mapping from inputs to outputs. The approach rests on characterizing and bounding a critical subset of the state space where controller action is required, partitioning this critical subset, and using satisfiability modulo theories (SMT) to prove nonexistence of safety counterexamples on each of the resulting partition elements. We demonstrate this approach on a simple collision avoidance neural network controller, trained with reinforcement learning to avoid collisions in a simplified simulated environment. After encoding the network weights in SMT, we formally verify safety of the neural network controller on a subset of the critical partition elements, and determine that the rest of the critical set partition elements are potentially unsafe. We further experimentally confirm the existence of actual adversarial collision scenarios in 90% of the identified potentially unsafe critical partition elements, indicating that our approach is reasonably tight.
Citation
D. Genin I. Papusha, J. Brulé, T. Young, G. Mullins, Y. Kouskoulas, R. Wu, and A. Schmidt. “Formal Verification of Neural Network Controllers for Collision-Free Flight,” Workshop on Numerical Software Verification, part of International Conference on Computer-Aided Verification (CAV), Los Angeles, CA, July 18–19, 2021.