ReachLipBnB: A branch-and-bound method for reachability analysis of neural autonomous systems using Lipschitz bounds

TL;DR

ReachLipBnB introduces a branch-and-bound approach leveraging Lipschitz bounds for precise reachability analysis of neural autonomous systems, effectively reducing over-approximation errors in both open-loop and closed-loop scenarios.

Contribution

The paper presents a novel branch-and-bound method that combines Lipschitz bounds, convex programming, and PCA to improve the accuracy of neural network reachability analysis.

Findings

Effective reduction of over-approximation error

Applicable to both open-loop and closed-loop systems

Demonstrated improved accuracy in various settings

Abstract

We propose a novel Branch-and-Bound method for reachability analysis of neural networks in both open-loop and closed-loop settings. Our idea is to first compute accurate bounds on the Lipschitz constant of the neural network in certain directions of interest offline using a convex program. We then use these bounds to obtain an instantaneous but conservative polyhedral approximation of the reachable set using Lipschitz continuity arguments. To reduce conservatism, we incorporate our bounding algorithm within a branching strategy to decrease the over-approximation error within an arbitrary accuracy. We then extend our method to reachability analysis of control systems with neural network controllers. Finally, to capture the shape of the reachable sets as accurately as possible, we use sample trajectories to inform the directions of the reachable set over-approximations using Principal Component Analysis (PCA). We evaluate the performance of the proposed method in several open-loop and closed-loop settings.