論文の概要: CLAD: Constrained Abstract Domain for Neural Network Verification

• arxiv url: http://arxiv.org/abs/2609.34628v1
• Date: Mon, 28 Sep 2026 08:48:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 11:48:49.326083
• Title: CLAD: Constrained Abstract Domain for Neural Network Verification
• Title（参考訳）: CLAD: ニューラルネットワーク検証のための制約付き抽象ドメイン
• Abstract要約: 制約付きラグランジアン抽象ドメイン(CLAD)を紹介する。 CLADは凸制約の組み合わせによって定義された入力領域上のニューラルネットワークの音響過近似を計算する。 我々は,4つの畳み込みネットワーク上の1,944インスタンスにおけるCLADの評価を行った。
• 参考スコア（独自算出の注目度）: 7.480478840881969
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Neural network verification (NNV) formally verifies that a network satisfies a specified property for all inputs within a defined region. Modern NNV tools employ abstract domains to compute a sound over-approximation of the network's behavior from the given input region, thus the tightness of these abstractions essentially determines efficiency. A long line of increasingly precise domains has been developed, but they all describe the valid input region in the same restrictive way, e.g., an Lp-norm ball. A practical input region is rarely a simple Lp ball, but rather a combination Lp ball with additional constraints. Verifying a network over such a region with existing abstraction produces a loose over-approximation, which results in either failing to verify a property or spurious counterexamples. We introduce Constrained Lagrangian Abstract Domain (CLAD), a new abstract domain that computes a sound over-approximation of neural networks over input regions defined by a combination of convex constraints. CLAD propagates these constraints and tightens bounds over the true feasible region. However, bounding a neuron over the intersection of these constraints has no closed-form solution, so CLAD relaxes each constraint into the objective with a Lagrange multiplier and solves the resulting max-min problem with a projected primal-dual method, alternating a projected gradient step on the input with a multiplier update. CLAD supports any convex constraint with a subgradient, e.g., from automatic differentiation. We evaluate CLAD on 1,944 instances across four convolutional networks with motion-blur structured perturbations with halfspace or L2-ball constraints. On standard unconstrained Linf property, CLAD verifies as many instances as GCPCROWN at a similar runtime. On constrained properties, CLAD verifies 60\% more instances than GCPCROWN on L2-ball properties, and 22% more in total.
• Abstract（参考訳）: ニューラルネットワーク検証(NNV)は、ネットワークが定義された領域内のすべての入力に対して指定されたプロパティを満たすことを正式に検証する。 現代のNNVツールは、与えられた入力領域からネットワークの振舞いの過度な近似を計算するために抽象ドメインを使用するため、これらの抽象化の厳密さが本質的に効率を決定する。 より正確な領域の長い行が開発されているが、それらはすべて、Lp-ノルム球のように、同じ制限的な方法で有効な入力領域を記述する。 実用的な入力領域は単純なLp球ではなく、追加の制約を伴うLp球の組み合わせである。 そのような領域上のネットワークを既存の抽象化で検証すると、ゆるやかなオーバー近似が発生するため、プロパティの検証に失敗するか、急激な反例が発生する。 コンベックス制約の組み合わせによって定義された入力領域上のニューラルネットワークの音響過度近似を計算する新しい抽象ドメインであるConstrained Lagrangian Abstract Domain (CLAD)を紹介する。 CLADはこれらの制約を伝播し、真の実現可能な領域上の境界を締め付ける。 しかし、これらの制約の交叉にニューロンを束縛することは閉形式解を持たないため、CLADは各制約をラグランジュ乗算器で対象に緩和し、投影された原始双対法で最大ミン問題を解き、乗算器更新で入力の射影勾配ステップを交互に交互に行う。 CLADは、自動微分から下位段階、例えば、等級の凸制約をサポートする。 我々は,4つの畳み込みネットワーク上の1,944インスタンスにおけるCLADの評価を行った。 標準の制約のないLinfプロパティでは、CLADは同様のランタイムでGCPCROWNと同じくらい多くのインスタンスを検証する。 制約特性について、CLADはGCPCROWNよりもL2-ball特性が60倍、合計で22%のインスタンスを検証している。

