論文の概要: Verifying Quantized Neural Networks using SMT-Based Model Checking
- arxiv url: http://arxiv.org/abs/2106.05997v1
- Date: Thu, 10 Jun 2021 18:27:45 GMT
- ステータス: 処理完了
- システム内更新日: 2021-06-14 14:02:18.198807
- Title: Verifying Quantized Neural Networks using SMT-Based Model Checking
- Title（参考訳）: SMTモデル検査による量子ニューラルネットワークの検証
- Authors: Luiz Sena, Xidan Song, Erickson Alves, Iury Bessa, Edoardo Manino,
Lucas Cordeiro
- Abstract要約: インクリメンタルモデルチェック(IMC)と満足度変調理論(SMT)を用いたシンボリック検証フレームワークの開発と評価を行った。
浮動小数点演算と不動小数点演算の両方で実装されたANNの安全な挙動を保証できる。
小規模から中規模のANNの場合、我々の手法は検証のほとんどを数分で完了します。
- 参考スコア（独自算出の注目度）: 2.38142799291692
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Artificial Neural Networks (ANNs) are being deployed on an increasing number
of safety-critical applications, including autonomous cars and medical
diagnosis. However, concerns about their reliability have been raised due to
their black-box nature and apparent fragility to adversarial attacks. Here, we
develop and evaluate a symbolic verification framework using incremental model
checking (IMC) and satisfiability modulo theories (SMT) to check for
vulnerabilities in ANNs. More specifically, we propose several ANN-related
optimizations for IMC, including invariant inference via interval analysis and
the discretization of non-linear activation functions. With this, we can
provide guarantees on the safe behavior of ANNs implemented both in
floating-point and fixed-point (quantized) arithmetic. In this regard, our
verification approach was able to verify and produce adversarial examples for
52 test cases spanning image classification and general machine learning
applications. For small- to medium-sized ANN, our approach completes most of
its verification runs in minutes. Moreover, in contrast to most
state-of-the-art methods, our approach is not restricted to specific choices of
activation functions or non-quantized representations.
- Abstract（参考訳）: ANN(Artificial Neural Networks)は、自動運転車や医療診断など、安全に重要なアプリケーションにデプロイされている。
しかし、ブラックボックスの性質と敵の攻撃に対する明らかな脆弱さにより、信頼性に関する懸念が高まっている。
本稿では,インクリメンタル・モデル・チェック(imc)とsmt(sipfiability modulo theories)を用いて,annの脆弱性をチェックできるシンボリック検証フレームワークを開発し,評価する。
具体的には、インターバル解析による不変推論や非線形アクティベーション関数の離散化など、IMCのANN関連最適化を提案する。
これにより、浮動小数点演算と不動小数点演算の両方で実装されたANNの安全な挙動を保証できる。
そこで本研究では,画像分類と一般的な機械学習アプリケーションにまたがる52の試験事例に対して,検証を行い,検証を行った。
小型から中型ANNの場合、我々の手法は検証のほとんどを数分で完了する。
さらに、ほとんどの最先端手法とは対照的に、我々の手法はアクティベーション関数や非量子化表現の特定の選択に制限されない。
関連論文リスト
- Feature Attenuation of Defective Representation Can Resolve Incomplete Masking on Anomaly Detection [1.0358639819750703]
教師なし異常検出(UAD)研究では、計算効率が高くスケーラブルなソリューションを開発する必要がある。
再建・塗り替えのアプローチを再考し、強みと弱みを分析して改善する。
異常再構成の特徴情報を減衰させる2つの層のみを用いるFADeR(Feature Attenuation of Defective Representation)を提案する。
論文 参考訳（メタデータ） (2024-07-05T15:44:53Z) - Securing Graph Neural Networks in MLaaS: A Comprehensive Realization of Query-based Integrity Verification [68.86863899919358]
我々は機械学習におけるGNNモデルをモデル中心の攻撃から保護するための画期的なアプローチを導入する。
提案手法は,GNNの完全性に対する包括的検証スキーマを含み,トランスダクティブとインダクティブGNNの両方を考慮している。
本稿では,革新的なノード指紋生成アルゴリズムを組み込んだクエリベースの検証手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T03:17:05Z) - Quantization-aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks [58.195261590442406]
我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。
近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。
本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
論文 参考訳（メタデータ） (2022-11-29T13:32:38Z) - Abstraction and Refinement: Towards Scalable and Exact Verification of
Neural Networks [9.85360493553261]
ディープニューラルネットワーク(DNN)の実践はますます進んでいるが、ロバストさの欠如により、安全クリティカルなドメインへの応用が妨げられている。
本稿では,スケーラブルで正確なDNN検証のための新しい抽象化・リファインメント手法を提案する。
論文 参考訳（メタデータ） (2022-07-02T07:04:20Z) - Batch-Ensemble Stochastic Neural Networks for Out-of-Distribution
Detection [55.028065567756066]
Out-of-Distribution(OOD)検出は、機械学習モデルを現実世界のアプリケーションにデプロイすることの重要性から、マシンラーニングコミュニティから注目を集めている。
本稿では,特徴量の分布をモデル化した不確実な定量化手法を提案する。
バッチアンサンブルニューラルネットワーク(BE-SNN)の構築と機能崩壊問題の克服を目的として,効率的なアンサンブル機構,すなわちバッチアンサンブルを組み込んだ。
We show that BE-SNNs yield superior performance on the Two-Moons dataset, the FashionMNIST vs MNIST dataset, FashionM。
論文 参考訳（メタデータ） (2022-06-26T16:00:22Z) - Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。
この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。
本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
論文 参考訳（メタデータ） (2022-06-08T04:09:13Z) - On the benefits of robust models in modulation recognition [53.391095789289736]
畳み込み層を用いたディープニューラルネットワーク(DNN)は、通信における多くのタスクにおいて最先端である。
画像分類のような他の領域では、DNNは敵の摂動に弱いことが示されている。
最新モデルの堅牢性をテストするための新しいフレームワークを提案する。
論文 参考訳（メタデータ） (2021-03-27T19:58:06Z) - Selective and Features based Adversarial Example Detection [12.443388374869745]
Deep Neural Networks (DNN) を中継するセキュリティに敏感なアプリケーションは、Adversarial Examples (AE) を生成するために作られた小さな摂動に弱い。
本稿では,マルチタスク学習環境における選択的予測,モデルレイヤの出力処理,知識伝達概念を用いた教師なし検出機構を提案する。
実験の結果,提案手法は,ホワイトボックスシナリオにおけるテスト攻撃に対する最先端手法と同等の結果を得られ,ブラックボックスとグレーボックスシナリオの精度が向上した。
論文 参考訳（メタデータ） (2021-03-09T11:06:15Z) - Incremental Verification of Fixed-Point Implementations of Neural
Networks [0.19573380763700707]
インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
論文 参考訳（メタデータ） (2020-12-21T10:03:44Z) - A Simple Framework to Quantify Different Types of Uncertainty in Deep
Neural Networks for Image Classification [0.0]
モデルの予測の不確実性を定量化することは、AIシステムの安全性を高めるために重要である。
これは、自動運転車の制御、医療画像分析、財務推定、法的分野など、エラーのコストが高いアプリケーションにとって極めて重要である。
本稿では,画像分類の課題に対して,Deep Neural Networksにおいて既知の3種類の不確実性を捕捉し,定量化するための完全なフレームワークを提案する。
論文 参考訳（メタデータ） (2020-11-17T15:36:42Z) - A Hamiltonian Monte Carlo Method for Probabilistic Adversarial Attack
and Learning [122.49765136434353]
本稿では,HMCAM (Acumulated Momentum) を用いたハミルトニアンモンテカルロ法を提案する。
また, 対数的対数的対数的学習(Contrastive Adversarial Training, CAT)と呼ばれる新たな生成法を提案し, 対数的例の平衡分布にアプローチする。
いくつかの自然画像データセットと実用システムに関する定量的および定性的な解析により、提案アルゴリズムの優位性が確認された。
論文 参考訳（メタデータ） (2020-10-15T16:07:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。