Branch and bound improves verifying nonlinear neural feedback systems scalability
Closing the Loop: Branch-and-Bound for Scalable Verification of Nonlinear Neural Feedback Systems
Artificial Intelligence
Summary
Verifying that complex systems controlled by neural networks behave safely is hard because these systems are large and have complicated dynamics. Existing methods either can't handle big networks or lose too much detail to be accurate. The authors develop a new method that breaks the problem into smaller parts and uses smarter math to keep track of relationships over time, making verification more practical for bigger systems. Their method shows better performance than previous approaches.
What this means in practice
- •For autonomy engineers: Verify safety properties of autonomous systems controlled by nonlinear neural networks at larger scales than before.
- •For control systems designers: Improve confidence in controllers for nonlinear dynamic systems by enabling scalable verification of neural feedback loops.
Authors
I. Samuel Akinwande, Mykel J. Kochenderfer, Clark Barrett
Abstract
Despite recent advances in the verification of nonlinear neural feedback systems, scalability remains the central obstacle, as state-of-the-art solvers do not yet handle the network sizes and nonlinear dynamics of autonomy applications. Combinatorial solvers do not scale to large networks, whereas propagative solvers excessively sacrifice precision. This work seeks to improve the scalability of combinatorial solvers by formulating verification as branch-and-bound on an abstraction of the closed-loop system. We introduce \rail, an interface that exposes polyhedral enclosures of the dynamics to LiRPA-style bound propagation, and \clipper, a branch-and-bound algorithm that jointly refines enclosures and splits controller activations. This framework enables joint reasoning on the computational graph of the closed-loop system, preserving symbolic correlations across time steps. We present our construction and show that it yields significant improvements over the state of the art.