The FABRIC Strategy for Verifying Neural Feedback Systems

This paper introduces the FaBRIC strategy, which integrates new scalable backward reachability algorithms with existing forward analysis techniques to significantly improve the verification of reach-avoid specifications in nonlinear neural feedback systems.

The Gist

Imagine you are the chief safety inspector for a fleet of self-driving cars, drones, and robots. These machines are controlled by "neural networks"—essentially, highly complex digital brains that learn how to drive or fly by looking at examples, rather than following a strict rulebook.

The big question is: Can we guarantee these machines will never crash or fly into a wall, no matter what happens?

This is where the paper comes in. It introduces a new strategy called FABRIC (Forward and Backward Reachability Integration for Certification). To understand why FABRIC is a big deal, let's use a simple analogy.

The Problem: The Foggy Mountain Pass

Imagine you are trying to get a hiker (the robot) from a starting camp (the Initial State) to a summit (the Goal State) without falling off a cliff (the Unsafe State).

The terrain is foggy, and the hiker's path is controlled by a mysterious guide (the Neural Network) who makes decisions based on what they see. The path is also slippery and unpredictable (non-linear dynamics).

The Old Way (Forward Analysis Only):
Most safety inspectors only look forward. They start at the camp and simulate thousands of possible paths the hiker could take.

• The Problem: If the hiker has a million possible paths, simulating them all takes forever. Even if you simulate a million, you can't be 100% sure you didn't miss the one path that leads to a cliff. It's like trying to find a needle in a haystack by looking at one straw at a time.

The Missing Piece (Backward Analysis):
What if, instead of just looking forward, you also looked backward from the summit?

• You ask: "From which spots on the mountain can the hiker guarantee they will reach the summit?"
• You also ask: "From which spots is it impossible to reach the summit without falling?"

This is Backward Reachability. It's like shining a flashlight from the destination back toward the start. However, doing this for a robot controlled by a "black box" neural network is incredibly hard. It's like trying to reverse-engineer a complex recipe just by tasting the final dish. Previous attempts at this were too slow or inaccurate to be useful.

The Solution: FABRIC

The authors of this paper built a new set of tools to make Backward Analysis work effectively, and then combined it with the old Forward Analysis to create FABRIC.

Think of FABRIC as a Two-Way Street Safety Check:

1. The Forward Lane (The "What If" Check): We simulate the robot moving forward from the start. We create a "safety bubble" around all the places it might go.
2. The Backward Lane (The "Must Reach" Check): We work backward from the goal. We create a "safe zone" of all the places the robot must be in to successfully reach the goal.

The Magic Moment:
If the "Forward Safety Bubble" and the "Backward Safe Zone" overlap, you have a mathematical proof that the robot will reach the goal safely. You don't need to simulate every single path; you just need to prove the two zones touch.

The New Tools (The "How")

To make this work, the authors invented three new "tricks" to handle the messy, non-linear math of neural networks:

• DRIPy (The Domain Refiner): Imagine trying to find a lost key in a giant warehouse. The old way was to check the whole warehouse. DRIPy is like a smart flashlight that starts with the whole warehouse, finds the general area where the key might be, and then shrinks the search area step-by-step until it's a tiny, precise box. This makes the backward check much faster.
• SHARP, CRISP, and CLEAN (The Inner Set Finders): Sometimes you need to prove that a specific area is definitely safe.
  • SHARP is like shrinking a balloon from the outside until it fits perfectly inside the safe zone.
  • CRISP is like throwing darts at a map; if the darts land in safe spots, you draw a box around them.
  • CLEAN is like taking a map and erasing all the dangerous spots, then drawing the biggest possible safe box in the remaining white space.

Why This Matters

Before this paper, verifying complex robots was like trying to solve a puzzle by only looking at half the pieces. It was slow, and often you couldn't prove the robot was safe.

FABRIC changes the game by:

1. Speed: It solves these problems much faster than before (sometimes 7 times faster!).
2. Certainty: It provides a mathematical guarantee, not just a guess.
3. Scalability: It works on bigger, more complex robots (like the "Attitude Control" drone in their tests) that previous methods couldn't handle.

The Bottom Line

The authors didn't just invent a new math trick; they built a two-way verification system. By looking forward and backward simultaneously, they created a strategy (FABRIC) that makes it possible to trust autonomous systems—like self-driving cars and medical robots—with a level of safety assurance that was previously out of reach.

It's the difference between hoping your bridge won't collapse because you walked across it once, and having a structural engineer prove, using math from both ends of the bridge, that it will hold up under any storm.

Technical Summary

Here is a detailed technical summary of the paper "The FABRIC Strategy for Verifying Neural Feedback Systems."

1. Problem Statement

Neural Feedback Systems (NFS), where dynamical systems are controlled by neural networks (NNs), are increasingly prevalent in robotics and autonomous systems. Verifying that these systems satisfy reach-avoid specifications (reaching a goal state while avoiding unsafe states) is critical for safety.

Existing verification methods face significant limitations:

• Forward Reachability: Dominates the field but struggles with the "curse of dimensionality" and often lacks precision for complex nonlinear dynamics.
• Backward Reachability: Historically underutilized for NFS due to scalability issues. Computing backward reachable sets (BRS) requires propagating sets backward through a neural network and nonlinear system dynamics, which is computationally challenging.
• Current State-of-the-Art: Existing backward methods for nonlinear NFS are either too conservative (loose bounds) or fail to scale to higher-dimensional systems.

The core problem addressed is the lack of scalable, precise algorithms for computing both over-approximations (outer sets) and under-approximations (inner sets) of backward reachable sets for nonlinear neural feedback systems, and the absence of a unified strategy to leverage both forward and backward analyses effectively.

