線形バウンド伝播によるニューラル制御バリア関数のスケーラブルな検証
Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
ニューラル制御バリア関数の検証を、線形バウンド伝播とマコーミック緩和で効率化し、大規模ネットワークにも適用可能にした。
詳しい要約
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術・手法の肝は？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
※ AIが要旨から生成した要約です。正確性は原文をご確認ください。
著者: Nikolaus Vertovec, Frederik Baymler Mathiesen, Thom Badings, Luca Laurenti, Alessandro Abate
分類: cs.LG, cs.RO, cs.SY, eess.SY, math.OC
原文アブストラクト
Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments.
