Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes
This work addresses safety verification and robust control synthesis for neural network systems, representing an incremental improvement in reachability analysis techniques.
The paper tackles the problem of over-approximating reachable sets for neural network-controlled dynamical systems by developing an approach using adaptive template polytopes, resulting in a method that adapts polytope geometry based on singular value decomposition and activation functions to improve accuracy and computational efficiency.
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.