Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming

TL;DR

This paper introduces Reach-SDP, a semidefinite programming-based method for safety verification of neural network controlled systems by approximating reachable sets, demonstrated on a quadrotor example.

Contribution

It presents a novel reachability analysis technique that abstracts neural network activations with quadratic constraints, enabling safety verification of neural network feedback systems.

Findings

Successfully certifies finite-time reachability in a quadrotor system.

Provides outer-approximation of reachable sets using semidefinite programming.

Demonstrates effectiveness in verifying safety constraints for neural network controllers.

Abstract

There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these systems is challenging due to the nonlinear and compositional structure of neural networks. In this paper, we propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback interconnection. Our technical approach relies on abstracting the nonlinear activation functions by quadratic constraints, which leads to an outer-approximation of forward reachable sets of the closed-loop system. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.