Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures

This paper proposes a novel algorithm for verifying the safety of nonlinear neural feedback systems by computing tight polyhedral enclosures of their transition functions and encoding them into a mixed-integer linear program (MILP), achieving an order-of-magnitude improvement over existing state-of-the-art methods.

The Gist

Imagine you are building a self-driving car or a drone that races through a forest. You've taught it using a "brain" made of a neural network (a type of AI). This AI is incredibly smart, but it's also a bit of a mystery box. It makes decisions based on complex, non-linear math that is hard to predict.

The big question is: Can we guarantee this AI won't crash?

If the car's physics were simple (like a toy car on a straight track), we could easily calculate every possible path it might take. But because the AI makes complex, wiggly decisions and the real world is messy, calculating the exact future path is impossible. It's like trying to predict the exact path of a leaf blowing in a hurricane.

This paper introduces a new tool called OVERTPoly to solve this problem. Here is how it works, explained with simple analogies.

1. The Problem: The "Black Box" and the "Wiggly Line"

Think of the AI controller as a black box that takes in the car's speed and position and spits out a steering command. The math inside this box is "non-linear," meaning if you double the input, the output doesn't just double; it might quadruple, or flip upside down.

Old methods tried to solve this in two ways:

• The "Fuzzy Cloud" method: They drew a giant, blurry cloud around the car to say, "It's definitely somewhere in here." This was fast, but the cloud got so big so quickly that it covered the whole city, making it useless for proving safety.
• The "Counting Every Possibility" method: They tried to check every single tiny scenario the AI could possibly choose. This was very precise, but it took so long (like trying to count every grain of sand on a beach) that it would take years to verify a 10-second drive.

2. The Solution: "Polyhedral Enclosures" (The Origami Box)

The authors propose a middle ground. Instead of a fuzzy cloud or counting every grain of sand, they use Polyhedral Enclosures.

