Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions

要約

トレーニングニューラルネットワーク（NNS）は、バリア関数（BFS）として機能するようになります。これは、自律動的システムの安全性を改善するための一般的な方法です。
大幅に実際的な成功にもかかわらず、これらの方法は、実証可能な意味で真のBFSを生成することを一般的に保証していません。
この論文では、自律システムの国家回避に関して、学習したNNを正式に認証する問題をBFとして検討します：つまり。
候補NNが証明されている状態空間の領域を計算します。
特に、浅いNNのこのような証明書セットを効率的に生成するサウンドアルゴリズムを提案します。
私たちのアルゴリズムは、2つの新しいアプローチを組み合わせています。最初にNN Reachabilityツールを使用して、NNの出力がシステムの軌跡に沿って増加しない状態のサブセットを識別します。
次に、ハイパープレーン配置に新しい列挙アルゴリズムを使用して、NNのゼロサブレベルセットと最初の状態セットの交差点を見つけます。
このように、私たちのアルゴリズムは、NNがBFとして認定されている状態のサブセットをしっかりと見つけています。
さらに、2つのケーススタディでBFSとして実世界のNNを認証するアルゴリズムの有効性を実証します。
アルゴリズムの効率を示すスケーラビリティ実験でこれらを補完しました。

要約(オリジナル)

Training Neural Networks (NNs) to serve as Barrier Functions (BFs) is a popular way to improve the safety of autonomous dynamical systems. Despite significant practical success, these methods are not generally guaranteed to produce true BFs in a provable sense, which undermines their intended use as safety certificates. In this paper, we consider the problem of formally certifying a learned NN as a BF with respect to state avoidance for an autonomous system: viz. computing a region of the state space on which the candidate NN is provably a BF. In particular, we propose a sound algorithm that efficiently produces such a certificate set for a shallow NN. Our algorithm combines two novel approaches: it first uses NN reachability tools to identify a subset of states for which the output of the NN does not increase along system trajectories; then, it uses a novel enumeration algorithm for hyperplane arrangements to find the intersection of the NN’s zero-sub-level set with the first set of states. In this way, our algorithm soundly finds a subset of states on which the NN is certified as a BF. We further demonstrate the effectiveness of our algorithm at certifying for real-world NNs as BFs in two case studies. We complemented these with scalability experiments that demonstrate the efficiency of our algorithm.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google