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

TL;DR

OVERT is a novel safety verification algorithm that combines classical formal methods with neural network verification techniques to efficiently certify safety properties of nonlinear control systems.

Contribution

It introduces a new approach that abstracts nonlinear functions with tight piecewise linear bounds for neural network safety verification.

Findings

Outperforms existing methods in computation time

Provides tighter bounds on reachable sets

Successfully verifies safety on classical benchmarks

Abstract

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