関連論文リスト

• Expressivity Saturation: Reduced Affine Region Usage Under Increasing Task Complexity [5.366707531676941]
  ピースワイズ・ファインニューラルネットワークは、連続的なピースワイズ・ファインマップを実装している。 実験後に実現した理論領域容量とアフィン領域のギャップについて検討した。
  論文  参考訳（メタデータ） (2026-06-19T18:55:46Z)
• Neural Networks as Local-to-Global Computations [0.0]
  エッジ上の制約マップとして各計算ステップを符号化することにより,任意のReLUニューラルネットワークからシーフを構築する。 フォワードパスとは異なり、熱方程式は層間で情報を双方向に伝播し、両方の方向に制約を課すピン付きニューロンを可能にする。 我々は, この枠組みを小さな合成問題に対して実験的に検証し, 収束定理を検証し, せん断に基づくトレーニングがまだ勾配降下と競合していないものの, 理論によって予測される定量的なスケーリング法則に従うことを示した。
  論文  参考訳（メタデータ） (2026-03-16T05:23:31Z)
• Convergence of Adam in Deep ReLU Networks via Directional Complexity and Kakeya Bounds [49.1574468325115]
  Adamのような一階適応最適化手法は、現代のディープニューラルネットワークをトレーニングするためのデフォルトの選択肢である。 我々は,領域横断の制限を段階的に強化する多層改質フレームワークを開発した。 有効次元において,領域交差の数が指数的からほぼ直線的に崩壊することが証明された。
  論文  参考訳（メタデータ） (2025-05-21T01:34:16Z)
• Zonotope Domains for Lagrangian Neural Network Verification [102.13346781220383]
  我々は、ディープニューラルネットワークを多くの2層ニューラルネットワークの検証に分解する。 我々の手法は線形プログラミングとラグランジアンに基づく検証技術の両方により改善された境界を与える。
  論文  参考訳（メタデータ） (2022-10-14T19:31:39Z)
• $\texttt{FedBC}$: Calibrating Global and Local Models via Federated Learning Beyond Consensus [66.62731854746856]
  フェデレートラーニング(FL)では、デバイス全体にわたるモデル更新の集約を通じて、グローバルモデルを協調的に学習する目的は、ローカル情報を通じたパーソナライズという目標に反対する傾向にある。 本研究では,このトレードオフを多基準最適化により定量的にキャリブレーションする。 私たちは、$texttFedBC$が、スイートデータセット間でグローバルおよびローカルモデルのテスト精度のメトリクスのバランスをとることを実証しています。
  論文  参考訳（メタデータ） (2022-06-22T02:42:04Z)
• On the Effective Number of Linear Regions in Shallow Univariate ReLU Networks: Convergence Guarantees and Implicit Bias [50.84569563188485]
  我々は、ラベルが$r$のニューロンを持つターゲットネットワークの符号によって決定されるとき、勾配流が方向収束することを示す。 我々の結果は、標本サイズによらず、幅が$tildemathcalO(r)$である、緩やかなオーバーパラメータ化をすでに維持しているかもしれない。
  論文  参考訳（メタデータ） (2022-05-18T16:57:10Z)
• How to Explain Neural Networks: A perspective of data space division [2.4499092754102874]
  ディープラーニングで表されるアルゴリズムの解釈可能性はまだオープンな問題です。 本稿では,説明の2つの属性に基づく既存の説明可能な手法の欠点について論じる。 本稿では,データ空間分割の観点から,完全局所解釈可能なモデル非依存説明法(CLIMEP)の原理を提案する。
  論文  参考訳（メタデータ） (2021-05-17T13:43:37Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。 活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。 BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
  論文  参考訳（メタデータ） (2021-04-14T09:22:42Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

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

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