論文の概要: E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching
- arxiv url: http://arxiv.org/abs/2602.05068v1
- Date: Wed, 04 Feb 2026 21:42:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-06 18:49:08.63073
- Title: E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching
- Title（参考訳）: E-Globe: タイトな上界とパターン認識分岐によるニューラルネットワークのスケーラブルな$ε$-Global検証
- Authors: Wenting Li, Saif R. Kazi, Russell Bent, Duo Zhou, Huan Zhang,
- Abstract要約: 形式的検証は堅牢性を保証するが、現在のメソッドはスケーラビリティと完全性というトレードオフに直面している。
我々は,$$$globalの最適値に到達するか,早期停止を起動するまで,上界と下界を効率的に締め付けるハイブリッド検証器を提案する。
- 参考スコア（独自算出の注目度）: 9.161865803917847
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Neural networks achieve strong empirical performance, but robustness concerns still hinder deployment in safety-critical applications. Formal verification provides robustness guarantees, but current methods face a scalability-completeness trade-off. We propose a hybrid verifier in a branch-and-bound (BaB) framework that efficiently tightens both upper and lower bounds until an $ε-$global optimum is reached or early stop is triggered. The key is an exact nonlinear program with complementarity constraints (NLP-CC) for upper bounding that preserves the ReLU input-output graph, so any feasible solution yields a valid counterexample and enables rapid pruning of unsafe subproblems. We further accelerate verification with (i) warm-started NLP solves requiring minimal constraint-matrix updates and (ii) pattern-aligned strong branching that prioritizes splits most effective at tightening relaxations. We also provide conditions under which NLP-CC upper bounds are tight. Experiments on MNIST and CIFAR-10 show markedly tighter upper bounds than PGD across perturbation radii spanning up to three orders of magnitude, fast per-node solves in practice, and substantial end-to-end speedups over MIP-based verification, amplified by warm-starting, GPU batching, and pattern-aligned branching.
- Abstract（参考訳）: ニューラルネットワークは、強い経験的性能を達成するが、ロバスト性に関する懸念は、安全クリティカルなアプリケーションのデプロイを妨げている。
形式的検証は堅牢性を保証するが、現在のメソッドはスケーラビリティと完全性というトレードオフに直面している。
本稿では, ε-$global の最適値に到達するか, 早期停止を起動するまで, 上界と下界の両方を効率的に締め付ける分岐結合(BaB)フレームワークのハイブリッド検証器を提案する。
鍵は、ReLU入力出力グラフを保存する上界の相補性制約(NLP-CC)を持つ正確な非線形プログラムであり、任意の実現可能な解は有効な反例となり、安全でないサブプロブレムの迅速なプルーニングを可能にする。
私たちはさらに検証を加速します
(i)ウォームスタートしたNLPは最小限の制約行列更新を必要とする。
(II) 分割を優先するパターン整列強い分岐は緩和の強化に最も効果的である。
また, NLP-CC上界がきつい条件も提示する。
MNISTとCIFAR-10の実験では、最大3桁の摂動半径にまたがるPGDよりもはるかに高い上限、高速なノード毎の解法、MIPベースの検証よりも相当なエンドツーエンドのスピードアップ、ウォームスタート、GPUバッチ、パターン整列によって増幅された。
関連論文リスト
- Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
我々は無益な無益な提案をする。
承認されたトークンの数を大幅に増加させる検証方法。
HSDは様々なモデルファミリやベンチマークの受け入れ率に一貫した改善をもたらすことを示す。
論文 参考訳（メタデータ） (2026-01-09T11:10:29Z) - Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
最先端ニューラルネットワーク(NN)検証は、分岐とバウンド(BaB)の手順を高速なバウンディング技術で適用することが、多くの挑戦的な検証特性に対処する上で重要な役割を果たしていることを示す。
本稿では,NN検証の有効性を高めるために,スケーラブルで効率的な手法のクラスである線形制約駆動型クリッピングフレームワークを紹介する。
論文 参考訳（メタデータ） (2025-12-11T19:59:37Z) - Scalable First-order Method for Certifying Optimal k-Sparse GLMs [9.613635592922174]
そこで本研究では,BnBフレームワークの視点緩和を解くために,一階近位勾配アルゴリズムを提案する。
提案手法は双有界計算を著しく高速化し,大規模問題に対する最適性証明の提供に極めて有効であることを示す。
論文 参考訳（メタデータ） (2025-02-13T17:14:18Z) - Robust Stochastically-Descending Unrolled Networks [85.6993263983062]
Deep Unrolling(ディープ・アンローリング)は、トレーニング可能なニューラルネットワークの層に切り捨てられた反復アルゴリズムをアンロールする、新たな学習最適化手法である。
アンロールネットワークの収束保証と一般化性は、いまだにオープンな理論上の問題であることを示す。
提案した制約の下で訓練されたアンロールアーキテクチャを2つの異なるアプリケーションで数値的に評価する。
論文 参考訳（メタデータ） (2023-12-25T18:51:23Z) - Achieving Constraints in Neural Networks: A Stochastic Augmented
Lagrangian Approach [49.1574468325115]
DNN(Deep Neural Networks)の正規化は、一般化性の向上とオーバーフィッティングの防止に不可欠である。
制約付き最適化問題としてトレーニングプロセスのフレーミングによるDNN正規化に対する新しいアプローチを提案する。
我々はAugmented Lagrangian (SAL) 法を用いて、より柔軟で効率的な正規化機構を実現する。
論文 参考訳（メタデータ） (2023-10-25T13:55:35Z) - Fast Global Convergence of Policy Optimization for Constrained MDPs [17.825031573375725]
勾配法は最適性ギャップと制約違反の両方に対して$mathcalO(log(T)/T)$大域収束率が得られることを示す。
スレーターの条件が満たされ、事前条件が知られているとき、十分大きなT$に対してゼロ制約違反がさらに保証される。
論文 参考訳（メタデータ） (2021-10-31T17:46:26Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳（メタデータ） (2021-04-14T09:22:42Z) - Fast and Complete: Enabling Complete Neural Network Verification with
Rapid and Massively Parallel Incomplete Verifiers [112.23981192818721]
BaB プロセス中に線形計画法 (LP) を置き換えるために, 逆モード線形緩和に基づく解析法 (LiRPA) を提案する。
LPとは異なり、LiRPAを適用すると、より弱い境界が得られ、分割時にサブドメインのコンフリクトをチェックすることもできない。
既存のLPベースのアプローチと比較して、桁違いのスピードアップを示す。
論文 参考訳（メタデータ） (2020-11-27T16:42:12Z) - On Lower Bounds for Standard and Robust Gaussian Process Bandit
Optimization [55.937424268654645]
有界ノルムを持つ関数のブラックボックス最適化問題に対するアルゴリズム非依存な下界を考える。
本稿では, 単純さ, 汎用性, エラー確率への依存性の向上など, 後悔の下位境界を導出するための新しい証明手法を提案する。
論文 参考訳（メタデータ） (2020-08-20T03:48:14Z) - PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier [1.1011268090482575]
我々は、ReLU NNの最も一般的な安全仕様を正式に検証するための新しいアプローチを導入する。
我々は, 線形実現可能性チェッカーとしてだけでなく, 解法で許容される緩和量のペナルティ化の手段として, 凸解法を用いる。
論文 参考訳（メタデータ） (2020-06-18T21:33:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。