論文の概要: Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

• arxiv url: http://arxiv.org/abs/2302.06455v1
• Date: Fri, 10 Feb 2023 04:31:28 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-14 15:03:28.199928
• Title: Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks
• Title（参考訳）: 深部ニューラルネットワーク検証のための増分満足度モード理論
• Authors: Pengfei Yang, Zhiming Chi, Zongxin Liu, Mengyu Zhao, Cheng-Chao Huang, Shaowei Cai, and Lijun Zhang
• Abstract要約: 本稿ではReluplexフレームワークに基づく漸進的満足度変調理論(SMT)を提案する。 我々は,DeepIncと呼ばれる漸進的な解法としてアルゴリズムを実装し,実験結果から,ほとんどの場合,DeepIncの方が効率的であることが示された。
• 参考スコア（独自算出の注目度）: 22.015676101940077
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, we propose the incremental DNN verification problem, which asks whether a safety property still holds after the DNN is modified. To solve the problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We simulate the most important features of the configurations that infers the verification result of the searching branches in the old solving procedure (with respect to the original network), and heuristically check whether the proofs are still valid for the modified DNN. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases. For the cases that the property holds both before and after modification, the acceleration can be faster by several orders of magnitude, showing that DeepInc is outstanding in incrementally searching for counterexamples. Moreover, based on the framework, we propose the multi-objective DNN repair problem and give an algorithm based on our incremental SMT solving algorithm. Our repair method preserves more potential safety properties on the repaired DNNs compared with state-of-the-art.
• Abstract（参考訳）: 制約解決はディープニューラルネットワーク(DNN)の基本的な検証方法である。 AI安全性の分野では、DNNは、その構造と、その修復や攻撃のパラメータを変更することができる。 そこで本研究では,DNN修正後の安全性が保たれているかどうかを問う,段階的なDNN検証問題を提案する。 この問題を解決するために、Reluplexフレームワークに基づく漸進的満足度変調理論(SMT)アルゴリズムを提案する。 従来の解法(元のネットワークに関して)における探索枝の検証結果を推測する構成の最も重要な特徴をシミュレートし、修正されたDNNに対して証明がまだ有効かどうかをヒューリスティックに検証する。 我々は,DeepIncと呼ばれる漸進的な解法としてアルゴリズムを実装し,実験結果から,ほとんどの場合,DeepIncの方が効率的であることが示された。 プロパティが修正前と修正後の両方を保持する場合、加速は数桁の速度で高速化され、DeepIncはインクリメンタルに反例を探すのに優れていることを示す。 さらに,本フレームワークをベースとして,多目的DNN修復問題を提案し,インクリメンタルSMT解法に基づくアルゴリズムを提案する。 本手法は, 修復済みDNNの安全性を, 最先端のDNNと比較して向上させる。

関連論文リスト

• A DPLL(T) Framework for Verifying Deep Neural Networks [9.422860826278788]
  人手によるソフトウェアと同じように、Deep Neural Networks(DNN)にもバグがあり、攻撃できる。 我々は,現代のSMTソルバで広く使われているDPLL(T)アルゴリズムに適応する新しい検証手法であるNeuralSATを紹介する。
  論文  参考訳（メタデータ） (2023-07-17T18:49:46Z)
• Incremental Verification of Neural Networks [3.9661031279983896]
  本稿では,新しい理論,データ構造,アルゴリズムの設計に基づく,インクリメンタルかつ完全なDNN検証のための新しい汎用フレームワークを提案する。 我々の貢献はIVANというツールに実装され、MNISTとCIFAR10の分類に挑戦する上での全体的な幾何平均スピードアップの2.4倍、最先端のベースライン上でのACAS-XU分類器の幾何平均スピードアップの3.8倍となる。
  論文  参考訳（メタデータ） (2023-04-04T15:28:22Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Automated Repair of Neural Networks [0.26651200086513094]
  安全でないNNの安全仕様を修復するためのフレームワークを提案する。 提案手法では,重み値のいくつかを修正して,新しい安全なNN表現を探索することができる。 我々は,提案するフレームワークが安全なNNを実現する能力を示す広範な実験を行った。
  論文  参考訳（メタデータ） (2022-07-17T12:42:24Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。 INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。 提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
  論文  参考訳（メタデータ） (2022-04-01T03:31:27Z)
• Provable Repair of Deep Neural Networks [8.55884254206878]
  ディープニューラルネットワーク(Deep Neural Networks, DNN)は、過去10年間で人気を博し、航空機の衝突回避などの安全上重要な領域で使われている。 本稿では,安全でない動作が見つかるとDNNの修正に対処する。 与えられた仕様を満たす新しいネットワークN'を構築するためにネットワークNを修復する問題である実証可能な修復問題を紹介します。
  論文  参考訳（メタデータ） (2021-04-09T15:03:53Z)
• 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)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。