Imagine you have a wiggly, curvy piece of string (the AI's behavior). You want to wrap it in a box so you know it can't escape.

• A simple box (a cube) is too loose; the string has too much room to wiggle.
• A perfect mold of the string is too hard to make.

The Polyhedral Enclosure is like origami. You take a piece of paper (a flat shape) and fold it into a box that fits the string very tightly, but the box is still made of flat, straight edges.

• The Magic: Because the box is made of flat, straight edges (mathematically called "polyhedra"), computers can solve the math for it very quickly.
• The Result: You get a tight, accurate box around the AI's behavior that is still easy for the computer to process.

3. How They Build the Box: "Lego Blocks"

The AI is made of many small math functions (like sine waves, multiplication, etc.). The authors treat these like Lego blocks.

1. Bound the Basics: First, they figure out the tightest possible "origami box" for each individual Lego block (e.g., "If the input is between 0 and 1, the output is definitely between 2 and 3").
2. Snap Them Together: They have a special rulebook for snapping these boxes together. If you snap a "multiplication box" to an "addition box," the rulebook tells you exactly how the new, bigger box should look.
3. The Result: They build a massive, multi-layered origami structure that perfectly wraps around the entire AI brain's decision-making process.

4. The "Time Machine" (Forward Reachability)

Now that they have a tight box for the AI, they need to see where the car goes over time.

• They don't just look at one second; they look at the whole trip.
• They use a technique called Symbolic Reachability. Imagine you are walking through a maze. Instead of walking step-by-step and getting lost, you take a giant leap and say, "If I am in this room, I could end up in any of these three rooms next."
• By doing this in "jumps" (groups of steps) rather than single steps, they avoid the math getting too messy (which usually happens when you do too many small steps).

5. The Results: Faster and Tighter

The authors tested their new tool, OVERTPoly, against the two best tools currently available:

• The "Fuzzy Cloud" tool (CORA): It was fast, but its boxes were too loose to prove safety for complex cars.
• The "Counting Everything" tool (OVERTVerify): It was very precise, but it was incredibly slow.

OVERTPoly won the race.

• It was 10 times faster than the precise tool.
• It was much more accurate than the fast tool.
• In some cases, it was the only tool that could finish the job without crashing the computer.

The Bottom Line

This paper is like inventing a new kind of safety net for AI-controlled machines. Instead of using a net that is too loose (letting the AI do dangerous things) or a net that takes a lifetime to weave (too slow to be useful), they built a net that is tight, strong, and quick to make.

This means we can now verify that complex AI systems (like self-driving cars or drones) are safe much faster and more reliably than ever before, bringing us one step closer to trusting robots with our lives.

Technical Summary

Here is a detailed technical summary of the paper "Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures".

1. Problem Statement

The paper addresses the critical safety challenge of neural feedback systems, where dynamical systems (e.g., drones, autonomous vehicles) are controlled by neural networks (NNs). While verification methods exist for systems with linear dynamics, verifying systems with nonlinear transition functions remains a significant bottleneck.

Existing approaches fall into two categories, both with limitations:

• Propagation-based methods (e.g., CORA): Use abstractions like zonotopes or Taylor models. They are computationally efficient but often produce loose over-approximations (high conservatism) for nonlinear systems, leading to false negatives (failing to verify safe systems).
• Combinatorial methods (e.g., OVERTVerify): Encode the problem as Mixed-Integer Linear Programs (MILPs) to handle NN nonlinearity precisely. While more precise, they suffer from poor scalability and high computational costs, often failing on complex benchmarks.

The goal is to develop a method that combines the precision of combinatorial methods with the scalability of propagation-based methods for nonlinear neural feedback systems.

2. Methodology: The OVERTPoly Algorithm

The authors propose OVERTPoly, a novel algorithm that uses Polyhedral Enclosures to create tight linear abstractions of nonlinear functions. The core workflow involves:

A. Polyhedral Enclosures

Instead of using global bounds, the algorithm constructs bounding sets for nonlinear functions.

• Bounding Set ($B$): Defined by a finite set of points $P$ in the domain and lower ($L$) and upper ($U$) bound functions evaluated at these points.
• Polyhedral Enclosure ($E$): The convex hull of the vertices formed by $(p, L(p))$ and $(p, U(p))$ for all $p \in P$. This creates a polyhedron in $n+1$ dimensions that encloses the graph of the function.
• Construction:
  1. Univariate Functions: The domain is partitioned into subintervals of uniform convexity. Piecewise-linear bounds are computed using the OVERT algorithm (stitching secant lines for upper bounds and tangent lines for lower bounds).
  2. Composition: For multivariate functions (e.g., $f(x) = x_4 \cos(x_3)$), the algorithm composes bounding sets of sub-functions.
     • Linear Ops (+, -): Bounds are combined directly.
     • Nonlinear Ops ($\times, \div$): The algorithm relaxes bounds within grid cells to constants, applies interval arithmetic, and refines the result. For bilinear terms, it utilizes McCormick envelopes to tighten the bounds further.
  3. Lifting and Interpolation: To compose functions with different input dimensions, the algorithm "lifts" bounding sets to a common dimension and "interpolates" them onto a shared grid of points to ensure the point sets match.

B. MILP Encoding

The polyhedral enclosures are encoded as Mixed-Integer Linear Programs (MILPs).

• The algorithm uses an aggregated convex combination method to represent any point in the domain as a convex combination of the vertices of a specific simplex in a Delaunay triangulation.
• Binary variables select the active simplex, and continuous variables represent the convex weights.
• This encoding ensures that the output of the nonlinear function is constrained to lie within the polyhedral enclosure.

C. Forward Reachability Analysis

The algorithm performs forward reachability analysis to compute the set of reachable states over time $T$:

• Concrete Reachability: Solves the MILP for one time step at a time. This is fast but accumulates "excess conservatism" (the reachable set grows too large due to repeated over-approximation).
• Symbolic Reachability: Solves for multiple time steps ($k$-steps) simultaneously within a single MILP. This tracks dependencies between state variables and significantly reduces conservatism.
• Dependency Graphs: To manage the scalability of symbolic reachability, the authors use dependency graphs to prune irrelevant models from the optimization problem, only including variables that actually influence the target state.

3. Key Contributions

1. Polyhedral Enclosures: A novel combinatorial abstraction for multivariate nonlinear functions that provides tighter bounds than standard zonotopes while remaining compatible with MILP solvers.
2. Efficient MILP Encoding: A method to encode these enclosures using aggregated convex combinations and SOS-2 constraints, enabling the use of standard MILP solvers (like Gurobi).
3. OVERTPoly Algorithm: A complete verification framework integrating bounding set construction, composition, and symbolic reachability analysis.
4. Performance Optimization: The use of dependency graphs and $k$-step symbolic analysis to mitigate the scalability issues typically associated with combinatorial verification.

4. Experimental Results

The authors evaluated OVERTPoly against CORA (state-of-the-art propagation) and OVERTVerify (state-of-the-art combinatorial) on four benchmarks from the ARCH Competition:

Benchmark	OVERTPoly (Time)	OVERTVerify (Time)	CORA (Time)	Key Finding
Single Pendulum	1.12s	0.73s	1.84s	All tools fast; CORA fastest, OVERTVerify most precise.
ACC (Adaptive Cruise)	12.28s	110.91s	4.78s	OVERTPoly is 9x faster than OVERTVerify with only a 2% increase in conservatism.
TORA	561.58s	983.76s	Failed	CORA could not verify due to set explosion. OVERTPoly was 2x faster than OVERTVerify.
Unicycle	3940s	16348s	Failed	CORA crashed. OVERTPoly was 4x faster than OVERTVerify.

• Scalability: In symbolic reachability tests (increasing time steps), OVERTPoly showed scalability improvements of several orders of magnitude over OVERTVerify.
• Precision: While OVERTPoly is slightly more conservative than OVERTVerify (due to the abstraction), it is significantly more precise than CORA, which often fails to verify complex nonlinear benchmarks entirely.

5. Significance

This work represents a major step forward in the formal verification of safety-critical autonomous systems.

• Bridging the Gap: It successfully bridges the gap between the speed of abstraction propagation and the precision of combinatorial methods.
• Scalability: By demonstrating that combinatorial methods can be scaled to handle complex, nonlinear benchmarks (like the Unicycle model) where previous tools failed, it makes the verification of realistic neural controllers feasible.
• Safety Assurance: The ability to verify nonlinear neural feedback systems with tight bounds provides a stronger guarantee of safety for applications in autonomous driving, robotics, and aerospace, moving the field closer to the deployment of certified AI controllers.