OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems

Deep learning methods can be used to produce control policies, but certifying\ntheir safety is challenging. The resulting networks are nonlinear and often\nvery large. In response to this challenge, we present OVERT: a sound algorithm\nfor safety verification of nonlinear discrete-time closed loop dynamical\nsystems with neural network control policies. The novelty of OVERT lies in\ncombining ideas from the classical formal methods literature with ideas from\nthe newer neural network verification literature. The central concept of OVERT\nis to abstract nonlinear functions with a set of optimally tight piecewise\nlinear bounds. Such piecewise linear bounds are designed for seamless\nintegration into ReLU neural network verification tools. OVERT can be used to\nprove bounded-time safety properties by either computing reachable sets or\nsolving feasibility queries directly. We demonstrate various examples of safety\nverification for several classical benchmark examples. OVERT compares favorably\nto existing methods both in computation time and in tightness of the reachable\nset.\n