論文の概要: 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%を検証・生成することができた。
検証時間は既存の手法よりも高いが,現状の検証手法では無視できる固定点実装の側面を検討することができる。
関連論文リスト
- cDP-MIL: Robust Multiple Instance Learning via Cascaded Dirichlet Process [23.266122629592807]
マルチプル・インスタンス・ラーニング (MIL) は全スライス・ヒストパラメトリック・イメージ (WSI) 解析に広く応用されている。
MILの既存の集約戦略は、主にインスタンス間の一階距離に依存するが、各インスタンスの真の特徴分布を正確に近似することができない。
本稿では、複数のインスタンス学習のための新しいベイズ非パラメトリックフレームワークを提案し、WSIのインスタンス・ツー・バッグ特性を組み込むためにディリクレ・プロセスのカスケード(cDP)を採用する。
論文 参考訳（メタデータ） (2024-07-16T07:28:39Z) - 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) - Learning Algorithms for Verification of Markov Decision Processes [20.5951492453299]
マルコフ決定過程(MDP)の検証に学習アルゴリズムを適用するための一般的な枠組みを提案する。
提案するフレームワークは,検証における中核的な問題である確率的到達性に重点を置いている。
論文 参考訳（メタデータ） (2024-03-14T08:54:19Z) - Provably Efficient UCB-type Algorithms For Learning Predictive State
Representations [55.00359893021461]
逐次決定問題は、予測状態表現(PSR)によってモデル化された低ランク構造が認められる場合、統計的に学習可能である
本稿では,推定モデルと実モデル間の全変動距離を上限とする新しいボーナス項を特徴とする,PSRに対する最初のUCB型アプローチを提案する。
PSRに対する既存のアプローチとは対照的に、UCB型アルゴリズムは計算的トラクタビリティ、最優先の準最適ポリシー、モデルの精度が保証される。
論文 参考訳（メタデータ） (2023-07-01T18:35:21Z) - Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。
また、局所的な一貫性の結果に基づいた理論的保証も提供する。
この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
論文 参考訳（メタデータ） (2022-11-17T15:48:06Z) - NUQ: Nonparametric Uncertainty Quantification for Deterministic Neural
Networks [151.03112356092575]
本研究では,Nadaraya-Watson の条件付きラベル分布の非パラメトリック推定に基づく分類器の予測の不確かさの測定方法を示す。
種々の実世界の画像データセットにおける不確実性推定タスクにおいて,本手法の強い性能を示す。
論文 参考訳（メタデータ） (2022-02-07T12:30:45Z) - 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) - Amortized Conditional Normalized Maximum Likelihood: Reliable Out of
Distribution Uncertainty Estimation [99.92568326314667]
本研究では,不確実性推定のための拡張性のある汎用的アプローチとして,償却条件正規化最大値(ACNML)法を提案する。
提案アルゴリズムは条件付き正規化最大度(CNML)符号化方式に基づいており、最小記述長の原理に従って最小値の最適特性を持つ。
我々は、ACNMLが、分布外入力のキャリブレーションの観点から、不確実性推定のための多くの手法と好意的に比較することを示した。
論文 参考訳（メタデータ） (2020-11-05T08:04:34Z) - Explaining and Improving Model Behavior with k Nearest Neighbor
Representations [107.24850861390196]
モデルの予測に責任のあるトレーニング例を特定するために, k 近傍表現を提案する。
我々は,kNN表現が学習した素因関係を明らかにするのに有効であることを示す。
以上の結果から,kNN手法により,直交モデルが逆入力に対してより堅牢であることが示唆された。
論文 参考訳（メタデータ） (2020-10-18T16:55:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。