要約
ニューラル ネットワークの形式的検証に関するほとんどの研究は、特定の入力セットに対応する出力セットの境界を設定することに焦点を当ててきました (たとえば、公称入力の境界のある摂動など)。
ただし、ニューラル ネットワーク検証の多くの使用例では、逆問題を解決するか、特定の出力につながる入力セットを過剰近似する必要があります。
線形制約された出力セットのプリイメージ上のプロパティを検証するための INVPROP アルゴリズムを紹介します。このアルゴリズムは、分岐限定と組み合わせて精度を高めることができます。
他のアプローチとは対照的に、私たちの効率的なアルゴリズムは GPU で高速化され、線形計画法ソルバーを必要としません。
私たちは、後方到達可能性分析を通じて動的システムの安全な制御領域を特定し、敵対的な堅牢性を検証し、ニューラル ネットワークへの分布外入力を検出するためのアルゴリズムを実証します。
私たちの結果は、特定の設定では、2.5 倍高速でありながら、以前の研究よりも 2500 倍以上厳密な過近似が見られることを示しています。
出力制約による堅牢性検証を強化することで、VNN-COMP 2023 の 167,000 ニューロンを備えた大規模モデルなど、複数のベンチマークで以前の最先端のものよりも多くのプロパティを一貫して検証します。私たちのアルゴリズムは $\alpha に組み込まれています。
、\!\beta$-CROWN 検証ツール、https://abcrown.org で入手可能。
要約(オリジナル)
Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the $\alpha,\!\beta$-CROWN verifier, available at https://abcrown.org.
arxiv情報
著者 | Suhas Kotha,Christopher Brix,Zico Kolter,Krishnamurthy Dvijotham,Huan Zhang |
発行日 | 2023-12-08 17:14:13+00:00 |
arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google