論文の概要: A DPLL(T) Framework for Verifying Deep Neural Networks
- arxiv url: http://arxiv.org/abs/2307.10266v3
- Date: Fri, 19 Jan 2024 23:51:05 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-23 21:14:55.633799
- Title: A DPLL(T) Framework for Verifying Deep Neural Networks
- Title(参考訳): 深部ニューラルネットワーク検証のためのDPLL(T)フレームワーク
- Authors: Hai Duong, ThanhVu Nguyen, Matthew Dwyer
- Abstract要約: 人手によるソフトウェアと同じように、Deep Neural Networks(DNN)にもバグがあり、攻撃できる。
我々は,現代のSMTソルバで広く使われているDPLL(T)アルゴリズムに適応する新しい検証手法であるNeuralSATを紹介する。
- 参考スコア(独自算出の注目度): 9.422860826278788
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deep Neural Networks (DNNs) have emerged as an effective approach to tackling
real-world problems. However, like human-written software, DNNs can have bugs
and can be attacked. To address this, research has explored a wide-range of
algorithmic approaches to verify DNN behavior. In this work, we introduce
NeuralSAT, a new verification approach that adapts the widely-used DPLL(T)
algorithm used in modern SMT solvers. A key feature of SMT solvers is the use
of conflict clause learning and search restart to scale verification. Unlike
prior DNN verification approaches, NeuralSAT combines an abstraction-based
deductive theory solver with clause learning and an evaluation clearly
demonstrates the benefits of the approach on a set of challenging verification
benchmarks.
- Abstract(参考訳): Deep Neural Networks (DNN)は、現実世界の問題を解決する効果的なアプローチとして登場した。
しかし、人間書きのソフトウェアのように、DNNにはバグがあり、攻撃される可能性がある。
これを解決するために、DNNの動作を検証するアルゴリズム的なアプローチを幅広く検討した。
本研究では,現代のSMTソルバで広く使われているDPLL(T)アルゴリズムに適応する新しい検証手法であるNeuralSATを紹介する。
SMTソルバの重要な特徴は、コンフリクト節学習と検索再起動をスケール検証に利用することである。
従来のDNN検証アプローチとは異なり、NeuralSATでは、抽象に基づく推論理論の解法と節学習を組み合わせることで、一連の挑戦的な検証ベンチマークに対するアプローチのメリットを明確に示す。
関連論文リスト
- Harnessing Neuron Stability to Improve DNN Verification [42.65507402735545]
我々は最近提案されたDPLLベースの制約DNN検証手法の拡張であるVeriStableを提案する。
完全接続型フィードネットワーク(FNN)、畳み込み型ニューラルネットワーク(CNN)、残留型ネットワーク(ResNet)など、さまざまな課題のあるベンチマークにおいてVeriStableの有効性を評価する。
予備的な結果は、VeriStableは、VNN-COMPの第1および第2のパフォーマーである$alpha$-$beta$-CROWNやMN-BaBなど、最先端の検証ツールよりも優れていることを示している。
論文 参考訳(メタデータ) (2024-01-19T23:48:04Z) - Incremental Satisfiability Modulo Theory for Verification of Deep Neural
Networks [22.015676101940077]
本稿ではReluplexフレームワークに基づく漸進的満足度変調理論(SMT)を提案する。
我々は,DeepIncと呼ばれる漸進的な解法としてアルゴリズムを実装し,実験結果から,ほとんどの場合,DeepIncの方が効率的であることが示された。
論文 参考訳(メタデータ) (2023-02-10T04:31:28Z) - OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep
Neural Networks [7.797299214812479]
Occlusionは、ディープニューラルネットワーク(DNN)に対する一般的かつ容易に実現可能なセマンティック摂動である
DNNを騙していくつかのセグメントを隠蔽することで入力画像を誤分類し、おそらく深刻なエラーを引き起こす可能性がある。
DNNの既存のロバスト性検証アプローチは、非意味的な摂動に重点を置いている。
論文 参考訳(メタデータ) (2023-01-27T18:54:00Z) - Nearest Neighbor Knowledge Distillation for Neural Machine Translation [50.0624778757462]
k-nearest-neighbor machine translation (NN-MT) は機械翻訳タスクにおける最先端の結果の多くを達成している。
NN-KDはベースNMTモデルをトレーニングし、NNの知識を直接学習する。
論文 参考訳(メタデータ) (2022-05-01T14:30:49Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳(メタデータ) (2022-04-01T03:31:27Z) - A Mixed Integer Programming Approach for Verifying Properties of
Binarized Neural Networks [44.44006029119672]
BNN検証のための混合整数計画法を提案する。
我々は,MNISTデータセットと航空機衝突回避制御器を用いて訓練したBNNの特性を検証することによって,我々のアプローチを実証する。
論文 参考訳(メタデータ) (2022-03-11T01:11:29Z) - Pruning and Slicing Neural Networks using Formal Verification [0.2538209532048866]
ディープニューラルネットワーク(DNN)は、様々なコンピュータシステムにおいてますます重要な役割を担っている。
これらのネットワークを作成するために、エンジニアは通常、望ましいトポロジを指定し、自動トレーニングアルゴリズムを使用してネットワークの重みを選択する。
本稿では,近年のDNN検証の進歩を活用して,この問題に対処することを提案する。
論文 参考訳(メタデータ) (2021-05-28T07:53:50Z) - Online Limited Memory Neural-Linear Bandits with Likelihood Matching [53.18698496031658]
本研究では,探索学習と表現学習の両方が重要な役割を果たす課題を解決するために,ニューラルネットワークの帯域について検討する。
破滅的な忘れ込みに対して耐性があり、完全にオンラインである可能性の高いマッチングアルゴリズムを提案する。
論文 参考訳(メタデータ) (2021-02-07T14:19:07Z) - Progressive Tandem Learning for Pattern Recognition with Deep Spiking
Neural Networks [80.15411508088522]
スパイキングニューラルネットワーク(SNN)は、低レイテンシと高い計算効率のために、従来の人工知能ニューラルネットワーク(ANN)よりも優位性を示している。
高速かつ効率的なパターン認識のための新しいANN-to-SNN変換およびレイヤワイズ学習フレームワークを提案する。
論文 参考訳(メタデータ) (2020-07-02T15:38:44Z) - Boosting Deep Neural Networks with Geometrical Prior Knowledge: A Survey [77.99182201815763]
ディープニューラルネットワーク(DNN)は多くの異なる問題設定において最先端の結果を達成する。
DNNはしばしばブラックボックスシステムとして扱われ、評価と検証が複雑になる。
コンピュータビジョンタスクにおける畳み込みニューラルネットワーク(CNN)の成功に触発された、有望な分野のひとつは、対称幾何学的変換に関する知識を取り入れることである。
論文 参考訳(メタデータ) (2020-06-30T14:56:05Z) - GraN: An Efficient Gradient-Norm Based Detector for Adversarial and
Misclassified Examples [77.99182201815763]
ディープニューラルネットワーク(DNN)は、敵対的な例やその他のデータ摂動に対して脆弱である。
GraNは、どのDNNにも容易に適応できる時間およびパラメータ効率の手法である。
GraNは多くの問題セットで最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2020-04-20T10:09:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。