論文の概要: Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks

• arxiv url: http://arxiv.org/abs/2207.00759v1
• Date: Sat, 2 Jul 2022 07:04:20 GMT
• ステータス: 処理完了
• システム内更新日: 2022-07-05 16:19:34.041935
• Title: Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks
• Title（参考訳）: 抽象化と洗練:ニューラルネットワークのスケーラブルで正確な検証に向けて
• Authors: Jiaxiang Liu, Yunhan Xing, Xiaomu Shi, Fu Song, Zhiwu Xu, Zhong Ming
• Abstract要約: ディープニューラルネットワーク(DNN)の実践はますます進んでいるが、ロバストさの欠如により、安全クリティカルなドメインへの応用が妨げられている。 本稿では,スケーラブルで正確なDNN検証のための新しい抽象化・リファインメント手法を提案する。
• 参考スコア（独自算出の注目度）: 9.85360493553261
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, they are limited in scalability and accuracy. In this paper, we present a novel abstraction-refinement approach for scalable and exact DNN verification. Specifically, we propose a novel abstraction to break down the size of DNNs by over-approximation. The result of verifying the abstract DNN is always conclusive if no spurious counterexample is reported. To eliminate spurious counterexamples introduced by abstraction, we propose a novel counterexample-guided refinement that refines the abstract DNN to exclude a given spurious counterexample while still over-approximating the original one. Our approach is orthogonal to and can be integrated with many existing verification techniques. For demonstration, we implement our approach using two promising and exact tools Marabou and Planet as the underlying verification engines, and evaluate on widely-used benchmarks ACAS Xu, MNIST and CIFAR-10. The results show that our approach can boost their performance by solving more problems and reducing up to 86.3% and 78.0% verification time, respectively. Compared to the most relevant abstraction-refinement approach, our approach is 11.6-26.6 times faster.
• Abstract（参考訳）: 新しいプログラミングパラダイムとして、ディープニューラルネットワーク(DNN)が実用化されつつあるが、ロバストさの欠如により、安全クリティカルなドメインでの応用が妨げられている。 正式な保証でDNNを検証する技術はあるが、スケーラビリティと精度に制限がある。 本稿では,スケーラブルかつ高精度なDNN検証のための新しい抽象化補正手法を提案する。 具体的には、過剰近似によりDNNのサイズを分解する新しい抽象化を提案する。 急激な反例が報告されていない場合、抽象的なDNNを検証する結果は、常に決定される。 そこで本研究では,抽象的なDNNを改良し,元のDNNを過度に近似しながら,与えられた急激な反例を除外する,新しい反例誘導改良法を提案する。 我々のアプローチは直交しており、既存の多くの検証技術と統合することができる。 実証のために,実証エンジンとしてMarabouとPlanetの2つの有望かつ正確なツールを用いて本手法を実装し,広く使用されているACAS Xu,MNIST,CIFAR-10の評価を行った。 提案手法は, より多くの問題を解くことにより, それぞれ86.3%, 78.0%の検証時間を短縮することで, 性能を向上できることを示す。 最も関連する抽象再定義アプローチと比較して、我々のアプローチは11.6-26.6倍高速です。

関連論文リスト

• Theoretically Achieving Continuous Representation of Oriented Bounding Boxes [64.15627958879053]
  本論文は,オブジェクト指向境界ボックス表現における不連続性を完全に解決しようとする試みである。 本研究では,既存の検出器に容易に統合可能なCOBB(Continuous OBB)という新しい表現法を提案する。 OOD評価のためのオープンソースのディープラーニングフレームワークJittorの検出ツールボックスJDetをベースとした,モジュール化されたベンチマークを開発した。
  論文  参考訳（メタデータ） (2024-02-29T09:27:40Z)
• 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)
• Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training [14.787056022080625]
  本稿では, 到達可能性解析における過剰近似DNNの欠如を回避するための, 抽象的アプローチを提案する。 我々は、実数をトレーニングの間隔に抽象化する抽象層を挿入することで、従来のDNNを拡張した。 我々は、DNN制御システムに対する最初のブラックボックス到達可能性分析手法を考案し、訓練されたDNNは抽象状態に対するアクションのためのブラックボックスオラクルとしてのみクエリされる。
  論文  参考訳（メタデータ） (2022-11-21T00:11:50Z)
• Tighter Abstract Queries in Neural Network Verification [0.0]
  CEGARETTEは,システムとプロパティを同時に抽象化し,洗練する新しい検証機構である。 私たちの結果は有望であり、複数のベンチマークよりもパフォーマンスが大幅に向上したことを証明しています。
  論文  参考訳（メタデータ） (2022-10-23T22:18:35Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。 この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。 本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-06-08T04:09:13Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。 INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。 提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
  論文  参考訳（メタデータ） (2022-04-01T03:31:27Z)
• Online Limited Memory Neural-Linear Bandits with Likelihood Matching [53.18698496031658]
  本研究では,探索学習と表現学習の両方が重要な役割を果たす課題を解決するために,ニューラルネットワークの帯域について検討する。 破滅的な忘れ込みに対して耐性があり、完全にオンラインである可能性の高いマッチングアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2021-02-07T14:19:07Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• Accelerating Robustness Verification of Deep Neural Networks Guided by Target Labels [8.9960048245668]
  ディープニューラルネットワーク(DNN)は、自律運転や医療診断など、多くの安全クリティカルなアプリケーションの主要なコンポーネントとなっている。 DNNは、入力に対する小さな摂動が誤った予測をもたらすような敵の例に感受性があるため、ロバスト性に悩まされる。 本稿では,ロバスト性検証を目標ラベルで導くことによって,ロバスト性検証手法を高速化する手法を提案する。
  論文  参考訳（メタデータ） (2020-07-16T00:51:52Z)

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

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