論文の概要: Branch and Bound for Piecewise Linear Neural Network Verification

• arxiv url: http://arxiv.org/abs/1909.06588v5
• Date: Tue, 26 Aug 2025 14:58:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-31 21:54:20.503576
• Title: Branch and Bound for Piecewise Linear Neural Network Verification
• Title（参考訳）: 線形ニューラルネットワーク検証のための分岐と境界
• Authors: Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, M. Pawan Kumar,
• Abstract要約: ブランチ・アンド・バウンド(BaB)に基づくアルゴリズム群を提案する。 複数の既存手法の強みを組み合わせた新しい手法を同定する。 我々はReLUの非線形性に効果的な分岐戦略を導入する。
• 参考スコア（独自算出の注目度）: 46.49816596173425
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The success of Deep Learning and its potential use in many safety-critical applications has motivated research on formal verification of Neural Network (NN) models. In this context, verification involves proving or disproving that an NN model satisfies certain input-output properties. Despite the reputation of learned NN models as black boxes, and the theoretical hardness of proving useful properties about them, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure and taking insights from formal methods such as Satisifiability Modulo Theory. However, these methods are still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we exploit the Mixed Integer Linear Programming (MIP) formulation of verification to propose a family of algorithms based on Branch-and-Bound (BaB). We show that our family contains previous verification methods as special cases. With the help of the BaB framework, we make three key contributions. Firstly, we identify new methods that combine the strengths of multiple existing approaches, accomplishing significant performance improvements over previous state of the art. Secondly, we introduce an effective branching strategy on ReLU non-linearities. This branching strategy allows us to efficiently and successfully deal with high input dimensional problems with convolutional network architecture, on which previous methods fail frequently. Finally, we propose comprehensive test data sets and benchmarks which includes a collection of previously released testcases. We use the data sets to conduct a thorough experimental comparison of existing and new algorithms and to provide an inclusive analysis of the factors impacting the hardness of verification problems.
• Abstract（参考訳）: ディープラーニングの成功と、多くの安全クリティカルなアプリケーションにおける潜在的な使用は、ニューラルネットワーク(NN)モデルの形式的検証を動機付けている。 この文脈では、検証は、NNモデルが特定の入出力特性を満たすことを証明または証明することを伴う。 学習したNNモデルをブラックボックスとして評価し、それらの有用性を証明する理論的な困難さにもかかわらず、研究者はそれらの断片的な線形構造を利用し、Satiifiability Modulo Theoryのような形式的な手法から洞察を得ることによってモデルのクラスを検証することに成功している。 しかし、これらの手法は依然として、スケーリングから現実的なニューラルネットワークには程遠い。 この重要な領域の進展を促進するために、検証のMIP(Mixed Integer Linear Programming)の定式化を利用して、ブランチ・アンド・バウンド(BaB)に基づくアルゴリズム群を提案する。 本研究は, 過去の検証手法を特殊な事例として含んでいることを示す。 BaBフレームワークの助けを借りて、私たちは3つの重要な貢献をしています。 まず、複数の既存手法の強みを組み合わせた新しい手法を特定し、従来の最先端技術よりも大幅な性能向上を実現した。 第2に、ReLUの非線形性に効果的な分岐戦略を導入する。 この分岐戦略により、従来の手法が頻繁に失敗する畳み込みネットワークアーキテクチャにおいて、高入力次元問題に効率よく、かつうまく対処できる。 最後に、以前にリリースされたテストケースの集合を含む包括的なテストデータセットとベンチマークを提案する。 このデータセットを用いて、既存のアルゴリズムと新しいアルゴリズムを徹底的に実験的に比較し、検証問題の硬さに影響を与える要因を包括的に分析する。

関連論文リスト

• SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
  本研究は,デザイナ・ちょうせん特性を満たすことが保証される識別可能なMLモデルを訓練する作業について考察する。 現代のニューラルモデルにおけるコンプライアンスの厳格な検証と実施という計算複雑性のため、これは非常に難しい。 1)保守的なセマンティクスによる効率的な検証を可能にする汎用的,シンプルなアーキテクチャ。 回帰における線形不等式によって定義される特性と、多重ラベル分類における相互排他的クラスに対するアプローチを評価する。
  論文  参考訳（メタデータ） (2024-09-30T17:19:57Z)
• Visual Prompting Upgrades Neural Network Sparsification: A Data-Model Perspective [64.04617968947697]
  より優れた重量空間を実現するために、新しいデータモデル共設計視点を導入する。 具体的には、提案したVPNフレームワークでニューラルネットワークのスパーシフィケーションをアップグレードするために、カスタマイズされたVisual Promptが実装されている。
  論文  参考訳（メタデータ） (2023-12-03T13:50:24Z)
• Inductive Knowledge Graph Completion with GNNs and Rules: An Analysis [18.11743347414004]
  ルールベース手法はグラフニューラルネットワーク(GNN)に基づく最先端手法を著しく上回る 本稿では,前述の問題に対処することを目的としたルールベースアプローチのバリエーションについて検討する。 その結果,NBFNetに近い性能が得られることがわかった。
  論文  参考訳（メタデータ） (2023-08-14T21:01: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)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  本研究は,NFに基づく多次元条件(後)密度推定器の検証診断を容易にすることを提案する。 また、局所的な一貫性の結果に基づいた理論的保証も提供する。 この作業は、より良い特定モデルの設計を支援したり、新しいSBIアルゴリズムの開発を促進するのに役立つだろう。
  論文  参考訳（メタデータ） (2022-11-17T15:48:06Z)
• Gone Fishing: Neural Active Learning with Fisher Embeddings [55.08537975896764]
  ディープニューラルネットワークと互換性のあるアクティブな学習アルゴリズムの必要性が高まっている。 本稿では,ニューラルネットワークのための抽出可能かつ高性能な能動学習アルゴリズムBAITを紹介する。
  論文  参考訳（メタデータ） (2021-06-17T17:26:31Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)
• Designing Interpretable Approximations to Deep Reinforcement Learning [14.007731268271902]
  ディープニューラルネットワーク(DNN)は、アルゴリズムのパフォーマンスのバーを設定する。 実際にそのようなハイパフォーマンスなDNNを使うことは不可能かもしれない。 この研究は、所望のパフォーマンスレベルを保持するだけでなく、例えば、DNNで表される潜伏した知識を簡潔に説明できるような縮小モデルを特定することを目指している。
  論文  参考訳（メタデータ） (2020-10-28T06:33:09Z)
• Rethinking Generalization of Neural Models: A Named Entity Recognition Case Study [81.11161697133095]
  NERタスクをテストベッドとして、異なる視点から既存モデルの一般化挙動を分析する。 詳細な分析による実験は、既存のニューラルNERモデルのボトルネックを診断する。 本論文の副産物として,最近のNER論文の包括的要約を含むプロジェクトをオープンソース化した。
  論文  参考訳（メタデータ） (2020-01-12T04:33:53Z)

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

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