論文の概要: Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification

• arxiv url: http://arxiv.org/abs/2603.14823v1
• Date: Mon, 16 Mar 2026 04:57:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-17 16:19:36.05683
• Title: Counterexample Guided Branching via Directional Relaxation Analysis in Complete Neural Network Verification
• Title（参考訳）: 完全ニューラルネットワーク検証における方向緩和解析による正解分岐法
• Authors: Jingyang Li, Fu Song, Guoqiang Li,
• Abstract要約: ディープニューラルネットワークは例外的な性能を示すが、敵の摂動に弱いままである。 現在のデータフローアプローチは、静的に依存するブラインドリファインメントプロセスで動作する。 本稿では,Falsification に積極的に寄与するニューロンの分岐を優先する Directional Gap を導入するフレームワーク DRG-BaB を提案する。
• 参考スコア（独自算出の注目度）: 10.808953992870954
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Deep Neural Networks demonstrate exceptional performance but remain vulnerable to adversarial perturbations, necessitating formal verification for safety-critical deployment. To address the computational complexity of this task, researchers often employ abstraction-refinement techniques that iteratively tighten an over-approximated model. While structural methods utilize Counterexample-Guided Abstraction Refine- ment, state-of-the-art dataflow verifiers typically rely on Branch-and-Bound to refine numerical convex relaxations. However, current dataflow approaches operate with blind refinement processes that rely on static heuristics and fail to leverage specific diagnostic information from verification failures. In this work, we argue that Branch-and-Bound should be reformulated as a Dataflow CEGAR loop where the spurious counterexample serves as a precise witness to local abstraction errors. We propose DRG-BaB, a framework that introduces the Directional Relaxation Gap heuristic to prioritize branching on neurons actively contributing to falsification in the abstract domain. By deriving a closed-form spurious counterexample directly from linear bounds, our method transforms generic search into targeted refinement. Experiments on high-dimensional benchmarks demonstrate that this approach significantly reduces search tree size and verification time compared to established baselines.
• Abstract（参考訳）: ディープニューラルネットワークは、例外的なパフォーマンスを示すが、敵の摂動に弱いままであり、安全クリティカルなデプロイメントの正式な検証を必要とする。 このタスクの計算複雑性に対処するために、研究者はしばしば過近似モデルを反復的に締め付ける抽象リファインメント技術を用いる。 構造的手法は反例ガイドによる抽象的再定義を利用するが、最先端のデータフロー検証は一般に分岐とバウンドに依存して数値凸緩和を洗練させる。 しかし、現在のデータフローアプローチは、静的ヒューリスティックに依存し、検証失敗から特定の診断情報を活用できないブラインド改善プロセスで動作する。 本研究では,ブランチ・アンド・バウンドをデータフロー CEGAR ループとして再編成すべきである,と論じる。 DRG-BaBは方向緩和ギャップヒューリスティック(Directional Relaxation Gap Heuristic)を導入し、抽象領域におけるファルシフィケーションに積極的に寄与するニューロンへの分岐を優先するフレームワークである。 線形境界から直接閉形式のスプリアス反例を導出することにより,ジェネリックサーチを対象の洗練に変換する。 高次元ベンチマーク実験により,本手法が確立された基準線に比べて探索木の大きさと検証時間を著しく短縮することが示された。

関連論文リスト

• Efficient Discovery of Approximate Causal Abstractions via Neural Mechanism Sparsification [0.0]
  ニューラルネットワークは解釈可能な因果機構を実装すると仮定される。 これを検証するには、因果抽象化を見つける必要があります -- 介入の下でネットワークに忠実な、よりシンプルでハイレベルな構造因果モデル(SCM)です。 我々は、構造的プルーニングを近似抽象の探索として見ることによって問題を再構築した。
  論文  参考訳（メタデータ） (2026-02-27T18:35:10Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  我々は, 正規サンプルの分布を低次元多様体で支持する異常検出において, 特定のユースケースに焦点を当てた。 我々は、訓練中に識別情報を活用する自己指導型学習体制に適応するが、通常の例のサブ多様体に焦点をあてる。 製造領域における視覚異常検出のための挑戦的なベンチマークであるMVTec ADデータセットで、最先端の新たな結果を達成する。
  論文  参考訳（メタデータ） (2022-06-23T14:16:30Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。 この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。 本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-06-08T04:09:13Z)

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

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