Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems

TL;DR

This paper introduces Reachable Polyhedral Marching (RPM), an exact method for analyzing neural network-based control systems by computing control invariant sets and regions of attraction without Lyapunov functions.

Contribution

The paper presents RPM, a novel algorithm for incrementally enumerating neural network affine regions to compute exact reachable sets and control invariant sets for ReLU networks.

Findings

RPM can find non-convex control invariant sets and ROAs.

The accelerated RPM achieves a 15x speedup in computations.

Applied to aircraft runway control, RPM identified stabilizing state sets.

Abstract

Neural networks are increasingly used in robotics as policies, state transition models, state estimation models, or all of the above. With these components being learned from data, it is important to be able to analyze what behaviors were learned and how this affects closed-loop performance. In this paper we take steps toward this goal by developing methods for computing control invariant sets and regions of attraction (ROAs) of dynamical systems represented as neural networks. We focus our attention on feedforward neural networks with the rectified linear unit (ReLU) activation, which are known to implement continuous piecewise-affine (PWA) functions. We describe the Reachable Polyhedral Marching (RPM) algorithm for enumerating the affine pieces of a neural network through an incremental connected walk. We then use this algorithm to compute exact forward and backward reachable sets, from which we provide methods for computing control invariant sets and ROAs. Our approach is unique in that we find these sets incrementally, without Lyapunov-based tools. In our examples we demonstrate the ability of our approach to find non-convex control invariant sets and ROAs on tasks with learned van der Pol oscillator and pendulum models. Further, we provide an accelerated algorithm for computing ROAs that leverages the incremental and connected enumeration of affine regions that RPM provides. We show this acceleration to lead to a 15x speedup in our examples. Finally, we apply our methods to find a set of states that are stabilized by an image-based controller for an aircraft runway control problem.