論文の概要: Provably Bounding Neural Network Preimages
- arxiv url: http://arxiv.org/abs/2302.01404v4
- Date: Sun, 17 Mar 2024 17:36:02 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-20 06:48:15.881035
- Title: Provably Bounding Neural Network Preimages
- Title(参考訳): ニューラルネットワークの予兆を想像する(動画あり)
- Authors: Suhas Kotha, Christopher Brix, Zico Kolter, Krishnamurthy Dvijotham, Huan Zhang,
- Abstract要約: InVPROPアルゴリズムは線形に制約された出力セットの事前画像上の特性を検証する。
他のアプローチとは対照的に、効率的なアルゴリズムはGPU加速であり、線形プログラミング解決器を必要としない。
その結果, 従来よりも2.5倍速く, 2500倍以上の過近似が得られていることがわかった。
- 参考スコア(独自算出の注目度): 18.810882386083655
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract(参考訳): ニューラルネットワークの形式的検証に関するほとんどの研究は、与えられた入力の集合に対応する出力の集合(例えば、名目入力の有界摂動)の有界化に焦点を当てている。
しかし、ニューラルネットワーク検証の多くのユースケースでは、逆問題を解決するか、特定の出力につながる入力の集合を過度に近似する必要がある。
InVPROPアルゴリズムは線形に制約された出力セットのプリイメージ上の特性を検証し、分岐とバウンドを組み合わせて精度を向上させる。
他のアプローチとは対照的に、効率的なアルゴリズムはGPU加速であり、線形プログラミング解決器を必要としない。
本稿では,動的システムの安全制御領域を後方到達性解析により同定し,逆方向のロバスト性を検証し,ニューラルネットワークへのアウト・オブ・ディストリビューションの入力を検出するアルゴリズムを実証する。
その結果, 従来よりも2.5倍速く, 2500倍以上の過近似が得られていることがわかった。
出力制約によるロバスト性検証を強化することで、VNN-COMP 2023の167kのニューロンを含む複数のベンチマークにおいて、従来よりも多くの特性を一貫して検証する。
私たちのアルゴリズムは$\alpha,\!
https://abcrown.orgで入手できる。
関連論文リスト
- PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks [30.701422594374456]
本稿では,任意の多面体出力集合のアンダー・アンド・オーバー近似を生成する事前抽象化のためのフレームワークを提案する。
提案手法を様々なタスクで評価し,高インプット次元画像分類タスクに対する効率とスケーラビリティの大幅な向上を示す。
論文 参考訳(メタデータ) (2024-08-17T17:24:47Z) - Tight Verification of Probabilistic Robustness in Bayesian Neural
Networks [17.499817915644467]
ベイズニューラルネットワーク(BNN)の確率論的ロバスト性に関する厳密な保証を計算するための2つのアルゴリズムを導入する。
提案アルゴリズムは,反復的拡張とネットワークの勾配を用いて,パラメータの空間を安全に探索する。
アルゴリズムがSoAよりも厳密なバウンダリを計算できることの証明に加えて、標準ベンチマーク上でのSoAに対するアルゴリズムの評価も行っています。
論文 参考訳(メタデータ) (2024-01-21T23:41:32Z) - Provable Preimage Under-Approximation for Neural Networks (Full Version) [27.519993407376862]
ニューラルネットワークに対する任意のポリヘドロン出力セットの事前像の記号的アンダー近似を生成するための効率的な時空アルゴリズムを提案する。
実験により,本手法の有効性を,高次元MNIST分類タスクを含む領域にわたって検証した。
我々は,形式的な保証を提供するために,ポリトープ表現の不整合和を利用する,前者のための健全で完全なアルゴリズムを提案する。
論文 参考訳(メタデータ) (2023-05-05T16:55:27Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - Towards Better Out-of-Distribution Generalization of Neural Algorithmic
Reasoning Tasks [51.8723187709964]
ニューラルネットワーク推論タスクのOOD一般化について検討する。
目標は、ディープニューラルネットワークを使用して入出力ペアからアルゴリズムを学ぶことである。
論文 参考訳(メタデータ) (2022-11-01T18:33:20Z) - Robust Training and Verification of Implicit Neural Networks: A
Non-Euclidean Contractive Approach [64.23331120621118]
本稿では,暗黙的ニューラルネットワークのトレーニングとロバスト性検証のための理論的および計算的枠組みを提案する。
組込みネットワークを導入し、組込みネットワークを用いて、元のネットワークの到達可能な集合の超近似として$ell_infty$-normボックスを提供することを示す。
MNISTデータセット上で暗黙的なニューラルネットワークをトレーニングするためにアルゴリズムを適用し、我々のモデルの堅牢性と、文献における既存のアプローチを通じてトレーニングされたモデルを比較する。
論文 参考訳(メタデータ) (2022-08-08T03:13:24Z) - A Mixed Integer Programming Approach for Verifying Properties of
Binarized Neural Networks [44.44006029119672]
BNN検証のための混合整数計画法を提案する。
我々は,MNISTデータセットと航空機衝突回避制御器を用いて訓練したBNNの特性を検証することによって,我々のアプローチを実証する。
論文 参考訳(メタデータ) (2022-03-11T01:11:29Z) - Robustification of Online Graph Exploration Methods [59.50307752165016]
我々は、古典的で有名なオンライングラフ探索問題の学習強化版について研究する。
本稿では,予測をよく知られたNearest Neighbor(NN)アルゴリズムに自然に統合するアルゴリズムを提案する。
論文 参考訳(メタデータ) (2021-12-10T10:02:31Z) - Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
本稿では,効率的な分岐戦略を設計するための新しい機械学習フレームワークを提案する。
グラフ入力として検証したいネットワークを直接扱う2つのグラフニューラルネットワーク(GNN)を学習する。
我々のGNNモデルは、より大きな未確認ネットワーク上での厳しい特性に対してよく一般化されていることを示す。
論文 参考訳(メタデータ) (2021-07-27T14:42:57Z) - Enabling certification of verification-agnostic networks via
memory-efficient semidefinite programming [97.40955121478716]
本稿では,ネットワークアクティベーションの総数にのみ線形なメモリを必要とする一階二重SDPアルゴリズムを提案する。
L-inf の精度は 1% から 88% ,6% から 40% に改善した。
また,変分オートエンコーダの復号器に対する2次安定性仕様の厳密な検証を行った。
論文 参考訳(メタデータ) (2020-10-22T12:32:29Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
論文 参考訳(メタデータ) (2020-02-24T17:55:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。