On Preimage Approximation for Neural Networks

要約

タイトル：ニューラルネットワークのプレイメージ近似について
要約：
– ニューラルネットワークの検証は、主にローカルな堅牢性特性に焦点を当てて行われています。
– しかしながら、ある特性が全体的に入力領域全体にわたって成立するかどうか、もしくは、その特性がどの程度の入力に対して成立するかどうかを把握することは重要です。
– 正確なプレイメージ生成は、ニューラルネットワークの等価な表現を生成し、このような（定量的な）グローバルな堅牢性検証に役立つことができますが、規模に応じて扱うことができません。
– 本研究では、線形リラックスに基づくシンボル的なプレイメージのアンダーアプロキシメーションを生成するための効率的で実用的なアルゴリズムを提案しています。
– アルゴリズムは、入力領域をサブリージョンに分割し、ニューラルネットワークのリラックス境界がよりタイトになる領域を優先的に分割し、体積近似誤差を反復的に最小化します。
– 加えて、サンプリングと微分可能な近似を用いて、分割する領域を優先的に決定し、リラックスのパラメータを最適化することで、より速く改善され、よりコンパクトなアンダーアプロキシメーションを生成することができます。
– 評価結果は、本手法が正確な方法よりも遥かに高速にプレイメージ近似を生成することができることを示しており、正確なプレイメージ生成が不可能なニューラルネットワークコントローラにスケールします。
– 加えて、本研究のアプローチを、定量的なグローバル検証に適用することも示されました。

要約(オリジナル)

Neural network verification mainly focuses on local robustness properties. However, often it is important to know whether a given property holds globally for the whole input domain, and if not then for what proportion of the input the property is true. While exact preimage generation can construct an equivalent representation of neural networks that can aid such (quantitative) global robustness verification, it is intractable at scale. In this work, we propose an efficient and practical anytime algorithm for generating symbolic under-approximations of the preimage of neural networks based on linear relaxation. Our algorithm iteratively minimizes the volume approximation error by partitioning the input region into subregions, where the neural network relaxation bounds become tighter. We further employ sampling and differentiable approximations to the volume in order to prioritize regions to split and optimize the parameters of the relaxation, leading to faster improvement and more compact under-approximations. Evaluation results demonstrate that our approach is able to generate preimage approximations significantly faster than exact methods and scales to neural network controllers for which exact preimage generation is intractable. We also demonstrate an application of our approach to quantitative global verification.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI