論文の概要: Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
- arxiv url: http://arxiv.org/abs/2505.00963v1
- Date: Fri, 02 May 2025 02:41:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-05 17:21:19.885142
- Title: Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
- Title（参考訳）: ニューラルネットワーク検証のための適応的分岐境界木探索
- Authors: Kota Fukuda, Guanqin Zhang, Zhenya Zhang, Yulei Sui, Jianjun Zhao,
- Abstract要約: ABONNはモンテカルロ木探索(MCTS)方式でBaBのサブプロブレム空間を適応的に探索する。
ABONNは、MNISTで最大$15.2times、CIFAR-10で$24.7timesのスピードアップを実証している。
- 参考スコア（独自算出の注目度）: 8.733719614108102
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the \emph{importance} of different sub-problems. To bridge this gap, we first introduce a notion of ``importance'' that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the ``importance'' of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonly-used datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to $15.2\times$ on MNIST and $24.7\times$ on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.
- Abstract（参考訳）: フォーマル検証は、ニューラルネットワークの品質を確実に保証する厳格なアプローチであり、これまでは、ブランチ・アンド・バウンド(BaB)は、問題を必要に応じて分割して検証を行い、オフ・ザ・シェルフ検証をサブプロブレムに適用してパフォーマンスを向上させる、最先端の技術である。
しかし、既存のBaBは、異なるサブプロブレムの \emph{importance} を無視した部分プロブレムの空間を探索する素な方法のため、効率的ではないかもしれない。
このギャップを埋めるために、我々はまず、サブプロブレムでカウンターサンプルが見つかる確率を反映した 'importance' の概念を導入し、次にモンテカルロ木探索(MCTS)スタイルでBaBのサブプロブレム空間を適応的に探索する ABONN と呼ばれる新しい検証手法を考案する。
この探索は、異なるサブプロブレムの「重要」によって導かれるため、反例を見つけやすいサブプロブレムが好まれる。
反例を見つけるとすぐに終了するが、すべてのサブプロブレムを訪問した後でも問題を確認することができる。
我々は、一般的なデータセットとニューラルネットワークモデルから52の検証問題でABONNを評価し、ベースラインアプローチとして最先端の検証器と比較した。
ABONNはMNISTで最大15.2\times$、CIFAR-10で24.7\times$のスピードアップを実証している。
さらに,ABONNの性能に及ぼすハイパーパラメータの影響と適応木探索の有効性について検討した。
関連論文リスト
- Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples [52.564617070814485]
本稿では,NN検証のための音響性ベンチマークを提案する。
私たちのベンチマークには、意図的に挿入された反例のインスタンスが含まれています。
我々のベンチマークでは、最先端のNN検証器のバグと合成バグの識別に成功している。
論文 参考訳（メタデータ） (2024-12-04T09:24:33Z) - A DPLL(T) Framework for Verifying Deep Neural Networks [9.422860826278788]
人手によるソフトウェアと同じように、Deep Neural Networks(DNN)にもバグがあり、攻撃できる。
我々は,現代のSMTソルバで広く使われているDPLL(T)アルゴリズムに適応する新しい検証手法であるNeuralSATを紹介する。
論文 参考訳（メタデータ） (2023-07-17T18:49:46Z) - Deep Graph Neural Networks via Posteriori-Sampling-based Node-Adaptive Residual Module [65.81781176362848]
グラフニューラルネットワーク(GNN)は、近隣情報収集を通じてグラフ構造化データから学習することができる。
レイヤーの数が増えるにつれて、ノード表現は区別不能になり、オーバー・スムーシング(over-smoothing)と呼ばれる。
我々は,textbfPosterior-Sampling-based, Node-distinguish Residual Module (PSNR)を提案する。
論文 参考訳（メタデータ） (2023-05-09T12:03:42Z) - OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep
Neural Networks [7.797299214812479]
Occlusionは、ディープニューラルネットワーク(DNN)に対する一般的かつ容易に実現可能なセマンティック摂動である
DNNを騙していくつかのセグメントを隠蔽することで入力画像を誤分類し、おそらく深刻なエラーを引き起こす可能性がある。
DNNの既存のロバスト性検証アプローチは、非意味的な摂動に重点を置いている。
論文 参考訳（メタデータ） (2023-01-27T18:54:00Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳（メタデータ） (2023-01-17T18:32:01Z) - The Devil is in the Conflict: Disentangled Information Graph Neural
Networks for Fraud Detection [17.254383007779616]
性能劣化は主にトポロジと属性の矛盾に起因すると我々は主張する。
注意機構を用いて2つの視点を適応的に融合する簡易かつ効果的な手法を提案する。
我々のモデルは、実世界の不正検出データセットで最先端のベースラインを大幅に上回ることができる。
論文 参考訳（メタデータ） (2022-10-22T08:21:49Z) - Revisiting Heterophily For Graph Neural Networks [42.41238892727136]
グラフニューラルネットワーク(GNN)は、関係帰納バイアスに基づくグラフ構造を用いて基本ニューラルネットワーク(NN)を拡張する(ホモフィリー仮定)
最近の研究は、NNと比較してパフォーマンスが不十分な、非自明なデータセットのセットを特定している。
論文 参考訳（メタデータ） (2022-10-14T08:00:26Z) - Abstraction and Refinement: Towards Scalable and Exact Verification of
Neural Networks [9.85360493553261]
ディープニューラルネットワーク(DNN)の実践はますます進んでいるが、ロバストさの欠如により、安全クリティカルなドメインへの応用が妨げられている。
本稿では,スケーラブルで正確なDNN検証のための新しい抽象化・リファインメント手法を提案する。
論文 参考訳（メタデータ） (2022-07-02T07:04:20Z) - Online Limited Memory Neural-Linear Bandits with Likelihood Matching [53.18698496031658]
本研究では,探索学習と表現学習の両方が重要な役割を果たす課題を解決するために,ニューラルネットワークの帯域について検討する。
破滅的な忘れ込みに対して耐性があり、完全にオンラインである可能性の高いマッチングアルゴリズムを提案する。
論文 参考訳（メタデータ） (2021-02-07T14:19:07Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳（メタデータ） (2020-10-07T08:19:48Z) - Exact posterior distributions of wide Bayesian neural networks [51.20413322972014]
正確なBNN後方収束は、前者のGP限界によって誘導されるものと(弱く)収束することを示す。
実験的な検証のために、リジェクションサンプリングにより、小さなデータセット上で有限BNNから正確なサンプルを生成する方法を示す。
論文 参考訳（メタデータ） (2020-06-18T13:57:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。