論文の概要: General Cutting Planes for Bound-Propagation-Based Neural Network Verification

• arxiv url: http://arxiv.org/abs/2208.05740v1
• Date: Thu, 11 Aug 2022 10:31:28 GMT
• ステータス: 処理完了
• システム内更新日: 2022-08-12 12:49:22.793259
• Title: General Cutting Planes for Bound-Propagation-Based Neural Network Verification
• Title（参考訳）: 境界伝達型ニューラルネットワーク検証のための一般切断平面
• Authors: Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter
• Abstract要約: 任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。 本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
• 参考スコア（独自算出の注目度）: 144.7290035694459
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Bound propagation methods, when combined with branch and bound, are among the most effective methods to formally verify properties of deep neural networks such as correctness, robustness, and safety. However, existing works cannot handle the general form of cutting plane constraints widely accepted in traditional solvers, which are crucial for strengthening verifiers with tightened convex relaxations. In this paper, we generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints, including those involving relaxed integer variables that do not appear in existing bound propagation formulations. Our generalized bound propagation method, GCP-CROWN, opens up the opportunity to apply general cutting plane methods} for neural network verification while benefiting from the efficiency and GPU acceleration of bound propagation methods. As a case study, we investigate the use of cutting planes generated by off-the-shelf mixed integer programming (MIP) solver. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers using our new formulation. Since the branching-focused bound propagation procedure and the cutting-plane-focused MIP solver can run in parallel utilizing different types of hardware (GPUs and CPUs), their combination can quickly explore a large number of branches with strong cutting planes, leading to strong verification performance. Experiments demonstrate that our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark compared to the best tool in VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a wide range of benchmarks. GCP-CROWN is part of the $\alpha$,$\beta$-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN
• Abstract（参考訳）: 境界伝播法は、分岐と束縛を組み合わせることで、正確性、堅牢性、安全性などのディープニューラルネットワークの特性を正式に検証する最も効果的な方法の一つである。 しかし、従来の解法では広く受け入れられる平面制約の一般的な形式は扱えないため、凸緩和が強化された検証器の強化に不可欠である。 本稿では,境界伝播手順を一般化し,既存の境界伝播定式化に現れない緩和された整数変数を含む任意の切断平面制約を付加することを可能にする。 一般化された有界伝播法であるGCP-CROWNは、有界伝播法の効率とGPU加速度の利点を生かしながら、ニューラルネットワーク検証に汎用的切削平面法を適用する機会を開く。 ケーススタディとして、オフザシェルフ混合整数計画法(MIP)によって生成される切断面の使用について検討する。 新しい定式化により, MIPソルバは, 境界プロパゲーションに基づく検証の強化のために高品質な切削面を生成することができることがわかった。 分岐中心の有界伝播プロシージャとカットプレーン中心のMIPソルバは、異なるタイプのハードウェア(GPUとCPU)を用いて並列に動作可能であるため、それらの組み合わせは、強い切断面を持つ多数の分岐を迅速に探索し、高い検証性能をもたらす。 VNN-COMP 2021のベストツールと比較して,oval20ベンチマークを完全に解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器であり,また,幅広いベンチマークにおいて最先端の検証器よりも顕著に優れていることを示す。 GCP-CROWNは、VNN-COMP 2022の勝者である$\alpha$,$\beta$-CROWN検証ツールの一部である。 コードはhttp://PaperCode.cc/GCP-CROWNで入手できる。

関連論文リスト

• Learning Cut Generating Functions for Integer Programming [1.1510009152620668]
  分岐とカットのアルゴリズムは、大規模な整数計画問題の解法である。 近年の進歩は、パラメータ化された族から最適な切断平面を選択するためのデータ駆動アプローチを採用している。 選択したCGFは,特定の分布に対するGMIカットよりも優れることを示す。
  論文  参考訳（メタデータ） (2024-05-22T20:56:34Z)
• Verifying message-passing neural networks via topology-based bounds tightening [3.3267518043390205]
  我々は、メッセージパッシングニューラルネットワーク(MPNN)のための堅牢な証明書を提供するための、計算学的に効果的なアプローチを開発する。 私たちの研究は混合整数最適化に基づいており、様々なサブプロブレムをエンコードしています。 ノード分類とグラフ分類の両方の問題を検証し、エッジの追加と削除の両方を行うトポロジ的攻撃について検討する。
  論文  参考訳（メタデータ） (2024-02-21T17:05:27Z)
• Solving a Class of Cut-Generating Linear Programs via Machine Learning [0.0]
  カット生成線形プログラム(CGLP)は分離オラクルとして重要な役割を担い、混合整数プログラムの可能な領域に対して有効な不等式を生成する。 分岐木と分岐木のノードでデュアルPを実行するのは、ノード候補の数と、ノードが有用な切断平面を許容する事前知識がないため、計算的に煩雑である。 本稿では,分岐木ノードで切断面を生成できるかどうかを判定する,マシンPクラスの最適値を近似する学習に基づく新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-10-30T18:31:52Z)
• GloptiNets: Scalable Non-Convex Optimization with Certificates [61.50835040805378]
  本稿では,ハイパーキューブやトーラス上のスムーズな関数を扱う証明書を用いた非キューブ最適化手法を提案する。 スペクトルの減衰に固有の対象関数の正則性を活用することにより、正確な証明を取得し、高度で強力なニューラルネットワークを活用することができる。
  論文  参考訳（メタデータ） (2023-06-26T09:42:59Z)
• GDB: Gated convolutions-based Document Binarization [0.0]
  我々は、ゲーティング値の学習としてテキスト抽出を定式化し、不正確なストロークエッジ抽出の問題を解決するために、エンドツーエンドのゲート畳み込みネットワーク(GDB)を提案する。 提案するフレームワークは,2つの段階から構成される。第1に,事前マスクとエッジを供給して,より正確な特徴マップを得るために,エッジブランチを付加した粗いサブネットワークを訓練する。 第2に、シャープエッジに基づくゲート畳み込みにより第1ステージの出力を洗練させるために、精製サブネットワークをカスケードする。
  論文  参考訳（メタデータ） (2023-02-04T02:56:40Z)
• Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
  本稿では,効率的な分岐戦略を設計するための新しい機械学習フレームワークを提案する。 グラフ入力として検証したいネットワークを直接扱う2つのグラフニューラルネットワーク(GNN)を学習する。 我々のGNNモデルは、より大きな未確認ネットワーク上での厳しい特性に対してよく一般化されていることを示す。
  論文  参考訳（メタデータ） (2021-07-27T14:42:57Z)
• 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)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• Patch-level Neighborhood Interpolation: A General and Effective Graph-based Regularization Strategy [77.34280933613226]
  我々は、ネットワークの計算において非局所的な表現を行うtextbfPatch-level Neighborhood Interpolation(Pani)と呼ばれる一般的な正規化器を提案する。 提案手法は,異なる層にパッチレベルグラフを明示的に構築し,その近傍のパッチ特徴を線形に補間し,汎用的で効果的な正規化戦略として機能する。
  論文  参考訳（メタデータ） (2019-11-21T06:31:59Z)

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

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