論文の概要: Incremental Neural Network Verification via Learned Conflicts

• arxiv url: http://arxiv.org/abs/2603.12232v1
• Date: Thu, 12 Mar 2026 17:52:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-13 14:46:26.271206
• Title: Incremental Neural Network Verification via Learned Conflicts
• Title（参考訳）: 学習紛争によるインクリメンタルニューラルネットワークの検証
• Authors: Raya Elsaleh, Liam Davis, Haoze Wu, Guy Katz,
• Abstract要約: 本稿では,関連する検証クエリ間の競合を再利用するインクリメンタルな検証手法を提案する。 継承された競合はSATソルバを使用して処理され、一貫性チェックと伝搬を行う。 我々の実験は、インクリメンタルコンフリクトの再利用は検証の労力を減らし、非インクリメンタルベースラインよりも最大1.9倍のスピードアップをもたらすことを示した。
• 参考スコア（独自算出の注目度）: 3.030776653725253
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to $1.9\times$ over a non-incremental baseline.
• Abstract（参考訳）: ニューラルネットワーク検証は、より大きな分析手順のコアコンポーネントとしてしばしば使用され、同一ネットワーク上で密接に関連する検証クエリのシーケンスを生成する。 既存のニューラルネットワーク検証器では、各クエリは通常独立して解決され、以前の実行中に得られた情報は破棄され、探索空間の同じ不可能な領域を何度も探索する。 本研究では,この冗長性を低減し,検証の迅速化を目指す。 本稿では,関連する検証クエリ間の競合を再利用するインクリメンタルな検証手法を提案する。 このテクニックは、ブランチとバウンドベースのニューラルネットワーク検証子の上に追加することができる。 検証中、検証者は、学習されたアクティベーションフェーズの不可能な組み合わせに対応する競合を記録し、それらを実行中に保持する。 検証クエリ間の改善関係を形式化し、クエリで学習した競合が洗練されても有効であることを示し、健全な競合継承を可能にする。 継承された競合をSATソルバを用いて処理し、一貫性チェックと伝搬を行い、探索の早い段階で不可能なサブプロブレムを検出してプルーニングすることができる。 提案手法をマラブー検証器に実装し, 局所ロバスト性半径決定, 入力分割による検証, 最小限の特徴集合抽出という3つの検証課題で評価する。 我々の実験は、インクリメンタルコンフリクトの再利用は検証の労力を減らし、非インクリメンタルベースラインよりも最大1.9\times$のスピードアップをもたらすことを示した。

関連論文リスト

• Beyond Hungarian: Match-Free Supervision for End-to-End Object Detection [6.786987355161583]
  提案手法は,DETRを用いた新しい整合性学習手法である。 我々は、符号化された地下構造情報を用いて、クロスアテンション機構を通じてデコーダクエリを探索する。 実験により,提案手法は従来のマッチング処理をバイパスすることを示した。
  論文  参考訳（メタデータ） (2026-03-09T15:44:23Z)
• Preventing the Collapse of Peer Review Requires Verification-First AI [49.995126139461085]
  我々は、真理結合、すなわち、過度に科学的真理をトラックする場所のスコアの厳密さを提案する。 プロキシ・ソブリン評価に向けた相転移を駆動する2つの力の形式化を行う。
  論文  参考訳（メタデータ） (2026-01-23T17:17:32Z)
• Coordinating Search-Informed Reasoning and Reasoning-Guided Search in Claim Verification [16.655011153015202]
  マルチホップクレーム検証のための階層型エージェント推論と情報検索(HARIS)を提案する。 HARISは、主検証チェーンの構築に集中し、より多くの情報が必要な場合に事実質問を生成する高レベル推論エージェントと、より多くの情報を反復的に検索する低レベル検索エージェントから構成される。 EX-FEVER と HOVER のベンチマーク実験の結果,HARIS は高い性能を示した。
  論文  参考訳（メタデータ） (2025-06-09T08:11:43Z)
• FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
  FIREはエビデンス検索とクレーム検証を反復的に統合する新しいフレームワークである。 大きな言語モデル(LLM)のコストを平均7.6倍、検索コストを16.5倍削減しながら、パフォーマンスが若干向上している。 これらの結果から,FIREは大規模ファクトチェック業務における適用を約束していることが明らかとなった。
  論文  参考訳（メタデータ） (2024-10-17T06:44:18Z)
• From Chaos to Clarity: Claim Normalization to Empower Fact-Checking [57.024192702939736]
  Claim Normalization(別名 ClaimNorm)は、複雑でノイズの多いソーシャルメディア投稿を、より単純で分かりやすい形式に分解することを目的としている。 本稿では,チェーン・オブ・ソートとクレーム・チェック・バシネス推定を利用した先駆的アプローチであるCACNを提案する。 実験により, CACNは様々な評価尺度において, いくつかの基準値を上回る性能を示した。
  論文  参考訳（メタデータ） (2023-10-22T16:07:06Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。 分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。 我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
  論文  参考訳（メタデータ） (2022-09-15T11:50:43Z)
• Neural Network Verification using Residual Reasoning [0.0]
  本稿では,経験的推論を用いて,抽象化に基づくニューラルネットワークの検証の強化を提案する。 本質的には、精細化されたネットワークが正しく振る舞うことを保証された検索空間の一部に関する情報を、検証者が格納することができる。
  論文  参考訳（メタデータ） (2022-08-05T10:39:04Z)
• ReAct: Temporal Action Detection with Relational Queries [84.76646044604055]
  本研究は,アクションクエリを備えたエンコーダ・デコーダフレームワークを用いて,時間的行動検出(TAD)の進展を図ることを目的とする。 まず,デコーダ内の関係注意機構を提案し,その関係に基づいてクエリ間の関心を誘導する。 最後に、高品質なクエリを区別するために、推論時に各アクションクエリのローカライズ品質を予測することを提案する。
  論文  参考訳（メタデータ） (2022-07-14T17:46:37Z)
• Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound [2.896192909215469]
  両パラダイムの強みを組み合わせた新しい完全検証器を提案する。 BaBプロセス中に生成されるサブプロブレムの数を劇的に減少させるために、マルチニューロン緩和を用いる。 評価の結果,既存のベンチマークと,従来考えられていたよりもはるかに高い精度のネットワークにおいて,検証が新たな最先端性を達成できることが確認された。
  論文  参考訳（メタデータ） (2022-04-30T13:12:33Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)

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

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