論文の概要: Provably Bounding Neural Network Preimages
- arxiv url: http://arxiv.org/abs/2302.01404v1
- Date: Thu, 2 Feb 2023 20:34:45 GMT
- ステータス: 処理完了
- システム内更新日: 2023-02-06 18:15:22.699996
- Title: Provably Bounding Neural Network Preimages
- Title(参考訳): ニューラルネットワークの予兆を想像する
- Authors: Suhas Kotha, Christopher Brix, Zico Kolter, Krishnamurthy (Dj)
Dvijotham, Huan Zhang
- Abstract要約: 本稿では,ニューラルネットワークの線形制約された出力セットの事前画像上の特性を検証するための,最初の効率的な境界伝搬アルゴリズム INVPROP を提案する。
その結果、ある設定では、以前の作業の2500倍以上の厳密なオーバー近似が見つかることがわかった。
- 参考スコア(独自算出の注目度): 12.266222842824957
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Most work on the formal verification of neural networks has focused on
bounding forward images of neural networks, i.e., the set of outputs of a
neural network 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, i.e, over-approximating the
set of inputs that lead to certain outputs. In this work, we present the first
efficient bound propagation algorithm, INVPROP, for verifying properties over
the preimage of a linearly constrained output set of a neural network, which
can be combined with branch-and-bound to achieve completeness. Our efficient
algorithm allows multiple passes of intermediate bound refinements, which are
crucial for tight inverse verification because the bounds of an intermediate
layer depend on relaxations both before and after this layer. We demonstrate
our algorithm on applications related to quantifying safe control regions for a
dynamical system and detecting out-of-distribution inputs to a neural network.
Our results show that in certain settings, we can find over-approximations that
are over 2500 times tighter than prior work while being 2.5 times faster on the
same hardware.
- Abstract(参考訳): ニューラルネットワークの形式的検証に関するほとんどの研究は、ニューラルネットワークの前方画像の境界、すなわち、与えられた入力のセットに対応するニューラルネットワークの出力のセット(例えば、名目入力の有界摂動)に焦点を当てている。
しかし、ニューラルネットワーク検証の多くのユースケースは、逆問題、すなわち特定の出力につながる入力の集合を過度に近似することを必要とする。
本研究では,ニューラルネットワークの線形制約された出力セットのプリイメージ上の特性を検証するための,最初の効率的な境界伝搬アルゴリズム INVPROP を提案する。
提案手法では,中間層の境界が前後の緩和に依存するため,中間境界細分化の複数の通過が可能であり,密な逆検証に不可欠である。
本稿では,動的システムのための安全な制御領域の定量化と,ニューラルネットワークへの分布外入力の検出に関するアプリケーションに関するアルゴリズムを実証する。
その結果、特定の設定で、同じハードウェア上で2.5倍高速で、以前の作業の2500倍以上の厳密なオーバー近似を見つけることができた。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。