論文の概要: Branch and Bound for Relational Verification of Neural Networks
- arxiv url: http://arxiv.org/abs/2608.13118v1
- Date: Thu, 13 Aug 2026 11:47:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 18:29:38.507948
- Title: Branch and Bound for Relational Verification of Neural Networks
- Title（参考訳）: ニューラルネットワークの相関検証のための分岐と境界
- Abstract要約: グローバルロバストネスなどのリレーショナル仕様に対するニューラルネットワークの検証は、サイバー物理システムの安全クリティカルな応用に不可欠である。
問題を軽減するための分岐結合(BaB)フレームワークを提案し、全てのサブプロブレムが検証されるまで反復的に問題を分割する。
我々は,ACAS Xu,MNIST-F,MNIST-C,CIFAR,GTSRBの817の検証問題に対するSaBReの評価を行った。
- 参考スコア（独自算出の注目度）: 2.593237301046536
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.
- Abstract（参考訳）: グローバルロバストネスなどのリレーショナル仕様に対するニューラルネットワークの検証は、AIコンポーネントの採用が増加していることを考えると、サイバー物理システム(CPS)の安全クリティカルな応用に不可欠である。
単純なトレース特性(例えば、局所ロバスト性)と比較して、関係性仕様を検証するには、複数のネットワーク推論の関係について推論する必要がある。
既存の研究では、ニューラルネットワーク出力の音響および凸過近似に基づく抽象化技術について検討されてきたが、これらのアプローチは本質的に不完全であり、誤報を引き起こす可能性があるため、効果的な抽象化改善の必要性をさらに強調している。
本稿では,問題を軽減するための分岐結合(BaB)フレームワークを提案し,全てのサブプロブレムが検証されるまで繰り返し分割する。
特に,我々のBaBフレームワークは,従来の作業のように個々のニューロンではなくリレーショナルニューロンの分割を特徴としており,本手法のコアとして,検証問題の二重定式化に基づくリレーショナルニューロン選択戦略を考案し,問題分割による洗練を最大化する(おそらく)最適リレーショナルニューロンを効率的に選択することができるようにした。
我々は,ACAS Xu,MNIST-F,MNIST-C,CIFAR,GTSRBの817の検証問題に対するSaBReの評価を行った。
その結果,SaBReは,解決されたインスタンス数や検証効率の観点から,異なるベースラインアプローチよりも優れており,提案手法の有効性が示された。
関連論文リスト
- Constraints Matrix Diffusion based Generative Neural Solver for Vehicle Routing Problems [16.541111954252397]
本稿では、離散ノイズグラフ拡散モデルを用いて車両ルーティング問題の根底にある制約を学習する新しい融合ニューラルネットワークフレームワークを提案する。
この研究は、378の組合せ空間にわたるニューラルネットワークモデルの解法に関する、初めての総合的な実験的研究である。
論文 参考訳（メタデータ） (2026-03-08T10:03:34Z) - Verification of Bit-Flip Attacks against Quantized Neural Networks [14.673682037450321]
我々は,ビットフリップ攻撃の欠如を正式に検証するための最初の検証フレームワークであるBFAVerifierを紹介する。
BFAVerifierは抽象的手法とMILP的手法の2つの積分成分からなる。
論文 参考訳（メタデータ） (2025-02-22T16:35:38Z) - Implicit Generative Prior for Bayesian Neural Networks [8.013264410621357]
複雑なデータ構造のための新しいニューラルネットワーク型経験ベイズ(NA-EB)フレームワークを提案する。
NA-EBフレームワークは変分推論と勾配上昇アルゴリズムを組み合わせたものである。
各種タスクの広範囲な評価を通じて,本フレームワークの実践的応用を実証する。
論文 参考訳（メタデータ） (2024-04-27T21:00:38Z) - Zonotope Domains for Lagrangian Neural Network Verification [102.13346781220383]
我々は、ディープニューラルネットワークを多くの2層ニューラルネットワークの検証に分解する。
我々の手法は線形プログラミングとラグランジアンに基づく検証技術の両方により改善された境界を与える。
論文 参考訳（メタデータ） (2022-10-14T19:31:39Z) - Knowledge Enhanced Neural Networks for relational domains [83.9217787335878]
我々は、ニューラルネットワークに事前論理的知識を注入するニューラルネットワークアーキテクチャであるKENNに焦点を当てる。
本稿では,関係データに対するKENNの拡張を提案する。
論文 参考訳（メタデータ） (2022-05-31T13:00:34Z) - Generalization of Neural Combinatorial Solvers Through the Lens of
Adversarial Robustness [68.97830259849086]
ほとんどのデータセットは単純なサブプロブレムのみをキャプチャし、おそらくは突発的な特徴に悩まされる。
本研究では, 局所的な一般化特性である対向ロバスト性について検討し, 厳密でモデル固有な例と突発的な特徴を明らかにする。
他のアプリケーションとは異なり、摂動モデルは知覚できないという主観的な概念に基づいて設計されているため、摂動モデルは効率的かつ健全である。
驚くべきことに、そのような摂動によって、十分に表現力のあるニューラルソルバは、教師あり学習で共通する正確さと悪質さのトレードオフの限界に悩まされない。
論文 参考訳（メタデータ） (2021-10-21T07:28:11Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳（メタデータ） (2021-04-14T09:22:42Z) - Online neural connectivity estimation with ensemble stimulation [5.156484100374058]
スパースネットワークにおけるこのプロセスの効率を大幅に向上させる,ノイズの多いグループテストに基づく手法を提案する。
人口規模に比例して対数的にしか成長しない多数のテストにより、二項化ネットワーク接続を回復可能であることを示す。
また、ネット上の数万のニューロンのネットワークに対して、接続性を推測する可能性も示しています。
論文 参考訳（メタデータ） (2020-07-27T23:47:03Z) - Parallelization Techniques for Verifying Neural Networks [52.917845265248744]
検証問題に基づくアルゴリズムを反復的に導入し、2つの分割戦略を探索する。
また、ニューラルネットワークの検証問題を単純化するために、ニューロンアクティベーションフェーズを利用する、高度に並列化可能な前処理アルゴリズムも導入する。
論文 参考訳（メタデータ） (2020-04-17T20:21:47Z) - Branch and Bound for Piecewise Linear Neural Network Verification [46.49816596173425]
ブランチ・アンド・バウンド(BaB)に基づくアルゴリズム群を提案する。
複数の既存手法の強みを組み合わせた新しい手法を同定する。
我々はReLUの非線形性に効果的な分岐戦略を導入する。
論文 参考訳（メタデータ） (2019-09-14T12:44:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。