Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes

This paper proposes a hybrid zonotope-based framework for computing exact and scalable forward and backward reachable sets of closed-loop ReLU RNNs without unrolling, featuring a tunable relaxation scheme to balance computational complexity and approximation accuracy while providing a sufficient condition for safety certification.

The Gist

Imagine you have a very smart, but slightly unpredictable, robot driver. This robot is trained to drive a car (the "plant") using a set of rules it learned from data (a Recurrent Neural Network, or RNN). Because the robot remembers its past actions and the car's history, it's great at handling complex, changing roads.

However, there's a big problem: We don't fully trust it yet. If you ask, "What if the robot makes a mistake and crashes?" or "What starting positions could lead to a crash?", it's incredibly hard to answer. The robot's internal "brain" is a black box with thousands of connections, and checking every single possibility one by one is like trying to count every grain of sand on a beach while the tide is coming in.

This paper presents a new, clever way to map out exactly where this robot can go and where it can't go, without getting lost in the math. Here is the breakdown using everyday analogies:

1. The Core Problem: The "Unrolling" Trap

Usually, to predict what a robot will do over time, researchers try to "unroll" the robot's brain. Imagine taking a video of the robot driving for 10 seconds and laying out every single frame side-by-side to analyze it.

• The Issue: As you add more seconds (time steps), the video gets huge. The computer gets overwhelmed, and the analysis becomes too slow to be useful.
• The Paper's Solution: Instead of laying out the whole video, they look at the relationship between the start and the finish directly. They treat the "Start State" and the "End State" as a pair, like a "Before and After" photo, and figure out the rules that connect them without looking at every single frame in between.

2. The Tool: Hybrid Zonotopes (The "Smart Cloud")

To do this, they use a mathematical shape called a Hybrid Zonotope.

• The Analogy: Imagine you are trying to draw a cloud that represents all possible places a robot could be.
  • A simple box (a rectangle) is too loose; it includes places the robot can never reach.
  • A perfect, jagged shape is too hard to calculate.
  • A Hybrid Zonotope is like a "smart cloud." It's a shape that can stretch and twist to fit the robot's possible movements tightly. It has two types of "wires" holding it together:
    1. Continuous wires: For smooth, predictable movements.
    2. Binary switches: For the "on/off" decisions the robot makes (like a traffic light turning red or green).
  • This shape is tight enough to be accurate but simple enough for a computer to handle.

3. The Innovation: The "Triangle-Area" Score

The biggest headache with these "smart clouds" is that every time the robot makes a tricky decision (specifically, a "ReLU" activation, which is like a light switch that only turns on if the signal is positive), the cloud gets more complex. If the robot has to make 1,000 decisions, the cloud becomes a tangled mess that the computer can't solve.

The authors came up with a tunable relaxation scheme.

• The Analogy: Imagine you are packing a suitcase for a trip. You have limited space (computing power). You have 100 items (decisions) to pack.
  • Some items are fragile and must be packed exactly (Exact ReLU).
  • Some items are soft and can be squished a bit (Relaxed ReLU).
  • The Trick: They assign a "score" to every decision based on how much "room" it takes up if you squish it. They call this the "Triangle-Area Score."
  • They sort the decisions from "most important to keep exact" to "least important."
  • Then, they say: "We can only keep the top 10 decisions exact. The rest? We'll squish them into a simple triangle shape."
