論文の概要: Efficient Certified Reasoning for Binarized Neural Networks
- arxiv url: http://arxiv.org/abs/2507.02916v1
- Date: Wed, 25 Jun 2025 09:27:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-13 12:05:57.518817
- Title: Efficient Certified Reasoning for Binarized Neural Networks
- Title(参考訳): 二元化ニューラルネットワークの効率的な認証推論
- Authors: Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel,
- Abstract要約: バイナリニューラルネットワーク(BNN)は、各ニューロンがブール値に制約されるニューラルネットワークの一種である。
既存のBNN解析手法では、スケーラビリティの制限や音質誤差への感受性に悩まされている。
我々は,BNNの質的,定量的な検証のために,スケーラブルで信頼性の高い手法を提案する。
- 参考スコア(独自算出の注目度): 25.20597060311209
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Neural networks have emerged as essential components in safety-critical applications -- these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNNs) are a type of neural network where each neuron is constrained to a Boolean value; they are particularly well-suited for safety-critical tasks because they retain much of the computational capacities of full-scale (floating-point or quantized) deep neural networks, but remain compatible with satisfiability solvers for qualitative verification and with model counters for quantitative reasoning. However, existing methods for BNN analysis suffer from either limited scalability or susceptibility to soundness errors, which hinders their applicability in real-world scenarios. In this work, we present a scalable and trustworthy approach for both qualitative and quantitative verification of BNNs. Our approach introduces a native representation of BNN constraints in a custom-designed solver for qualitative reasoning, and in an approximate model counter for quantitative reasoning. We further develop specialized proof generation and checking pipelines with native support for BNN constraint reasoning, ensuring trustworthiness for all of our verification results. Empirical evaluations on a BNN robustness verification benchmark suite demonstrate that our certified solving approach achieves a $9\times$ speedup over prior certified CNF and PB-based approaches, and our certified counting approach achieves a $218\times$ speedup over the existing CNF-based baseline. In terms of coverage, our pipeline produces fully certified results for $99\%$ and $86\%$ of the qualitative and quantitative reasoning queries on BNNs, respectively. This is in sharp contrast to the best existing baselines which can fully certify only $62\%$ and $4\%$ of the queries, respectively.
- Abstract(参考訳): ニューラルネットワークは、安全クリティカルなアプリケーションにおいて不可欠なコンポーネントとして現れています。
バイナリ化ニューラルネットワーク(BNN)は、各ニューロンがブール値に制約されるニューラルネットワークの一種であり、特に安全性に問題のあるタスクには適しているが、フルスケール(浮動小数点または量子化)の深層ニューラルネットワークの計算能力の多くを維持できるが、定性検証のための満足度解決器や量的推論のためのモデルカウンタとの互換性は保たれている。
しかし,既存のBNN解析手法では,拡張性に限界があるか,音質の誤差が原因で,現実のシナリオでは適用性が低下する。
本研究では,BNNの質的,定量的な検証を行うための,スケーラブルで信頼性の高い手法を提案する。
本手法では,定性的推論のためのカスタム設計の解法と量的推論のための近似モデルカウンタに,BNN制約のネイティブ表現を導入する。
さらに、BNN制約推論をネイティブにサポートし、検証結果の信頼性を確保しながら、特別な証明生成とチェックパイプラインを開発する。
BNNのロバスト性検証ベンチマークスイートの実証評価では,従来のCNFおよびPBベースのアプローチよりも9-times$の高速化を実現し,既存のCNFベースのベースラインよりも218-times$の高速化を実現している。
我々のパイプラインは、それぞれBNNの質的および定量的推論クエリの99\%$と86\%$の完全認定結果を生成する。
これは、それぞれ62\%$と4\%$のクエリを完全に認証できる、最高の既存のベースラインとは対照的である。
関連論文リスト
- Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
グラフニューラルネットワーク(GNN)におけるラベルフリップの正確な認証手法を提案する。
本稿では,ノード分類タスクにおける広範囲なGNNアーキテクチャの認証に本手法を適用した。
私たちの研究は、ニューラルネットワークによって引き起こされた毒殺攻撃に対する最初の正確な認証を提示します。
論文 参考訳(メタデータ) (2024-11-30T17:05:12Z) - An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
量子ニューラルネットワーク(QNN)が開発され、二項化ニューラルネットワーク(BNN)は特殊なケースとしてバイナリ値に制限されている。
本稿では,指定された特性を満たすBNNの自動合成手法を提案する。
論文 参考訳(メタデータ) (2023-07-29T06:27:28Z) - Adversarial Robustness Certification for Bayesian Neural Networks [22.71265211510824]
逆入力摂動に対するベイズニューラルネットワーク(BNN)の計算の堅牢性検証問題について検討する。
本フレームワークは, 重み付け, 積分, および有界伝搬技術に基づいており, 多数のパラメータを持つBNNに適用可能である。
論文 参考訳(メタデータ) (2023-06-23T16:58:25Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - 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) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳(メタデータ) (2022-04-01T03:31:27Z) - Robustness of Bayesian Neural Networks to White-Box Adversarial Attacks [55.531896312724555]
ベイジアンネットワーク(BNN)は、ランダム性を組み込むことで、敵の攻撃を扱うのに頑丈で適している。
我々はベイズ的推論(つまり変分ベイズ)をDenseNetアーキテクチャに融合させることで、BNN-DenseNetと呼ばれるBNNモデルを作成する。
逆向きに訓練されたBNNは、ほとんどの実験で非ベイズ的で逆向きに訓練されたBNNよりも優れています。
論文 参考訳(メタデータ) (2021-11-16T16:14:44Z) - Certification of Iterative Predictions in Bayesian Neural Networks [79.15007746660211]
我々は、BNNモデルの軌道が与えられた状態に到達する確率に対して、安全でない状態の集合を避けながら低い境界を計算する。
我々は、制御と強化学習の文脈において、下限を用いて、与えられた制御ポリシーの安全性保証を提供する。
論文 参考訳(メタデータ) (2021-05-21T05:23:57Z) - BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized
Neural Networks [7.844146033635129]
一般実数ニューラルネットワークの1ビット量子化であるBinarized Neural Networks(BNNs)の検証問題について検討する。
我々のアプローチは,BNNの内部構造を利用して,BNNをBDD(Bibinary Decision Diagram)にエンコードすることである。
符号化に基づいて,BNNの高精度かつ包括的分析が可能なBNNの定量的検証フレームワークを開発する。
論文 参考訳(メタデータ) (2021-03-12T12:02:41Z) - S2-BNN: Bridging the Gap Between Self-Supervised Real and 1-bit Neural
Networks via Guided Distribution Calibration [74.5509794733707]
本研究では, 実数値から, 最終予測分布上のバイナリネットワークへの誘導型学習パラダイムを提案する。
提案手法は,bnn上で5.515%の絶対利得で,単純なコントラスト学習ベースラインを向上できる。
提案手法は、単純なコントラスト学習ベースラインよりも大幅に改善され、多くの主流教師付きBNN手法に匹敵する。
論文 参考訳(メタデータ) (2021-02-17T18:59:28Z) - Incorporating Interpretable Output Constraints in Bayesian Neural
Networks [34.103445420814644]
出力制約付きBNN(OC-BNN)は不確実性定量化のためのベイズフレームワークと完全に一致している。
我々は、医療、刑事司法、信用スコアなどの複数の領域にまたがる実世界のデータセットに対するOC-BNNの有効性を実証する。
論文 参考訳(メタデータ) (2020-10-21T13:00:05Z) - Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。
本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。
われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
論文 参考訳(メタデータ) (2020-02-17T09:53:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。