論文の概要: Incremental Verification of Fixed-Point Implementations of Neural
Networks
- arxiv url: http://arxiv.org/abs/2012.11220v1
- Date: Mon, 21 Dec 2020 10:03:44 GMT
- ステータス: 処理完了
- システム内更新日: 2021-04-27 06:24:50.742578
- Title: Incremental Verification of Fixed-Point Implementations of Neural
Networks
- Title（参考訳）: ニューラルネットワークの固定点実装のインクリメンタル検証
- Authors: Luiz Sena, Erickson Alves, Iury Bessa, Eddie Filho, and Lucas Cordeiro
- Abstract要約: インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
- 参考スコア（独自算出の注目度）: 0.19573380763700707
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Implementations of artificial neural networks (ANNs) might lead to failures,
which are hardly predicted in the design phase since ANNs are highly parallel
and their parameters are barely interpretable. Here, we develop and evaluate a
novel symbolic verification framework using incremental bounded model checking
(BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain
adversarial cases and validate coverage methods in a multi-layer perceptron
(MLP). We exploit incremental BMC based on interval analysis to compute
boundaries from a neuron's input. Then, the latter are propagated to
effectively find a neuron's output since it is the input of the next one. This
paper describes the first bit-precise symbolic verification framework to reason
over actual implementations of ANNs in CUDA, based on invariant inference,
therefore providing further guarantees about finite-precision arithmetic and
its rounding errors, which are routinely ignored in the existing literature. We
have implemented the proposed approach on top of the efficient SMT-based
bounded model checker (ESBMC), and its experimental results show that it can
successfully verify safety properties, in actual implementations of ANNs, and
generate real adversarial cases in MLPs. Our approach was able to verify and
produce adversarial examples for 85.8% of 21 test cases considering different
input images, and 100% of the properties related to covering methods. Although
our verification time is higher than existing approaches, our methodology can
consider fixed-point implementation aspects that are disregarded by the
state-of-the-art verification methodologies.
- Abstract（参考訳）: 人工ニューラルネットワーク(ANN)の実装は、ANNが並列性が高く、パラメータがほとんど解釈できないため、設計段階では予測できない失敗につながる可能性がある。
本稿では, インクリメンタル境界モデル検査 (BMC) , SMT (Satisfiability modulo theory) および不変推論を用いた新しい記号検証フレームワークの開発と評価を行い, 多層パーセプトロン (MLP) における逆ケースの取得とカバレッジ手法の検証を行う。
ニューロンの入力から境界を計算するために間隔解析に基づくインクリメンタルbmcを利用する。
次に、後者を伝播させて、次のニューロンの入力であるため、ニューロンの出力を効果的に見つける。
本稿では,変分推論に基づくCUDAにおけるANNの実際の実装を推論する最初のビット精度シンボル検証フレームワークについて述べる。
提案手法は,効率的なSMTベース有界モデルチェッカー(ESBMC)上に実装されており,その実験結果から,ANNの実際の実装における安全性特性の検証と,MLPにおける実敵ケースの生成が可能であることが示された。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
検証時間は既存の手法よりも高いが,現状の検証手法では無視できる固定点実装の側面を検討することができる。
関連論文リスト
- Model-Agnostic Few-Shot Open-Set Recognition [36.97433312193586]
我々はFew-Shot Open-Set Recognition (FSOSR) 問題に取り組む。
既存のモデルにプラグイン可能なモデルに依存しない推論手法の開発に注力する。
オープン・セット・トランスダクティブ・インフォメーション・最大化手法OSTIMを提案する。
論文 参考訳（メタデータ） (2022-06-18T16:27:59Z) - Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。
この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。
本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
論文 参考訳（メタデータ） (2022-06-08T04:09:13Z) - A Simple Approach to Improve Single-Model Deep Uncertainty via
Distance-Awareness [33.09831377640498]
本研究では,1つの決定論的表現に基づく1つのネットワークの不確実性向上手法について検討する。
本稿では,現代のDNNにおける距離認識能力を向上させる簡易な手法として,スペクトル正規化ニューラルガウス過程(SNGP)を提案する。
ビジョンと言語理解のベンチマークスイートでは、SNGPは予測、キャリブレーション、ドメイン外検出において、他の単一モデルアプローチよりも優れている。
論文 参考訳（メタデータ） (2022-05-01T05:46:13Z) - NUQ: Nonparametric Uncertainty Quantification for Deterministic Neural
Networks [151.03112356092575]
本研究では,Nadaraya-Watson の条件付きラベル分布の非パラメトリック推定に基づく分類器の予測の不確かさの測定方法を示す。
種々の実世界の画像データセットにおける不確実性推定タスクにおいて,本手法の強い性能を示す。
論文 参考訳（メタデータ） (2022-02-07T12:30:45Z) - Training on Test Data with Bayesian Adaptation for Covariate Shift [96.3250517412545]
ディープニューラルネットワークは、信頼できない不確実性推定で不正確な予測を行うことが多い。
分布シフトの下でのラベルなし入力とモデルパラメータとの明確に定義された関係を提供するベイズモデルを導出する。
本手法は精度と不確実性の両方を向上することを示す。
論文 参考訳（メタデータ） (2021-09-27T01:09:08Z) - On the Practicality of Deterministic Epistemic Uncertainty [106.06571981780591]
決定論的不確実性法(DUM)は,分布外データの検出において高い性能を達成する。
DUMが十分に校正されており、現実のアプリケーションにシームレスにスケールできるかどうかは不明だ。
論文 参考訳（メタデータ） (2021-07-01T17:59:07Z) - Verifying Quantized Neural Networks using SMT-Based Model Checking [2.38142799291692]
インクリメンタルモデルチェック(IMC)と満足度変調理論(SMT)を用いたシンボリック検証フレームワークの開発と評価を行った。
浮動小数点演算と不動小数点演算の両方で実装されたANNの安全な挙動を保証できる。
小規模から中規模のANNの場合、我々の手法は検証のほとんどを数分で完了します。
論文 参考訳（メタデータ） (2021-06-10T18:27:45Z) - Minimum-Delay Adaptation in Non-Stationary Reinforcement Learning via
Online High-Confidence Change-Point Detection [7.685002911021767]
非定常環境におけるポリシーを効率的に学習するアルゴリズムを導入する。
これは、リアルタイム、高信頼な変更点検出統計において、潜在的に無限のデータストリームと計算を解析する。
i) このアルゴリズムは, 予期せぬ状況変化が検出されるまでの遅延を最小限に抑え, 迅速な応答を可能にする。
論文 参考訳（メタデータ） (2021-05-20T01:57:52Z) - Attentional Prototype Inference for Few-Shot Semantic Segmentation [114.74344993331196]
数ショットセマンティックセグメンテーションのための確率的潜時変数フレームワークである注目プロトタイプ推論(API)を提案する。
我々は各オブジェクトカテゴリのプロトタイプを表現するためにグローバル潜在変数を定義し、確率分布としてモデル化する。
我々は3つのベンチマークについて広範な実験を行い,提案手法は最先端手法よりも,少なくとも競争性が高く,しばしば優れた性能を得る。
論文 参考訳（メタデータ） (2021-05-14T06:58:44Z) - Improving Uncertainty Calibration via Prior Augmented Data [56.88185136509654]
ニューラルネットワークは、普遍関数近似器として機能することで、複雑なデータ分布から学習することに成功した。
彼らはしばしば予測に自信過剰であり、不正確で誤った確率的予測に繋がる。
本稿では,モデルが不当に過信である特徴空間の領域を探索し,それらの予測のエントロピーをラベルの以前の分布に対して条件的に高める手法を提案する。
論文 参考訳（メタデータ） (2021-02-22T07:02:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。