Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes

TL;DR

This paper introduces an adaptive polytope-based method for over-approximating the reachable sets of neural network-controlled dynamical systems, improving accuracy and efficiency in safety verification.

Contribution

It presents a novel approach combining adaptive template polytopes with SVD of linear layers and a branch-and-bound method for precise reachability analysis.

Findings

Effective over-approximation of neural network-controlled system reachability.

Improved computational efficiency over traditional methods.

Validated on linear systems with neural network controllers.

Abstract

Over-approximating the reachable sets of dynamical systems is a fundamental problem in safety verification and robust control synthesis. The representation of these sets is a key factor that affects the computational complexity and the approximation error. In this paper, we develop a new approach for over-approximating the reachable sets of neural network dynamical systems using adaptive template polytopes. We use the singular value decomposition of linear layers along with the shape of the activation functions to adapt the geometry of the polytopes at each time step to the geometry of the true reachable sets. We then propose a branch-and-bound method to compute accurate over-approximations of the reachable sets by the inferred templates. We illustrate the utility of the proposed approach in the reachability analysis of linear systems driven by neural network controllers.