論文の概要: QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks

• arxiv url: http://arxiv.org/abs/2212.11138v1
• Date: Sat, 10 Dec 2022 03:00:29 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-25 03:11:33.165580
• Title: QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks
• Title（参考訳）: QVIP: ILPに基づく量子ニューラルネットワークの形式検証手法
• Authors: Yedi Zhang and Zhe Zhao and Fu Song and Min Zhang and Taolue Chen and Jun Sun
• Abstract要約: 量子化は、浮動小数点数に匹敵する精度でニューラルネットワークのサイズを減らすための有望な技術として登場した。 そこで本研究では,QNNに対する新しい,効率的な形式検証手法を提案する。 特に、QNNの検証問題を整数線形制約の解法に還元する符号化を初めて提案する。
• 参考スコア（独自算出の注目度）: 14.766917269393865
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.
• Abstract（参考訳）: ディープラーニングは、多くの課題を解決するという驚くべきパフォーマンスのおかげで、ソフトウェア開発において有望なプログラミングパラダイムになっています。 ディープニューラルネットワーク(DNN)の実用化はますます進んでいるが、計算能力の需要のためリソース制限されたデバイスに限られている。 量子化は、浮動小数点数に匹敵する精度でDNNのサイズを減らすための有望な手法として登場した。 結果の量子化ニューラルネットワーク(QNN)はエネルギー効率よく実装できる。 浮動小数点数(floating-point numbered)と同様、QNNの品質保証技術(テストや形式検証など)は必須だが、現在はあまり研究されていない。 そこで本研究では,QNNに対する新規かつ効率的な形式検証手法を提案する。 特に,本研究では,QNNの検証問題を整数線形制約の解法に還元する符号化法を提案する。 私たちのエンコーディングは健全かつ完全です。 本稿では,局所ロバスト性検証と最大ロバスト性半径計算への応用を示す。 提案手法を試作ツールQVIPに実装し,徹底的な評価を行う。 量子化ビットの異なるQNNの実験結果により、我々のアプローチの有効性と効率、例えば、2桁の精度で、最先端の手法よりも多くの検証タスクを同時に解くことができる。

関連論文リスト

• ARQ: A Mixed-Precision Quantization Framework for Accurate and Certifiably Robust DNNs [15.43153209571646]
  混合精度量子化は、限られたリソースコンピューティングプラットフォーム上でディープニューラルネットワーク(DNN)の実行を可能にする重要な技術となっている。 本稿では、スムーズな分類器のクリーンな精度を保ちつつ、その信頼性を保ちながら、新しい混合精度量子化手法であるARQを紹介する。
  論文  参考訳（メタデータ） (2024-10-31T17:59:37Z)
• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  量子ニューラルネットワーク(QNN)が開発され、二項化ニューラルネットワーク(BNN)は特殊なケースとしてバイナリ値に制限されている。 本稿では,指定された特性を満たすBNNの自動合成手法を提案する。
  論文  参考訳（メタデータ） (2023-07-29T06:27:28Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• QEBVerif: Quantization Error Bound Verification of Neural Networks [6.327780998441913]
  量子化は、エッジデバイスにディープニューラルネットワーク(DNN)をデプロイするための有望なテクニックとして広く見なされている。 既存の検証方法は、個々のニューラルネットワーク(DNNまたはQNN)または部分量子化のための量子化エラーにフォーカスする。 本稿では、重みとアクティベーションテンソルの両方を量子化する量子化誤差境界検証手法QEBVerifを提案する。
  論文  参考訳（メタデータ） (2022-12-06T06:34:38Z)
• 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)
• Low-bit Shift Network for End-to-End Spoken Language Understanding [7.851607739211987]
  本稿では,連続パラメータを低ビットの2値に量子化する2乗量子化法を提案する。 これにより、高価な乗算演算を除去し、低ビット重みを使用すれば計算の複雑さを低減できる。
  論文  参考訳（メタデータ） (2022-07-15T14:34:22Z)
• FATNN: Fast and Accurate Ternary Neural Networks [89.07796377047619]
  Ternary Neural Networks (TNN) は、完全な精度のニューラルネットワークよりもはるかに高速で、電力効率が高いため、多くの注目を集めている。 そこで本研究では、3次内積の計算複雑性を2。 性能ギャップを軽減するために,実装に依存した3次量子化アルゴリズムを精巧に設計する。
  論文  参考訳（メタデータ） (2020-08-12T04:26:18Z)
• AQD: Towards Accurate Fully-Quantized Object Detection [94.06347866374927]
  本稿では,浮動小数点演算を除去するために,AQDと呼ばれる高精度な量子化オブジェクト検出ソリューションを提案する。 我々のAQDは、非常に低ビットのスキームの下での完全精度と比較して、同等またはそれ以上の性能を実現しています。
  論文  参考訳（メタデータ） (2020-07-14T09:07:29Z)
• Boosting Deep Neural Networks with Geometrical Prior Knowledge: A Survey [77.99182201815763]
  ディープニューラルネットワーク(DNN)は多くの異なる問題設定において最先端の結果を達成する。 DNNはしばしばブラックボックスシステムとして扱われ、評価と検証が複雑になる。 コンピュータビジョンタスクにおける畳み込みニューラルネットワーク(CNN)の成功に触発された、有望な分野のひとつは、対称幾何学的変換に関する知識を取り入れることである。
  論文  参考訳（メタデータ） (2020-06-30T14:56:05Z)
• Widening and Squeezing: Towards Accurate and Efficient QNNs [125.172220129257]
  量子化ニューラルネットワーク(QNN)は、非常に安価な計算とストレージオーバーヘッドのため、業界にとって非常に魅力的なものだが、その性能は、完全な精度パラメータを持つネットワークよりも悪い。 既存の手法の多くは、より効果的なトレーニング技術を利用して、特にバイナリニューラルネットワークの性能を高めることを目的としている。 本稿では,従来の完全精度ネットワークで高次元量子化機能に特徴を投影することで,この問題に対処する。
  論文  参考訳（メタデータ） (2020-02-03T04:11:13Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。