Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components

TL;DR

This paper introduces Reachable Polyhedral Marching (RPM), a novel algorithm for exact safety verification of neural network-based robotic systems, which efficiently computes reachable sets by incrementally enumerating polyhedral cells, enabling faster unsafe action detection.

Contribution

The paper presents RPM, a new safety verification algorithm that builds reachable sets by cell enumeration, reducing memory use and enabling anytime unsafe cell detection in neural network systems.

Findings

Faster unsafe action detection than existing methods

Certifies safety with comparable or less time

Successfully verifies safety of a neural network model of pendulum dynamics

Abstract

We present a method for computing exact reachable sets for deep neural networks with rectified linear unit (ReLU) activation. Our method is well-suited for use in rigorous safety analysis of robotic perception and control systems with deep neural network components. Our algorithm can compute both forward and backward reachable sets for a ReLU network iterated over multiple time steps, as would be found in a perception-action loop in a robotic system. Our algorithm is unique in that it builds the reachable sets by incrementally enumerating polyhedral cells in the input space, rather than iterating layer-by-layer through the network as in other methods. If an unsafe cell is found, our algorithm can return this result without completing the full reachability computation, thus giving an anytime property that accelerates safety verification. In addition, our method requires less memory during execution compared to existing methods where memory can be a limiting factor. We demonstrate our algorithm on safety verification of the ACAS Xu aircraft advisory system. We find unsafe actions many times faster than the fastest existing method and certify no unsafe actions exist in about twice the time of the existing method. We also compute forward and backward reachable sets for a learned model of pendulum dynamics over a 50 time step horizon in 87s on a laptop computer. Algorithm source code: https://github.com/StanfordMSL/Neural-Network-Reach.