論文の概要: QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking

• arxiv url: http://arxiv.org/abs/2111.13110v1
• Date: Thu, 25 Nov 2021 14:55:40 GMT
• ステータス: 処理完了
• システム内更新日: 2021-11-29 16:15:01.773101
• Title: QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
• Title（参考訳）: qnnverifier:smtベースのモデルチェックを用いたニューラルネットワークの検証ツール
• Authors: Xidan Song, Edoardo Manino, Luiz Sena, Erickson Alves, Eddie de Lima Filho, Iury Bessa, Mikel Lujan, Lucas Cordeiro
• Abstract要約: QNNVerifierは、ニューラルネットワークの実装を検証する最初のオープンソースツールである。 これは、ニューラルネットワークの実装を、満足度変調理論(SMT)に基づく一階述語論理の決定可能な断片に変換する。 これにより、安否確認プロパティを指定し、異なる検証戦略で結果のモデルを検証することができる。
• 参考スコア（独自算出の注目度）: 2.140126541785805
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifier allows to specify bespoke safety properties and verify the resulting model with different verification strategies (incremental and k-induction) and SMT solvers. Finally, QNNVerifier is the first tool that combines invariant inference via interval analysis and discretization of non-linear activation functions to speed up the verification of neural networks by orders of magnitude. A video presentation of QNNVerifier is available at https://youtu.be/7jMgOL41zTY
• Abstract（参考訳）: QNNVerifierは、演算子の有限ワード長(量子化)を考慮してニューラルネットワークの実装を検証する最初のオープンソースツールである。 量子化のための新しいサポートは、最先端ソフトウェアモデル検査(SMC)技術を用いて達成される。 ニューラルネットワークの実装を、満足度変調理論(SMT)に基づく一階述語論理の決定可能な断片に変換する。 固定点演算と浮動小数点演算の効果は、ハードウェア決定精度の直接実装によって表される。 さらに、QNNVerifierは、異常な安全性特性を特定し、異なる検証戦略(インクリメンタルおよびk-インダクション)とSMTソルバで結果モデルを検証することができる。 最後に、QNNVerifierは、インターバル解析と非線形アクティベーション関数の離散化による不変推論を組み合わせて、ニューラルネットワークの検証を桁違いに高速化する最初のツールである。 QNNVerifierのビデオプレゼンテーションはhttps://youtu.be/7jMgOL41zTYで公開されている。

関連論文リスト

• Scalable Mechanistic Neural Networks [52.28945097811129]
  長い時間的シーケンスを含む科学機械学習応用のための拡張ニューラルネットワークフレームワークを提案する。 元のメカニスティックニューラルネットワーク (MNN) を再構成することにより、計算時間と空間の複雑さを、それぞれ、列長に関して立方体と二次体から線形へと減少させる。 大規模な実験により、S-MNNは元のMNNと精度で一致し、計算資源を大幅に削減した。
  論文  参考訳（メタデータ） (2024-10-08T14:27:28Z)
• Exploiting the equivalence between quantum neural networks and perceptrons [2.598133279943607]
  パラメタライズド量子回路に基づく量子機械学習モデルは、量子デバイスへの応用において最も有望な候補であると考えられている。 我々はQNNの表現率と帰納バイアスを$x$から$xotimes x$に作用する古典的パーセプトロンへの入力を含むQNNからの正確なマッピングを利用して検討する。
  論文  参考訳（メタデータ） (2024-07-05T09:19:58Z)
• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  量子ニューラルネットワーク(QNN)が開発され、二項化ニューラルネットワーク(BNN)は特殊なケースとしてバイナリ値に制限されている。 本稿では,指定された特性を満たすBNNの自動合成手法を提案する。
  論文  参考訳（メタデータ） (2023-07-29T06:27:28Z)
• Permutation Equivariant Neural Functionals [92.0667671999604]
  この研究は、他のニューラルネットワークの重みや勾配を処理できるニューラルネットワークの設計を研究する。 隠れた層状ニューロンには固有の順序がないため, 深いフィードフォワードネットワークの重みに生じる置換対称性に着目する。 実験の結果, 置換同変ニューラル関数は多種多様なタスクに対して有効であることがわかった。
  論文  参考訳（メタデータ） (2023-02-27T18:52:38Z)
• QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks [14.766917269393865]
  量子化は、浮動小数点数に匹敵する精度でニューラルネットワークのサイズを減らすための有望な技術として登場した。 そこで本研究では,QNNに対する新しい,効率的な形式検証手法を提案する。 特に、QNNの検証問題を整数線形制約の解法に還元する符号化を初めて提案する。
  論文  参考訳（メタデータ） (2022-12-10T03:00:29Z)
• 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)
• Deterministic Tensor Network Classifiers [0.0]
  テンソルネットワークは決定論的に初期化され、短期中規模量子(NISQ)デバイスに実装される可能性がある。 特徴抽出は、$log N_textpixels$ qubitsで振幅符号化されたイメージを直接組み合わせて圧縮する。 性能は、構造によらず任意の分類器の予測に適用できる決定論的手法であるQuantum Stackingを用いて改善される。
  論文  参考訳（メタデータ） (2022-05-19T18:00:02Z)
• Toward Trainability of Quantum Neural Networks [87.04438831673063]
  量子ニューラルネットワーク(QNN)は、量子スピードアップを達成するために古典的ニューラルネットワークの一般化として提案されている。 QNNのトレーニングには、入力キュービット数に指数関数的に勾配速度がなくなるため、非常に大きなボトルネックが存在する。 木テンソルとステップ制御された構造を持つQNNを二分分類に適用し,ランダムな構造を持つQNNと比較してより高速な収束率と精度を示す。
  論文  参考訳（メタデータ） (2020-11-12T08:32:04Z)
• Decentralizing Feature Extraction with Quantum Convolutional Neural Network for Automatic Speech Recognition [101.69873988328808]
  特徴抽出のための量子回路エンコーダからなる量子畳み込みニューラルネットワーク(QCNN)を構築した。 入力音声はまず、Mel-spectrogramを抽出するために量子コンピューティングサーバにアップストリームされる。 対応する畳み込み特徴は、ランダムパラメータを持つ量子回路アルゴリズムを用いて符号化される。 符号化された機能は、最終認識のためにローカルRNNモデルにダウンストリームされる。
  論文  参考訳（メタデータ） (2020-10-26T03:36:01Z)
• Recurrent Quantum Neural Networks [7.6146285961466]
  リカレントニューラルネットワークは、機械学習における多くのシーケンス対シーケンスモデルの基盤となっている。 非自明なタスクに対して実証可能な性能を持つ量子リカレントニューラルネットワーク(QRNN)を構築する。 我々はQRNNをMNIST分類で評価し、QRNNに各画像ピクセルを供給し、また、最新のデータ拡張を前処理のステップとして利用する。
  論文  参考訳（メタデータ） (2020-06-25T17:59:44Z)
• Widening and Squeezing: Towards Accurate and Efficient QNNs [125.172220129257]
  量子化ニューラルネットワーク(QNN)は、非常に安価な計算とストレージオーバーヘッドのため、業界にとって非常に魅力的なものだが、その性能は、完全な精度パラメータを持つネットワークよりも悪い。 既存の手法の多くは、より効果的なトレーニング技術を利用して、特にバイナリニューラルネットワークの性能を高めることを目的としている。 本稿では,従来の完全精度ネットワークで高次元量子化機能に特徴を投影することで,この問題に対処する。
  論文  参考訳（メタデータ） (2020-02-03T04:11:13Z)

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

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