2. Methodology

The authors propose FABRIC (Forward and Backward Reachability Integration for Certification), a strategy that integrates forward analysis with new backward analysis techniques.

A. Backward Reachability Algorithms

The paper introduces new algorithms to compute approximations of the backward reachable sets, distinguishing between:

• May-BRS (Outer Sets): States that may reach a target (used for safety/avoidance verification).
• Must-BRS (Inner Sets): States that must reach a target (used for reachability verification).

1. Outer Set Computation (Over-approximation):

• Polyhedral Enclosures: The authors use polyhedral enclosures to bound nonlinear transition dynamics and the neural network controller.
• DRIPy (Domain Refinement with Polyhedral Enclosures): An extension of the DRIP algorithm (originally for linear systems) to nonlinear settings.
  • Mechanism: It iteratively refines the domain $D$ over which the backward reachability problem is solved. It starts with a conservative domain, solves Mixed-Integer Linear Programs (MILPs) to find bounds on the backward reachable set, and shrinks the domain to these bounds.
  • Optimization: It supports both "concrete" (step-by-step) and "symbolic" (multi-step simultaneous) approaches to balance precision and computational cost.

2. Inner Set Computation (Under-approximation):
To find a certified inner set (a subset of the true Must-BRS), the authors formulate an optimization problem: find the largest subset of an outer set whose forward image is fully contained within the target set. Three specific algorithms are proposed:

• SHARP (Scaled Hyperrectangular Approximation): Scales an outer hyperrectangle inward via iterative line search (Golden-section) to find the largest valid inner rectangle.
• CRISP (Convex Rectangle Inferred via Sampled Positives): Uses space-filling sampling (Sobol sequences) on the outer set. It classifies samples as "positive" (forward reachable to target) or "negative." It then computes the largest axis-aligned hyperrectangle contained within the convex hull of the positive samples.
• CLEAN (Constrained Local Exclusion of Aligned Negatives): Similar to CRISP but explicitly excludes negative samples. It formulates a Mixed-Integer Linear Program (MILP) to find the largest rectangle that contains no negative samples, handling non-convex or irregular backward reachable sets.

B. The FABRIC Integration Strategy

FABRIC partitions the time horizon $T$ into $F$ (forward) and $B$ (backward) steps ($T = F + B$).

• Reach Properties: Run $F$ steps of forward over-approximation from the initial set and $B$ steps of backward under-approximation from the goal. If the forward set at step $F$ is contained within the backward set, the goal is reachable.
• Avoid Properties: Run $F$ steps of forward over-approximation and $B$ steps of backward over-approximation from the unsafe set. If the forward sets never intersect the unsafe set or the backward "may-reachable" set, the system is safe.
• Rationale: Forward analysis is generally cheaper; backward analysis is more expensive but provides tighter constraints for reachability. FABRIC balances these to minimize total computation time while maintaining soundness.

3. Key Contributions

1. New Backward Algorithms: Introduced algorithms for computing over-approximations (via DRIPy) and under-approximations (via SHARP, CRISP, CLEAN) of backward reachable sets for nonlinear neural feedback systems.
2. Domain Refinement Extension: Extended the DRIP domain refinement technique from linear to nonlinear transition dynamics using polyhedral enclosures.
3. FABRIC Strategy: Developed a unified verification framework that dynamically combines forward and backward reachability analysis to outperform single-direction approaches.
4. Comprehensive Evaluation: Validated the approach on a representative benchmark suite (ARCH Competition) covering TORA, Unicycle, and Attitude control models with varying neural network sizes.

4. Results

The evaluation compared FABRIC and its components against state-of-the-art baselines: HyBReach-MILP (for outer sets), BURNS (for inner sets), and pure Forward Analysis.

• Outer Sets (Over-approximation):

  • DRIPy significantly outperformed HyBReach-MILP in scalability. On the Unicycle and Attitude benchmarks, DRIPy was up to 90x faster and produced outer sets 40x to 2900x smaller (tighter) than HyBReach-MILP, especially when domain refinement was applied.
  • HyBReach-MILP frequently timed out on larger benchmarks, whereas DRIPy succeeded.

• Inner Sets (Under-approximation):

  • CRISP was the best-performing variant, successfully computing certified inner sets where BURNS failed (returned empty sets or failed to converge) on high-dimensional benchmarks (Unicycle, Attitude).
  • BURNS struggled with the "curse of dimensionality" in 6D spaces, while sampling-based approaches (CRISP/CLEAN) succeeded by sampling from the smaller outer set rather than the full domain.

• FABRIC Strategy:

  • On challenging benchmarks (Unicycle), FABRIC achieved speedups of up to 7x compared to forward-only analysis for both reach and avoid properties.
  • On simpler benchmarks (TORA), the overhead of backward analysis made FABRIC slower, highlighting the need for adaptive parameter selection ($F$ vs. $B$).
  • Overall, FABRIC demonstrated that integrating backward analysis can drastically reduce verification time for complex nonlinear systems.

5. Significance

This work addresses a critical gap in the formal verification of safety-critical AI systems. By enabling scalable backward reachability analysis for nonlinear neural feedback systems, the authors provide a powerful tool for:

• Formal Guarantees: Moving beyond sampling-based falsification to provide mathematical proofs of safety and liveness.
• Efficiency: Solving verification problems that were previously intractable due to the computational cost of backward analysis.
• Precision: Offering tighter bounds (smaller over-approximations and larger under-approximations) than existing methods, reducing false positives in safety verification.

The FABRIC strategy represents a paradigm shift from relying solely on forward propagation to a hybrid approach that leverages the strengths of both forward and backward reasoning, paving the way for the rigorous certification of complex autonomous systems controlled by deep neural networks.