We introduce a branch‑and‑bound framework that makes verification of nonlinear neural feedback systems scalable.
First, we provide the \rail interface, which wraps the closed‑loop dynamics into polyhedral enclosures and exposes them to a LiRPA‑style bound propagation engine.
On top of this, we implement the \clipper algorithm. During the branch‑and‑bound search it jointly refines the polyhedral enclosures and splits the activation patterns of the controller.
By reasoning over the entire closed‑loop computational graph, the method preserves symbolic correlations across time steps, dramatically improving the scalability of combinatorial solvers.
Empirical results on several autonomous‑system benchmarks show substantial gains over the current state‑of‑the‑art.
Review