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

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.

References in corpus (2)

• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• DeepChess: End-to-End Deep Neural Network for Automatic Learning in Chess

Cited by in corpus (5)

• Reachability Analysis and Safety Verification of Neural Feedback Systems via Hybrid Zonotopes
• Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems
• Verification of Neural Network Control Systems in Continuous Time
• The inverse problem for neural networks
• The Reachability Problem for Neural-Network Control Systems