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.

翻译：我们提出了一种新颖的分支定界方法，用于开放环路和闭环设置下神经网络的可达性分析。核心思路是：首先利用凸规划离线计算神经网络在特定关注方向上的Lipschitz常数的精确界，随后基于这些界，通过Lipschitz连续性论证获得可达集的瞬时但保守的多面体近似。为降低保守性，我们将该定界算法嵌入分支策略中，以任意精度逐步减小过近似误差。进一步地，我们将该方法扩展至含神经网络控制器的控制系统可达性分析。最后，为尽可能精确地捕捉可达集的形状，我们利用样本轨迹，通过主成分分析（PCA）确定可达集过近似的方向。我们在多个开放环路与闭环场景下评估了所提方法的性能。