• The Result: You can choose how much accuracy you want. If you need 100% safety, you keep them all exact (but it takes longer). If you need a quick answer, you squish more of them (it's faster but slightly less precise). It's a slider between Speed and Safety.

4. Two-Way Street: Forward and Backward

Most previous methods only looked Forward: "If I start here, where will I end up?"
This paper does Backward analysis too: "If I want to end up in a crash zone, where did I have to start?"

• Forward (The Future): "If we start in this parking spot, will the car hit the wall in 5 seconds?"
• Backward (The Past): "If the car hits the wall in 5 seconds, which parking spots were dangerous to begin with?"
• Why it matters: This is crucial for finding "adversarial" attacks (tricks that fool the AI) and for designing controllers that guarantee safety by avoiding those dangerous starting spots.

5. The Safety Check

Finally, they use these maps to prove safety.

• Imagine drawing a "No-Go Zone" (like a red circle on a map) where the car shouldn't go.
• The method checks if the "Smart Cloud" of possible future positions ever touches the red circle.
• If the cloud and the red circle don't touch, the system is safe.
• If they do touch, the method can actually trace back and show you the exact path the robot took to get there, so engineers can fix the code.

Summary

In short, this paper gives engineers a GPS for AI safety.
Instead of trying to simulate every possible future (which is impossible), they create a tight, mathematical "cloud" that wraps around all possible futures. They invented a smart way to simplify this cloud so it doesn't crash the computer, allowing them to check if a self-driving car (or any AI controller) will stay safe, and even work backward to find out exactly how it might fail.

It turns a "black box" problem into a "clear map" problem, giving us the confidence to put these smart robots in charge of critical systems.

Technical Summary

Here is a detailed technical summary of the paper "Forward and Backward Reachability Analysis of Closed-loop Recurrent Neural Networks via Hybrid Zonotopes" by Yuhao Zhang and Xiangru Xu.

1. Problem Statement

Recurrent Neural Networks (RNNs) are increasingly used in safety-critical control systems to model complex dynamics and design controllers. However, their deployment raises significant safety concerns due to issues like sensitivity to input perturbations and the "exploding gradient" problem.

The core challenge addressed in this paper is the reachability analysis of closed-loop RNN systems (where an RNN plant and an RNN controller are interconnected). Specifically, the authors aim to compute:

• Forward Reachable Sets (FRS): The set of all possible states the system can reach from a given initial set over a time horizon.
• Backward Reachable Sets (BRS): The set of all initial states that can lead to a specific target (or unsafe) set within a time horizon.

Key Constraints & Challenges:

• Exactness vs. Scalability: Existing methods either "unroll" the RNN into a large feedforward network (causing exponential growth in complexity) or use invariant inference (which accumulates over-approximation errors).
• Closed-Loop Dynamics: The feedback loop creates temporal and structural dependencies between hidden states across layers and time steps, making standard Feedforward Neural Network (FNN) verification techniques inapplicable.
• Nonlinearity: The presence of ReLU activation functions introduces non-convexity, requiring precise handling to avoid overly conservative results.

2. Methodology

The authors propose a novel set-based framework using Hybrid Zonotopes (HZs) to represent reachable sets without unrolling the RNN.

A. Hybrid Zonotopes (HZs)

An HZ is a set representation that combines continuous generators (like standard zonotopes) and binary generators (to capture non-convexities). It is defined by generators and linear equality constraints, allowing it to exactly represent the graph of ReLU activation functions.

B. State-Pair Sets and Hidden-State-Pair Sets

To handle the temporal dependencies of RNNs without unrolling, the authors introduce two key concepts:

1. State-Pair Set ($S_x$): A set containing pairs of the initial state ($x_1$) and the state at time $t$ ($x_t$).
2. Hidden-State-Pair Set ($S_h$): A set containing pairs of hidden states from adjacent layers/time steps (e.g., $h^{(\ell)}_{t-1}$ and $h^{(\ell-1)}_t$).

These sets are constructed using a Constrained Product operation on HZs. This operation enforces equality constraints between the two operands, ensuring that the pairs are generated by the same initial state, thereby preserving the system's trajectory logic.

C. Exact Reachability Algorithm (Algorithm 1)

The method propagates the initial state set through the RNN layers and time steps:

1. Initialization: Start with the initial state set as an HZ.
2. Pairing: For each time step $t \ge 2$, compute the hidden-state-pair set by taking the constrained product of the previous hidden state and the current layer's input.
3. Linear Mapping: Apply the weight matrices to the paired sets.
4. ReLU Handling: Represent the ReLU activation graph exactly as an HZ using the interval hull of the input.
5. Output: Construct the final state-pair set by combining the initial state and the state at time $t$.
6. Projection: Extract the FRS or BRS by projecting the state-pair set onto the relevant dimensions.

D. Tunable Relaxation Scheme (Algorithm 2)

To address scalability issues caused by the exponential growth of binary generators (which occurs with every unstable ReLU), the authors propose a tunable relaxation scheme:

• Triangle-Area Score: For every unstable ReLU unit (where the input interval $[\alpha, \beta]$ spans zero), a "triangle-area" score is calculated: $score = -\alpha \cdot \beta / 2$. This represents the area of the convex relaxation gap.
• Ranking & Selection: All unstable ReLUs across all layers and time steps are ranked by this score.
• Binary Limit ($N_b$): A user-defined parameter $N_b$ limits the number of ReLUs kept as exact (binary) representations.
  • The top $N_b$ ReLUs (highest scores) are kept exact.
  • The remaining ReLUs are approximated using a triangle relaxation (convex hull), which removes binary generators and reduces the set to a constrained zonotope.
• Trade-off: This allows an explicit trade-off between computational complexity and approximation accuracy. If $N_b$ is large enough to cover all unstable units, the result is exact.

E. Safety Verification

The paper derives a sufficient condition for safety:

• Forward: Check if the over-approximated FRS intersects with the unsafe set $O$.
• Backward: Check if the over-approximated BRS of the unsafe set intersects with the initial set $X_1$.
• If the intersection is empty, the system is safe. If not, the BRS can be used to explicitly construct unsafe trajectories.

3. Key Contributions

1. Exact Reachability without Unrolling: The first method to compute exact forward and backward reachable sets for closed-loop RNNs with ReLU activations using Hybrid Zonotopes, avoiding the computational explosion of unrolling.
2. Tunable Relaxation Framework: A novel scheme that ranks unstable ReLU units globally (across all layers and time steps) based on a triangle-area score. This enables a controlled trade-off between complexity and accuracy via a single binary limit parameter.
3. Safety Certification: A derived sufficient condition for verifying the safety of closed-loop RNN systems and identifying specific unsafe initial sequences using backward reachability.
4. Unified Approach: The framework unifies the computation of both forward and backward reachability, which is crucial for control synthesis and adversarial analysis.

4. Results

The authors validated their approach using numerical examples:

• Mass-Spring-Damper System: A closed-loop system with a 2-cart mass-spring-damper plant and an MPC controller, both approximated by RNNs.
• Performance:
  • The method successfully computed FRSs up to $T=5$ steps.
  • Scalability: By varying the binary limit parameter $N_b$, the authors demonstrated that the size of the over-approximated reachable sets decreases monotonically as $N_b$ increases.
  • Exactness: When $N_b$ was set to cover all unstable ReLUs ($N_t$), the computed sets matched the exact reachable sets.
  • Backward Analysis: The method successfully identified the set of initial states that could lead to a specified unsafe region and reconstructed the corresponding unsafe trajectories.

5. Significance

• Bridging the Gap: This work addresses a critical gap in the literature where backward reachability for closed-loop RNNs was largely unexplored.
• Control Safety: It provides a rigorous mathematical tool for certifying the safety of neural network-based controllers, a prerequisite for deploying RNNs in autonomous vehicles, robotics, and industrial automation.
• Efficiency: By avoiding unrolling and offering a tunable relaxation, the method makes reachability analysis feasible for longer time horizons and larger networks compared to previous state-of-the-art methods.
• Generalizability: While focused on RNNs, the underlying set-propagation logic and HZ framework are adaptable to other architectures (FNNs, CNNs) and nonlinear plant models.