論文の概要: Neuro-Symbolic Verification of Deep Neural Networks
- arxiv url: http://arxiv.org/abs/2203.00938v1
- Date: Wed, 2 Mar 2022 08:40:01 GMT
- ステータス: 処理完了
- システム内更新日: 2022-03-03 14:19:59.906570
- Title: Neuro-Symbolic Verification of Deep Neural Networks
- Title（参考訳）: ディープニューラルネットワークのニューロシンボリック検証
- Authors: Xuan Xie, Kristian Kersting, Daniel Neider
- Abstract要約: 本稿ではニューラルシンボリック検証という,ニューラルネットワークの検証のための新しいフレームワークを提案する。
重要なアイデアは、論理的な仕様の一部としてニューラルネットワークを使用することだ。
本稿では,ニューラルネットワークの既存の検証基盤上に,ニューロシンボリック検証をどのように実装できるかを示す。
- 参考スコア（独自算出の注目度）: 20.973078277539276
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal verification has emerged as a powerful approach to ensure the safety
and reliability of deep neural networks. However, current verification tools
are limited to only a handful of properties that can be expressed as
first-order constraints over the inputs and output of a network. While
adversarial robustness and fairness fall under this category, many real-world
properties (e.g., "an autonomous vehicle has to stop in front of a stop sign")
remain outside the scope of existing verification technology. To mitigate this
severe practical restriction, we introduce a novel framework for verifying
neural networks, named neuro-symbolic verification. The key idea is to use
neural networks as part of the otherwise logical specification, enabling the
verification of a wide variety of complex, real-world properties, including the
one above. Moreover, we demonstrate how neuro-symbolic verification can be
implemented on top of existing verification infrastructure for neural networks,
making our framework easily accessible to researchers and practitioners alike.
- Abstract（参考訳）: 深層ニューラルネットワークの安全性と信頼性を確保するための強力なアプローチとして,形式的検証が登場した。
しかし、現在の検証ツールは、ネットワークの入力と出力に対する一階の制約として表現できるプロパティに限られている。
敵の頑健さと公正さはこのカテゴリーに該当するが、多くの現実世界の特性(例えば「自動運転車は停止標識の前に停止しなければならない」など)は既存の検証技術の範囲外にとどまる。
この厳しい実践的制約を軽減するため,ニューラルシンボリック検証という,ニューラルネットワークを検証するための新しい枠組みを導入する。
重要なアイデアは、論理的な仕様の一部としてニューラルネットワークを使用することで、上記を含むさまざまな複雑な実世界の特性の検証を可能にする。
さらに,ニューラルネットワークの既存の検証基盤上に,ニューロシンボリック検証を実装すれば,研究者や実践者にも容易にフレームワークが利用できるようになることを実証する。
関連論文リスト
- Quantum-Inspired Analysis of Neural Network Vulnerabilities: The Role of
Conjugate Variables in System Attacks [54.565579874913816]
ニューラルネットワークは、敵の攻撃として現れる小さな非ランダムな摂動に固有の脆弱性を示す。
この機構と量子物理学の不確実性原理の間に数学的に一致し、予想外の学際性に光を当てる。
論文 参考訳（メタデータ） (2024-02-16T02:11:27Z) - Expediting Neural Network Verification via Network Reduction [4.8621567234713305]
本稿では,検証前の事前処理手法として,ネットワーク削減手法を提案する。
提案手法は、安定なReLUニューロンを除去し、それらをシーケンシャルなニューラルネットワークに変換することにより、ニューラルネットワークを削減する。
我々は、最先端の完全および不完全検証ツールの縮小手法をインスタンス化する。
論文 参考訳（メタデータ） (2023-08-07T06:23:24Z) - Fully Automatic Neural Network Reduction for Formal Verification [8.017543518311196]
到達可能性解析を用いたニューラルネットワークの完全自動・音量低減手法を提案する。
音質は、低減されたネットワークの検証が元のネットワークの検証を必要とすることを保証します。
提案手法は, ニューロンの数を, 小さい外近似で, 元のニューロン数のごく一部に減らすことができることを示す。
論文 参考訳（メタデータ） (2023-05-03T07:13:47Z) - Efficient Symbolic Reasoning for Neural-Network Verification [48.384446430284676]
本稿では,ニューラルネットワーク検証のための新しいプログラム推論フレームワークを提案する。
我々のフレームワークの主要な構成要素は、記号領域と二次関係の利用である。
我々のフレームワークは、ニューラルネットワークの検証問題に新しい理論的洞察と実践的なツールをもたらすことができると信じている。
論文 参考訳（メタデータ） (2023-03-23T18:08:11Z) - 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) - CheckINN: Wide Range Neural Network Verification in Imandra [0.0]
我々は,関数型プログラミング言語Imandraと定理証明器が,ニューラルネットワーク検証のための総合的な基盤を提供する方法を示す。
We developed a novel library CheckINN that formals neural network in Imandra, and covers different important facets of neural network verification。
論文 参考訳（メタデータ） (2022-07-21T16:06:58Z) - Searching for the Essence of Adversarial Perturbations [73.96215665913797]
本稿では,ニューラルネットワークの誤予測の原因となる,人間の認識可能な情報を含む対人摂動について述べる。
この人間の認識可能な情報の概念は、敵の摂動に関連する重要な特徴を説明できる。
論文 参考訳（メタデータ） (2022-05-30T18:04:57Z) - Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem
Provers [1.5749416770494706]
車両には、ニューラルネットワーク仕様を記述するための表現力のあるドメイン固有言語が備わっている。
同様のITPの形式化において、保守性とスケーラビリティに関する過去の問題を克服しています。
ニューラルネットワーク検証器であるMarabouをAgdaに接続し、ニューラルネットワークで操縦された車が道路を離れないことを正式に検証することで、その実用性を実証する。
論文 参考訳（メタデータ） (2022-02-10T18:09:23Z) - Building Compact and Robust Deep Neural Networks with Toeplitz Matrices [93.05076144491146]
この論文は、コンパクトで、訓練が容易で、信頼性があり、敵の例に対して堅牢なニューラルネットワークを訓練する問題に焦点を当てている。
Toeplitzファミリーの構造化行列の特性を利用して、コンパクトでセキュアなニューラルネットワークを構築する。
論文 参考訳（メタデータ） (2021-09-02T13:58:12Z) - Provably Training Neural Network Classifiers under Fairness Constraints [70.64045590577318]
過パラメータのニューラルネットワークが制約を満たしていることを示す。
公平なニューラルネットワーク分類器を構築する上で重要な要素は、ニューラルネットワークの非応答解析を確立することである。
論文 参考訳（メタデータ） (2020-12-30T18:46:50Z) - Towards Repairing Neural Networks Correctly [6.600380575920419]
本稿では,ニューラルネットワークの正確性を保証するための実行時検証手法を提案する。
実験結果から,本手法は特性を満たすことが保証されたニューラルネットワークを効果的に生成することが示された。
論文 参考訳（メタデータ） (2020-12-03T12:31:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。