Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes
This work addresses safety verification for RNNs in control systems, which is crucial for applications like autonomous vehicles and robotics, though it is an incremental improvement over existing reachability methods.
The paper tackles the problem of analyzing safety and reachability in closed-loop recurrent neural networks (RNNs) with ReLU activations by developing a hybrid zonotope-based method that computes exact forward and backward reachable sets without unrolling, and introduces a tunable relaxation scheme to improve scalability while allowing a tradeoff between complexity and accuracy.
Recurrent neural networks (RNNs) are widely employed to model complex dynamical systems due to their hidden-state structure, which inherently captures temporal dependencies. This work presents a hybrid zonotope-based approach for computing exact forward and backward reachable sets of closed-loop RNN systems with ReLU activation functions. The method formulates state-pair sets to compute reachable sets as hybrid zonotopes without requiring unrolling. To improve scalability, a tunable relaxation scheme is proposed that ranks unstable ReLU units across all layers using a triangle-area score and selectively applies convex relaxations within a fixed binary limit in the hybrid zonotopes. This scheme enables an explicit tradeoff between computational complexity and approximation accuracy, with exact reachability as a special case. In addition, a sufficient condition is derived to certify the safety of closed-loop RNN systems. Numerical examples demonstrate the effectiveness of the proposed approach.