Polytopic Trees for Verification of Learning-Based Controllers

Abstract

Reinforcement learning is increasingly used to synthesize controllers for a broad range of applications. However, formal guarantees on the behavior of learning-based controllers are elusive due to the blackbox nature of machine learning models such as neural networks. In this paper, we propose an algorithm for verifying learning-based controllers—in particular, deep neural networks with ReLU activations, and decision trees with linear decisions and leaf values—for deterministic, piecewise affine (PWA) dynamical systems. In this setting, our algorithm computes the safe (resp., unsafe) region of the state space—i.e., the region of the state space on which the learned controller is guaranteed to satisfy (resp., fail to satisfy) a given reach-avoid specification. Knowing the safe and unsafe regions is substantially more informative than the boolean characterization of safety (i.e., safe or unsafe) provided by standard verification algorithms—for example, this knowledge can be used to compose controllers that are safe on different portions of the state space. At a high level, our algorithm uses convex programming to iteratively compute new regions (in the form of polytopes) that are guaranteed to be entirely safe or entirely unsafe. Then, it connects these polytopic regions together in a tree-like fashion. We conclude with an illustrative example on controlling a hybrid model of a contact-based robotics problem.

This research was partially supported by ONR award N00014-17-1-2699.

A Appendix

1.1 A.1 Proof of Theorem 2

Proof

Let $X^i_{r}=X^{\max }_{s} \setminus X^i_{s}$. We need to show that with probability one. The same argument holds for $X^{\max }_{f} \setminus X^i_{f}$. We prove by contradiction. Let $\lim _{i \rightarrow \infty } X_r^i$ be a measurable set. It follows from Assumption 1 that we obtain a sample from $X_r^{\infty }$ with non-zero probability. Then we simulate the system forward from the sampled state $x_0$. Once the trajectory is obtained, the polytopic trajectory is computed, and by Assumption 2, we obtain a measurable $\mathbb {P}_0$, centered at that has non-empty intersection with $X_r^{\infty }$. Therefore, by non-zero probability, the volume of $X_r^{i}$ shrinks in one iteration by at least $\lambda$. Thus we reach a contradiction.