Verifying Safety of Neural Networks from Topological Perspectives

要約

ニューラル ネットワーク (NN) は、自動運転車などの安全性が重要なシステムにますます適用されています。
しかし、彼らは傷つきやすく、行儀が悪いことがよくあります。
したがって、実際に展開する前に、それらの動作は厳格な保証を受ける必要があります。
本稿では、トポロジカルな観点からNNの安全性検証問題を調査するためのセット境界到達可能性手法を提案します。
入力セットと安全セットを持つ NN が与えられた場合、安全性検証の問題は、入力セットから得られる NN のすべての出力が安全セット内に収まるかどうかを判断することです。
私たちの方法では、NN の同相同型特性とオープン マップ特性が主に利用され、入力セットの境界と出力セットの境界の間に厳密な保証が確立されます。
これら 2 つのプロパティを活用すると、入力セット全体ではなく入力セットのサブセットを抽出することで到達可能性の計算が容易になり、到達可能性分析におけるラッピング効果を制御し、安全性検証のための計算負荷の軽減が容易になります。
準同型性特性は、可逆残差ネットワーク (i-ResNets) やニューラル常微分方程式 (Neural ODE) などの一部の広く使用されている NN に存在します。オープン マップは、準同型性特性と比較して厳密性が低く、満たしやすい特性です。
これらのプロパティのいずれかを確立する NN の場合、セット境界到達可能性メソッドは、入力セットの境界で到達可能性分析を実行するだけで済みます。
さらに、入力セットに関してこれらのプロパティを備えていない NN の場合、局所同型特性を確立するために入力セットのサブセットを探索し、到達可能性の計算のためにこれらのサブセットを放棄します。
最後に、いくつかの例で、提案された方法のパフォーマンスを示します。

要約(オリジナル)

Neural networks (NNs) are increasingly applied in safety-critical systems such as autonomous vehicles. However, they are fragile and are often ill-behaved. Consequently, their behaviors should undergo rigorous guarantees before deployment in practice. In this paper, we propose a set-boundary reachability method to investigate the safety verification problem of NNs from a topological perspective. Given an NN with an input set and a safe set, the safety verification problem is to determine whether all outputs of the NN resulting from the input set fall within the safe set. In our method, the homeomorphism property and the open map property of NNs are mainly exploited, which establish rigorous guarantees between the boundaries of the input set and the boundaries of the output set. The exploitation of these two properties facilitates reachability computations via extracting subsets of the input set rather than the entire input set, thus controlling the wrapping effect in reachability analysis and facilitating the reduction of computation burdens for safety verification. The homeomorphism property exists in some widely used NNs such as invertible residual networks (i-ResNets) and Neural ordinary differential equations (Neural ODEs), and the open map is a less strict property and easier to satisfy compared with the homeomorphism property. For NNs establishing either of these properties, our set-boundary reachability method only needs to perform reachability analysis on the boundary of the input set. Moreover, for NNs that do not feature these properties with respect to the input set, we explore subsets of the input set for establishing the local homeomorphism property and then abandon these subsets for reachability computations. Finally, some examples demonstrate the performance of the proposed method.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google