Stability and performance verification of dynamical systems controlled by neural networks: algorithms and complexity

TL;DR

This paper develops convex semidefinite programming methods to verify stability and performance of nonlinear systems controlled by neural networks, highlighting computational challenges and providing numerical validation for systems up to 50 dimensions.

Contribution

It introduces a convex semidefinite programming approach for stability verification of polynomial systems with neural network controllers, and discusses undecidability in linear cases.

Findings

Convex SDP can certify stability for polynomial systems with ReLU networks.

Verifying asymptotic stability in linear systems with ReLU networks is undecidable.

Numerical experiments validate the method on high-dimensional systems.

Abstract

This work makes several contributions on stability and performance verification of nonlinear dynamical systems controlled by neural networks. First, we show that the stability and performance of a polynomial dynamical system controlled by a neural network with semialgebraically representable activation functions (e.g., ReLU) can be certified by convex semidefinite programming. The result is based on the fact that the semialgebraic representation of the activation functions and polynomial dynamics allows one to search for a Lyapunov function using polynomial sum-of-squares methods. Second, we remark that even in the case of a linear system controlled by a neural network with ReLU activation functions, the problem of verifying asymptotic stability is undecidable. Finally, under additional assumptions, we establish a converse result on the existence of a polynomial Lyapunov function for this class of systems. Numerical results with code available online on examples of state-space dimension up to 50 and neural networks with several hundred neurons and up to 30 layers demonstrate the method.