論文の概要: Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers

• arxiv url: http://arxiv.org/abs/2011.13824v2
• Date: Tue, 16 Mar 2021 16:35:00 GMT
• ステータス: 処理完了
• システム内更新日: 2022-09-20 01:38:04.671381
• Title: Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Title（参考訳）: fast and complete: rapid and massively parallel incomplete verifiersによる完全ニューラルネットワーク検証の実現
• Authors: Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, Cho-Jui Hsieh
• Abstract要約: BaB プロセス中に線形計画法 (LP) を置き換えるために, 逆モード線形緩和に基づく解析法 (LiRPA) を提案する。 LPとは異なり、LiRPAを適用すると、より弱い境界が得られ、分割時にサブドメインのコンフリクトをチェックすることもできない。 既存のLPベースのアプローチと比較して、桁違いのスピードアップを示す。
• 参考スコア（独自算出の注目度）: 112.23981192818721
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of neural networks (NNs) is a challenging and important problem. Existing efficient complete solvers typically require the branch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such as Linear Programming (LP) on linearly relaxed sub-domains. In this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typical machine learning accelerators such as GPUs and TPUs. However, unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire procedure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On a single GPU, we demonstrate an order of magnitude speedup compared to existing LP-based approaches.
• Abstract（参考訳）: ニューラルネットワーク(NN)の形式的検証は困難で重要な問題である。 既存の効率的な完全解法は分岐とバウンド(BaB)プロセスを必要とするが、これは問題領域をサブドメインに分割し、線形に緩和されたサブドメイン上の線形プログラミング(LP)のようなより高速だが弱い不完全な検証器を用いて各サブドメインを解く。 本稿では,gpuやtpusなどの一般的な機械学習アクセラレータ上で効率的に実装可能なbabプロセス中にlpを置き換えるために,逆モード線形緩和に基づく摂動解析(lirpa)を提案する。 しかし、LPとは異なり、LiRPAが適用されると、より弱い境界が生成され、分割時にサブドメインのコンフリクトをチェックできないため、BaB後に手続き全体が不完全となる。 これらの課題に対処すべく,高速な勾配に基づく境界引き締め手順とバッチ分割を併用し,lpバウンドプロシージャの最小使用法の設計を行い,lpベースアプローチを著しく上回るような完全なnn検証問題に対して,アクセラレータハードウェア上でlirpaを効果的に使用することを可能にした。 1つのGPU上では、既存のLPベースのアプローチと比較して桁違いのスピードアップを示す。

関連論文リスト

• A Learned Proximal Alternating Minimization Algorithm and Its Induced Network for a Class of Two-block Nonconvex and Nonsmooth Optimization [4.975853671529418]
  本研究では,学習可能な2ブロック非平滑問題の解法として,一般学習型交互最小化アルゴリズムLPAMを提案する。 提案するLPAM-netはパラメータ効率が高く,いくつかの最先端手法と比較して良好な性能を示す。
  論文  参考訳（メタデータ） (2024-11-10T02:02:32Z)
• OptEx: Expediting First-Order Optimization with Approximately Parallelized Iterations [12.696136981847438]
  ほぼ並列化されたイテレーション (OptEx) で高速化された一階最適化を導入する。 OptExは、並列コンピューティングを活用して、その反復的ボトルネックを軽減することで、FOOの効率を高める最初のフレームワークである。 我々は、カーネル化された勾配推定の信頼性とSGDベースのOpsExの複雑さを理論的に保証する。
  論文  参考訳（メタデータ） (2024-02-18T02:19:02Z)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  本稿では,ニューラルネットワークトレーニングを安定化(大規模)するための原理的手法として,線形アヘッドの理論解析を提案する。 最適化過程の不安定性は、しばしば損失ランドスケープの非単調性によって引き起こされるものであり、非拡張作用素の理論を活用することによって線型性がいかに役立つかを示す。
  論文  参考訳（メタデータ） (2023-10-20T12:45:12Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。 活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。 BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
  論文  参考訳（メタデータ） (2021-04-14T09:22:42Z)
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification [151.62491805851107]
  私たちは、ニューロン毎の分割を完全にエンコードできるバウンド伝搬ベースの検証器である$beta$-crownを開発した。 Beta$-CROWNはLPベースのBaB法よりも3桁近い速さで堅牢性検証が可能です。 BaBを早期に終了することにより、不完全な検証にも使用できます。
  論文  参考訳（メタデータ） (2021-03-11T11:56:54Z)
• Activation Relaxation: A Local Dynamical Approximation to Backpropagation in the Brain [62.997667081978825]
  活性化緩和(AR)は、バックプロパゲーション勾配を力学系の平衡点として構成することで動機付けられる。 我々のアルゴリズムは、正しいバックプロパゲーション勾配に迅速かつ堅牢に収束し、単一のタイプの計算単位しか必要とせず、任意の計算グラフで操作できる。
  論文  参考訳（メタデータ） (2020-09-11T11:56:34Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

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

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