Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes

TL;DR

This paper introduces a novel polynomial zonotope-based method for neural network verification and reachability analysis, effectively capturing non-convexities and improving performance over existing approaches.

Contribution

It proposes a new set-based abstraction using polynomial zonotopes for neural network verification and system reachability, handling non-convexities more accurately.

Findings

Outperforms existing methods on benchmark tests

Efficiently captures non-convex neural network behaviors

Applicable to open- and closed-loop system verification

Abstract

We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.