論文の概要: Lagrangian Decomposition for Neural Network Verification
- arxiv url: http://arxiv.org/abs/2002.10410v3
- Date: Wed, 17 Jun 2020 17:49:58 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-29 03:10:00.191084
- Title: Lagrangian Decomposition for Neural Network Verification
- Title(参考訳): ニューラルネットワーク検証のためのラグランジアン分解
- Authors: Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy
Dvijotham, Pushmeet Kohli, Philip H.S. Torr, M. Pawan Kumar
- Abstract要約: ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。
ラグランジアン分解に基づく新しい手法を提案する。
ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
- 参考スコア(独自算出の注目度): 148.0448557991349
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: A fundamental component of neural network verification is the computation of
bounds on the values their outputs can take. Previous methods have either used
off-the-shelf solvers, discarding the problem structure, or relaxed the problem
even further, making the bounds unnecessarily loose. We propose a novel
approach based on Lagrangian Decomposition. Our formulation admits an efficient
supergradient ascent algorithm, as well as an improved proximal algorithm. Both
the algorithms offer three advantages: (i) they yield bounds that are provably
at least as tight as previous dual algorithms relying on Lagrangian
relaxations; (ii) they are based on operations analogous to forward/backward
pass of neural networks layers and are therefore easily parallelizable,
amenable to GPU implementation and able to take advantage of the convolutional
structure of problems; and (iii) they allow for anytime stopping while still
providing valid bounds. Empirically, we show that we obtain bounds comparable
with off-the-shelf solvers in a fraction of their running time, and obtain
tighter bounds in the same time as previous dual algorithms. This results in an
overall speed-up when employing the bounds for formal verification. Code for
our algorithms is available at
https://github.com/oval-group/decomposition-plnn-bounds.
- Abstract(参考訳): ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンドの計算である。
従来の手法では、既定の解法を使ったり、問題構造を捨てたり、問題をさらに緩和したりして、境界を不必要にゆるめたりしている。
我々はラグランジアン分解に基づく新しいアプローチを提案する。
この定式化は,高効率な超次昇降アルゴリズムと改良された近位アルゴリズムを認めている。
どちらのアルゴリズムも3つの利点があります
(i)ラグランジュ緩和に依拠して、少なくとも以前の双対アルゴリズムと同程度に密接な境界を与える。
(ii)それらは、ニューラルネットワーク層のフォワード/バックパスに類似した操作に基づいており、容易に並列化でき、gpuの実装に適合し、問題の畳み込み構造を活用できる。
(iii)有効限度を保ちながら、いつでも停止できる。
実験の結果,本論文では,本論文では,本論文の解法に匹敵する解法が実行時間の一部で得られ,従来の2重アルゴリズムと同時期により厳密な解法が得られた。
これにより、形式検証に境界を用いる場合の全体的なスピードアップが実現される。
私たちのアルゴリズムのコードはhttps://github.com/oval-group/decomposition-plnn-boundsで利用可能です。
関連論文リスト
- Infeasible Deterministic, Stochastic, and Variance-Reduction Algorithms for Optimization under Orthogonality Constraints [9.301728976515255]
本稿では,着陸アルゴリズムの実用化と理論的展開について述べる。
まず、この方法はスティーフェル多様体に拡張される。
また、コスト関数が多くの関数の平均である場合の分散還元アルゴリズムについても検討する。
論文 参考訳(メタデータ) (2023-03-29T07:36:54Z) - Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
我々は、制約付き最適化のための一階アルゴリズムと非滑らかなシステムの間で、新しい一階アルゴリズムのクラスを設計する。
これらのアルゴリズムの重要な性質は、制約がスパース変数の代わりに速度で表されることである。
論文 参考訳(メタデータ) (2023-02-01T08:50:48Z) - Block-coordinate Frank-Wolfe algorithm and convergence analysis for
semi-relaxed optimal transport problem [20.661025590877774]
凸半緩和最適輸送(OT)問題に対する高速ブロックコーディネートFrank-Wolfe (BCFW) アルゴリズムを提案する。
数値実験により,提案アルゴリズムはカラー転送に有効であり,最先端のアルゴリズムを超越することを示した。
論文 参考訳(メタデータ) (2022-05-27T05:54:45Z) - Lower Bounds and Optimal Algorithms for Smooth and Strongly Convex
Decentralized Optimization Over Time-Varying Networks [79.16773494166644]
通信ネットワークのノード間を分散的に保存するスムーズで強い凸関数の和を最小化するタスクについて検討する。
我々は、これらの下位境界を達成するための2つの最適アルゴリズムを設計する。
我々は,既存の最先端手法と実験的な比較を行うことにより,これらのアルゴリズムの理論的効率を裏付ける。
論文 参考訳(メタデータ) (2021-06-08T15:54:44Z) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳(メタデータ) (2021-04-14T09:22:42Z) - Scaling the Convex Barrier with Sparse Dual Algorithms [141.4085318878354]
本稿では,ニューラルネットワークバウンダリングのための2つの新しい2重アルゴリズムを提案する。
どちらの方法も新しい緩和の強さを回復する: 厳密さと線形分離オラクル。
実行時間のほんの一部で、既製のソルバよりも優れた境界を得ることができます。
論文 参考訳(メタデータ) (2021-01-14T19:45:17Z) - An Asymptotically Optimal Primal-Dual Incremental Algorithm for
Contextual Linear Bandits [129.1029690825929]
複数の次元に沿った最先端技術を改善する新しいアルゴリズムを提案する。
非文脈線形帯域の特別な場合において、学習地平線に対して最小限の最適性を確立する。
論文 参考訳(メタデータ) (2020-10-23T09:12:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。