arXiv reaDer
Correctness Verification of Neural Networks
知覚タスクのニューラル ネットワークの正しさをグローバルに指定および検証するための新しいフレームワークを提示します。知覚タスクのニューラル ネットワーク検証に関するこれまでの研究のほとんどは、ロバスト性の検証に焦点を当てています。ラベル付けされたポイント周辺の一部のローカル領域でネットワークの予測が安定していることを検証することを目的とする堅牢性の検証とは異なり、私たちのフレームワークは、ターゲット入力空間全体でグローバルに正確性を指定し、ネットワークがすべてのターゲット入力に対して正しいことを検証する方法を提供します(または、ネットワークが正しくない地域を見つけます)。 1) 世界の関連するすべての状態から構成される状態空間、および 2) 世界の状態からニューラル ネットワーク入力を生成する観測プロセスを通じて、仕様を提供します。有限数のタイルで状態空間と入力空間をタイル張りし、状態タイルからグラウンド トゥルース境界を取得し、入力タイルからネットワーク出力境界を取得してから、グラウンド トゥルースとネットワーク出力境界を比較すると、任意のネットワーク出力誤差の上限が得られます。関心のある入力。提示されたフレームワークは、不正な入力、つまり状態空間と観測プロセスによって定義されたターゲット入力空間に含まれていない (または近くにない) 入力 (ニューラル ネットワークはそれらに対して動作するように設計されていません) の検出も可能にします。保証がない場合にフラグを立てることができます。 2 つのケース スタディの結果は、ターゲット入力空間全体でエラー境界を検証する手法の能力を強調し、エラー境界が状態と入力空間でどのように変化するかを示しています。
We present a novel framework for specifying and verifying correctness globally for neural networks on perception tasks. Most previous works on neural network verification for perception tasks focus on robustness verification. Unlike robustness verification, which aims to verify that the prediction of a network is stable in some local regions around labelled points, our framework provides a way to specify correctness globally in the whole target input space and verify that the network is correct for all target inputs (or find the regions where the network is not correct). We provide a specification through 1) a state space consisting of all relevant states of the world and 2) an observation process that produces neural network inputs from the states of the world. Tiling the state and input spaces with a finite number of tiles, obtaining ground truth bounds from the state tiles and network output bounds from the input tiles, then comparing the ground truth and network output bounds delivers an upper bound on the network output error for any inputs of interest. The presented framework also enables detecting illegal inputs -- inputs that are not contained in (or close to) the target input space as defined by the state space and observation process (the neural network is not designed to work on them), so that we can flag when we don't have guarantees. Results from two case studies highlight the ability of our technique to verify error bounds over the whole target input space and show how the error bounds vary over the state and input spaces.
updated: Tue Aug 23 2022 19:01:30 GMT+0000 (UTC)
published: Mon Jun 03 2019 19:13:24 GMT+0000 (UTC)
参考文献 (このサイトで利用可能なもの) / References (only if available on this site)
被参照文献 (このサイトで利用可能なものを新しい順に) / Citations (only if available on this site, in order of most recent)アソシエイト