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

We present a method for computing exact reachable sets for deep neural\nnetworks with rectified linear unit (ReLU) activation. Our method is\nwell-suited for use in rigorous safety analysis of robotic perception and\ncontrol systems with deep neural network components. Our algorithm can compute\nboth forward and backward reachable sets for a ReLU network iterated over\nmultiple time steps, as would be found in a perception-action loop in a robotic\nsystem. Our algorithm is unique in that it builds the reachable sets by\nincrementally enumerating polyhedral cells in the input space, rather than\niterating layer-by-layer through the network as in other methods. If an unsafe\ncell is found, our algorithm can return this result without completing the full\nreachability computation, thus giving an anytime property that accelerates\nsafety verification. In addition, our method requires less memory during\nexecution compared to existing methods where memory can be a limiting factor.\nWe demonstrate our algorithm on safety verification of the ACAS Xu aircraft\nadvisory system. We find unsafe actions many times faster than the fastest\nexisting method and certify no unsafe actions exist in about twice the time of\nthe existing method. We also compute forward and backward reachable sets for a\nlearned model of pendulum dynamics over a 50 time step horizon in 87s on a\nlaptop computer. Algorithm source code:\nhttps://github.com/StanfordMSL/Neural-Network-Reach.\n