論文の概要: Scalable Verification of Quantized Neural Networks (Technical Report)
- arxiv url: http://arxiv.org/abs/2012.08185v1
- Date: Tue, 15 Dec 2020 10:05:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2021-05-07 05:36:53.879864
- Title: Scalable Verification of Quantized Neural Networks (Technical Report)
- Title（参考訳）: 量子化ニューラルネットワークのスケーラブルな検証(技術報告)
- Authors: Thomas A. Henzinger, Mathias Lechner, {\DJ}or{\dj}e \v{Z}ikeli\'c
- Abstract要約: ビットベクトル仕様を持つ量子化ニューラルネットワークのビットエクササイズ実装はPSPACEハードであることを示す。
量子化されたニューラルネットワークのSMTに基づく検証をよりスケーラブルにするための3つの手法を提案する。
- 参考スコア（独自算出の注目度）: 14.04927063847749
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification of neural networks is an active topic of research, and
recent advances have significantly increased the size of the networks that
verification tools can handle. However, most methods are designed for
verification of an idealized model of the actual network which works over real
arithmetic and ignores rounding imprecisions. This idealization is in stark
contrast to network quantization, which is a technique that trades numerical
precision for computational efficiency and is, therefore, often applied in
practice. Neglecting rounding errors of such low-bit quantized neural networks
has been shown to lead to wrong conclusions about the network's correctness.
Thus, the desired approach for verifying quantized neural networks would be one
that takes these rounding errors into account. In this paper, we show that
verifying the bit-exact implementation of quantized neural networks with
bit-vector specifications is PSPACE-hard, even though verifying idealized
real-valued networks and satisfiability of bit-vector specifications alone are
each in NP. Furthermore, we explore several practical heuristics toward closing
the complexity gap between idealized and bit-exact verification. In particular,
we propose three techniques for making SMT-based verification of quantized
neural networks more scalable. Our experiments demonstrate that our proposed
methods allow a speedup of up to three orders of magnitude over existing
approaches.
- Abstract（参考訳）: ニューラルネットワークの形式的検証は研究の活発なトピックであり、最近の進歩により、検証ツールが扱えるネットワークのサイズが大幅に増加した。
しかし,ほとんどの手法は実数演算上で動作し,ラウンドリング不正確さを無視する実ネットワークの理想的なモデルを検証するために設計されている。
この理想化は、数値の精度を計算効率と交換する手法であるネットワーク量子化とは対照的であり、したがって実際にはしばしば適用される。
このような低ビット量子化ニューラルネットワークの丸め誤差を無視すると、ネットワークの正しさに関する誤った結論が導かれる。
したがって、量子化されたニューラルネットワークを検証するための望ましいアプローチは、これらの丸め誤差を考慮するものである。
本稿では,ビットベクトル仕様のみを満足できる理想化された実数値ネットワークを検証したとしても,ビットベクトル仕様による量子化ニューラルネットワークの実装がPSPACEハードであることを示す。
さらに,理想化とビット実行検証の複雑性ギャップを埋めるための実用的ヒューリスティックスについて検討する。
特に,SMTに基づく量子化ニューラルネットワークの検証をよりスケーラブルにするための3つの手法を提案する。
実験の結果,提案手法では既存手法に比べて最大3桁の高速化が可能となった。
関連論文リスト
- Verified Neural Compressed Sensing [58.98637799432153]
精度の高い計算タスクのために、初めて(私たちの知識を最大限に活用するために)証明可能なニューラルネットワークを開発します。
極小問題次元(最大50)では、線形および双項線形測定からスパースベクトルを確実に回復するニューラルネットワークを訓練できることを示す。
ネットワークの複雑さは問題の難易度に適応できることを示し、従来の圧縮センシング手法が証明不可能な問題を解く。
論文 参考訳（メタデータ） (2024-05-07T12:20:12Z) - On the Convergence of Locally Adaptive and Scalable Diffusion-Based Sampling Methods for Deep Bayesian Neural Network Posteriors [2.3265565167163906]
ベイズニューラルネットワークは、ディープニューラルネットワークにおける不確実性をモデル化するための有望なアプローチである。
ニューラルネットワークの 後部分布からサンプルを生成することは 大きな課題です
この方向の進歩の1つは、モンテカルロ・マルコフ連鎖サンプリングアルゴリズムへの適応的なステップサイズの導入である。
本稿では,これらの手法が,ステップサイズやバッチサイズが小さくても,サンプリングした分布にかなりの偏りがあることを実証する。
論文 参考訳（メタデータ） (2024-03-13T15:21:14Z) - Expediting Neural Network Verification via Network Reduction [4.8621567234713305]
本稿では,検証前の事前処理手法として,ネットワーク削減手法を提案する。
提案手法は、安定なReLUニューロンを除去し、それらをシーケンシャルなニューラルネットワークに変換することにより、ニューラルネットワークを削減する。
我々は、最先端の完全および不完全検証ツールの縮小手法をインスタンス化する。
論文 参考訳（メタデータ） (2023-08-07T06:23:24Z) - 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) - CEG4N: Counter-Example Guided Neural Network Quantization Refinement [2.722899166098862]
我々は,カウンタ・サンプル・ガイド付きニューラルネットワーク量子化リファインメント(CEG4N)を提案する。
この手法は探索に基づく量子化と等価検証を組み合わせたものである。
最先端技術よりも最大72%精度のモデルを作成します。
論文 参考訳（メタデータ） (2022-07-09T09:25:45Z) - Post-training Quantization for Neural Networks with Provable Guarantees [9.58246628652846]
学習後ニューラルネットワーク量子化手法であるGPFQを,欲求経路追従機構に基づいて修正する。
単層ネットワークを定量化するためには、相対二乗誤差は本質的に重み数で線形に減衰する。
論文 参考訳（メタデータ） (2022-01-26T18:47:38Z) - Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity
on Pruned Neural Networks [79.74580058178594]
目的関数の幾何学的構造を解析することにより、刈り取られたニューラルネットワークを訓練する性能を解析する。
本稿では,ニューラルネットワークモデルがプルーニングされるにつれて,一般化が保証された望ましいモデル近傍の凸領域が大きくなることを示す。
論文 参考訳（メタデータ） (2021-10-12T01:11:07Z) - Searching for Low-Bit Weights in Quantized Neural Networks [129.8319019563356]
低ビットの重みとアクティベーションを持つ量子ニューラルネットワークは、AIアクセラレータを開発する上で魅力的なものだ。
本稿では、任意の量子化ニューラルネットワークにおける離散重みを探索可能な変数とみなし、差分法を用いて正確に探索する。
論文 参考訳（メタデータ） (2020-09-18T09:13:26Z) - ESPN: Extremely Sparse Pruned Networks [50.436905934791035]
簡単な反復マスク探索法により,非常に深いネットワークの最先端の圧縮を実現することができることを示す。
本アルゴリズムは,シングルショット・ネットワーク・プルーニング法とロッテ・ティケット方式のハイブリッド・アプローチを示す。
論文 参考訳（メタデータ） (2020-06-28T23:09:27Z) - Widening and Squeezing: Towards Accurate and Efficient QNNs [125.172220129257]
量子化ニューラルネットワーク(QNN)は、非常に安価な計算とストレージオーバーヘッドのため、業界にとって非常に魅力的なものだが、その性能は、完全な精度パラメータを持つネットワークよりも悪い。
既存の手法の多くは、より効果的なトレーニング技術を利用して、特にバイナリニューラルネットワークの性能を高めることを目的としている。
本稿では,従来の完全精度ネットワークで高次元量子化機能に特徴を投影することで,この問題に対処する。
論文 参考訳（メタデータ） (2020-02-03T04:11:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。