論文の概要: 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桁の高速化が可能となった。
関連論文リスト
- A Lightweight, Efficient and Explainable-by-Design Convolutional Neural
Network for Internet Traffic Classification [66.58073672357064]
本稿では、インターネットトラフィック分類のための軽量で効率的なeXplainable-by-design畳み込みニューラルネットワーク(LEXNet)を提案する。
LEXNetは(軽量で効率の良い目的のために)新しい残留ブロックと(説明可能性のために)プロトタイプ層に依存している。
商用グレードのデータセットに基づいて、LEXNetは最先端のニューラルネットワークと同じ精度を維持することに成功した。
論文 参考訳（メタデータ） (2022-02-11T10:21:34Z) - Robustness Verification for Attention Networks using Mixed Integer
Programming [2.365702128814616]
線形化層正規化とスパースマックス活性化を含むアテンションネットワークの変種を定式化する。
一般ニューラルネットワークにおけるソフトマックスアクティベーションにも適用可能な,スパースマックスアクティベーションのための新しいバウンディング手法を見出した。
注意ネットワークは一般的に一般的なニューラルネットワークよりも高い精度を提供するが、同じ大きさのマルチ層パーセプトロンに対して頑丈さは、必ずしも堅牢ではないことを驚くほど示している。
論文 参考訳（メタデータ） (2022-02-08T15:27:33Z) - Post-training Quantization for Neural Networks with Provable Guarantees [9.58246628652846]
学習後ニューラルネットワーク量子化手法であるGPFQを,欲求経路追従機構に基づいて修正する。
単層ネットワークを定量化するためには、相対二乗誤差は本質的に重み数で線形に減衰する。
論文 参考訳（メタデータ） (2022-01-26T18:47:38Z) - Neural Network Quantization for Efficient Inference: A Survey [0.0]
ニューラルネットワークの量子化は、最近、ニューラルネットワークのサイズと複雑さを減らすというこの要求を満たすために発生した。
本稿では,過去10年間に開発された多くのニューラルネットワーク量子化技術について検討する。
論文 参考訳（メタデータ） (2021-12-08T22:49:39Z) - A Layer-wise Adversarial-aware Quantization Optimization for Improving
Robustness [4.794745827538956]
逆向きに学習したニューラルネットワークは、通常のモデルよりも量子化損失に対して脆弱であることがわかった。
ニューラルネットワークの最適量子化パラメータ設定を選択するために,Lipschitz定数を用いた層ワイド逆アウェア量子化法を提案する。
実験結果から,本手法は,量子化逆学習ニューラルネットワークのロバスト性を効果的かつ効果的に向上できることが示された。
論文 参考訳（メタデータ） (2021-10-23T22:11:30Z) - Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity
on Pruned Neural Networks [79.74580058178594]
目的関数の幾何学的構造を解析することにより、刈り取られたニューラルネットワークを訓練する性能を解析する。
本稿では,ニューラルネットワークモデルがプルーニングされるにつれて,一般化が保証された望ましいモデル近傍の凸領域が大きくなることを示す。
論文 参考訳（メタデータ） (2021-10-12T01:11:07Z) - Cluster-Promoting Quantization with Bit-Drop for Minimizing Network
Quantization Loss [61.26793005355441]
クラスタ・プロモーティング・量子化(CPQ)は、ニューラルネットワークに最適な量子化グリッドを見つける。
DropBitsは、ニューロンの代わりにランダムにビットをドロップする標準のドロップアウト正規化を改訂する新しいビットドロップ技術である。
本手法を様々なベンチマークデータセットとネットワークアーキテクチャ上で実験的に検証する。
論文 参考訳（メタデータ） (2021-09-05T15:15:07Z) - Mitigating Performance Saturation in Neural Marked Point Processes:
Architectures and Loss Functions [50.674773358075015]
本稿では,グラフ畳み込み層のみを利用するGCHPという単純なグラフベースのネットワーク構造を提案する。
我々は,GCHPがトレーニング時間を大幅に短縮し,時間間確率仮定による確率比損失がモデル性能を大幅に改善できることを示した。
論文 参考訳（メタデータ） (2021-07-07T16:59:14Z) - SignalNet: A Low Resolution Sinusoid Decomposition and Estimation
Network [79.04274563889548]
本稿では,正弦波数を検出するニューラルネットワークアーキテクチャであるSignalNetを提案する。
基礎となるデータ分布と比較して,ネットワークの結果を比較するための最悪の学習しきい値を導入する。
シミュレーションでは、我々のアルゴリズムは常に3ビットデータのしきい値を超えることができるが、しばしば1ビットデータのしきい値を超えることはできない。
論文 参考訳（メタデータ） (2021-06-10T04:21:20Z) - A Survey of Quantization Methods for Efficient Neural Network Inference [75.55159744950859]
量子化は、必要なビット数を最小限に抑えるために、固定された離散数の集合に連続実数値を分散する問題である。
近年、コンピュータビジョン、自然言語処理、関連分野でのニューラルネットワークモデルの顕著な性能のために最前線に達しています。
浮動小数点表現から4ビット以下の低精度固定整数値への移行は、メモリフットプリントとレイテンシを16倍削減する可能性を秘めている。
論文 参考訳（メタデータ） (2021-03-25T06:57:11Z) - Data-free mixed-precision quantization using novel sensitivity metric [6.031526641614695]
量子化誤差がタスクロスや他の層との相互作用に与える影響を考慮した新しい感度測定法を提案する。
実験により,提案手法が量子化感度をよりよく表現し,生成したデータは混合精度量子化に適用できることを示す。
論文 参考訳（メタデータ） (2021-03-18T07:23:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。