論文の概要: Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification

• arxiv url: http://arxiv.org/abs/2512.11087v1
• Date: Thu, 11 Dec 2025 19:59:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-15 15:48:11.555719
• Title: Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification
• Title（参考訳）: Clip-and-Verify: ニューラルネットワーク検証高速化のための線形制約駆動型ドメインクリッピング
• Authors: Duo Zhou, Jorge Chavez, Hesun Chen, Grani A. Hanasusanto, Huan Zhang,
• Abstract要約: 最先端ニューラルネットワーク(NN)検証は、分岐とバウンド(BaB)の手順を高速なバウンディング技術で適用することが、多くの挑戦的な検証特性に対処する上で重要な役割を果たしていることを示す。 本稿では,NN検証の有効性を高めるために,スケーラブルで効率的な手法のクラスである線形制約駆動型クリッピングフレームワークを紹介する。
• 参考スコア（独自算出の注目度）: 9.733843486234878
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties. In this work, we introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers. Under this framework, we develop two novel algorithms that efficiently utilize linear constraints to 1) reduce portions of the input space that are either verified or irrelevant to a subproblem in the context of branch-and-bound, and 2) directly improve intermediate bounds throughout the network. The process novelly leverages linear constraints that often arise from bound propagation methods and is general enough to also incorporate constraints from other sources. It efficiently handles linear constraints using a specialized GPU procedure that can scale to large neural networks without the use of expensive external solvers. Our verification procedure, Clip-and-Verify, consistently tightens bounds across multiple benchmarks and can significantly reduce the number of subproblems handled during BaB. We show that our clipping algorithms can be integrated with BaB-based verifiers such as $α,β$-CROWN, utilizing either the split constraints in activation-space BaB or the output constraints that denote the unverified input space. We demonstrate the effectiveness of our procedure on a broad range of benchmarks where, in some instances, we witness a 96% reduction in the number of subproblems during branch-and-bound, and also achieve state-of-the-art verified accuracy across multiple benchmarks. Clip-and-Verify is part of the $α,β$-CROWN verifier (http://abcrown.org), the VNN-COMP 2025 winner. Code available at https://github.com/Verified-Intelligence/Clip_and_Verify.
• Abstract（参考訳）: 最先端ニューラルネットワーク(NN)検証は、分岐とバウンド(BaB)の手順を高速なバウンディング技術で適用することが、多くの挑戦的な検証特性に対処する上で重要な役割を果たしていることを示す。 本稿では,NN検証の有効性を高めるために,スケーラブルで効率的な手法のクラスである線形制約駆動型クリッピングフレームワークを紹介する。 そこで我々は,線形制約を効率的に活用する2つの新しいアルゴリズムを開発した。 1) 分岐とバウンドの文脈でサブプロブレムに検証されたり、関係のない入力空間の部分を縮小し、 2) ネットワーク全体の中間境界を直接改善する。 このプロセスは、境界伝播法からしばしば生じる線形制約を新しく利用し、他のソースからの制約も組み込むのに十分な一般性を持つ。 高価な外部解決器を使わずに、大規模ニューラルネットワークにスケール可能な、特殊なGPUプロシージャを使用して、線形制約を効率的に処理する。 検証手順であるClip-and-Verifyは、複数のベンチマークのバウンダリを一貫して厳格化し、BaBで処理されるサブプロブレムの数を著しく削減できる。 本稿では,このクリッピングアルゴリズムを,アクティベーション空間BaBの分割制約や,未検証入力空間を表す出力制約を利用して,$α,β$-CROWNなどのBaBベースの検証器と統合可能であることを示す。 提案手法の有効性を広範囲なベンチマークで実証し,ブランチ・アンド・バウンド中のサブプロブレム数の96%削減と,複数のベンチマークにおける最先端の精度向上を図った。 Clip-and-Verifyは、VNN-COMP 2025の勝者である$α,β$-CROWN検証(http://abcrown.org)の一部である。 コードはhttps://github.com/Verified-Intelligence/Clip_and_Verifyで公開されている。

関連論文リスト

• Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
  ブランチ・アンド・バウンド(BaB)は、ニューラルネットワーク(NN)検証において最も効果的な手法の一つである。 我々は、一般的な非線形性にBaBを実行し、一般的なアーキテクチャでNNを検証する汎用フレームワークGenBaBを開発した。 我々のフレームワークは、一般的な非線形グラフの検証を可能にし、単純なNNを超えた検証アプリケーションを可能にする。
  論文  参考訳（メタデータ） (2024-05-31T17:51:07Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。 分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。 我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
  論文  参考訳（メタデータ） (2022-09-15T11:50:43Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。 本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
  論文  参考訳（メタデータ） (2022-08-11T10:31:28Z)
• 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)
• 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)

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

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