Reachability Analysis and Safety Verification of Neural Feedback Systems via Hybrid Zonotopes

TL;DR

This paper introduces hybrid zonotope-based methods for precise reachability analysis and safety verification of neural feedback systems, enabling certification of safety and efficient computation of reachable sets.

Contribution

It develops novel hybrid zonotope algorithms for neural network layer analysis and system safety verification, providing the tightest convex relaxations and complexity reduction techniques.

Findings

Proposes hybrid zonotope methods for neural feedback systems.

Formulates safety certification as a mixed-integer linear program.

Demonstrates superior performance in numerical examples.

Abstract

Hybrid zonotopes generalize constrained zonotopes by introducing additional binary variables and possess some unique properties that make them convenient to represent nonconvex sets. This paper presents novel hybrid zonotope-based methods for the reachability analysis and safety verification of neural feedback systems. Algorithms are proposed to compute the input-output relationship of each layer of a feedforward neural network, as well as the exact reachable sets of neural feedback systems. In addition, a sufficient and necessary condition is formulated as a mixed-integer linear program to certify whether the trajectories of a neural feedback system can avoid unsafe regions. The proposed approach is shown to yield a formulation that provides the tightest convex relaxation for the reachable sets of the neural feedback system. Complexity reduction techniques for the reachable sets are developed to balance the computation efficiency and approximation accuracy. Two numerical examples demonstrate the superior performance of the proposed approach compared to other existing methods.