A Method for Formal Verification of Neural Network Collision Avoidance Controller

No ratings

Presented at High Confidence Software and Systems Conference 2022 by

Daniel Genin

We present an approach for verifying the safety of an autonomous system controller, such as a collision avoidance controller, implemented by a neural network (NN). The described approach applies to NN controllers with piecewise affine activation units, which includes many common NN architectures. The approach relies on a combination of reachability analysis and an algorithm for identifying the critical state space regions where the controller's choice of action determines future safety. We show that by evaluating the safety of the controller on this critical set, its safety can be guaranteed for a large subset of the state space. On the critical set, the controller safety can be exhaustively checked using an SMT (Solver Modulo Theory) solver, to evaluate a conservative safety condition over a discretization partition. We demonstrate the proposed approach on a simplified 2D collision avoidance NN controller in an adversarial environment simulating vertical aircraft collision avoidance.