A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers
It addresses the problem of verifying safety for dynamical systems controlled by deep neural networks over multiple time steps, which is important for safety-critical applications.
This work presents a reachability method that combines system dynamics bounding and neural network verification tools to over-approximate reachable states, providing guarantees that a dynamical system with a deep neural network controller will not enter unsafe states. The method is demonstrated on the mountain car and aircraft collision avoidance problems, showing it can provide guarantees given a bounded dynamic model.
Deep neural networks can be trained to be efficient and effective controllers for dynamical systems; however, the mechanics of deep neural networks are complex and difficult to guarantee. This work presents a general approach for providing guarantees for deep neural network controllers over multiple time steps using a combination of reachability methods and open source neural network verification tools. By bounding the system dynamics and neural network outputs, the set of reachable states can be over-approximated to provide a guarantee that the system will never reach states outside the set. The method is demonstrated on the mountain car problem as well as an aircraft collision avoidance problem. Results show that this approach can provide neural network guarantees given a bounded dynamic model.