論文の概要: Proof Minimization in Neural Network Verification

• arxiv url: http://arxiv.org/abs/2511.08198v1
• Date: Wed, 12 Nov 2025 01:46:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-12 20:17:03.690223
• Title: Proof Minimization in Neural Network Verification
• Title（参考訳）: ニューラルネットワーク検証における最小化の証明
• Authors: Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz,
• Abstract要約: ディープニューラルネットワーク(DNN)は複雑なツールであり、健全性を損なう可能性のあるバグが含まれ、検証プロセスの信頼性を損なう可能性がある。 検証過程で学習した事実を除去するアルゴリズムを提案するが、証明自体には不要である。 提案アルゴリズムは,検証プロセス自体に実行時のオーバヘッドを7%～20%導入した上で,証明サイズを37%～82%削減し,検証時間を30%～88%短縮することを示した。
• 参考スコア（独自算出の注目度）: 3.2006701823251578
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.
• Abstract（参考訳）: ディープニューラルネットワーク(DNN)の普及は、安全性を検証するための効率的なテクニックを必要とする。 DNN検証は複雑なツールであり、その健全性を損なう可能性のあるバグが含まれ、検証プロセスの信頼性を損なう可能性がある。 この懸念は、証明によって緩和することができる: 外部で信頼性の高い証明チェッカーによってチェック可能であり、検証プロセスの正確性を証明するアーティファクト。 しかし、そのような証明は非常に大きく、多くのシナリオでの使用を制限する傾向にある。 本研究では,DNN検証器が生成する不満足性の証明を最小化することにより,この問題に対処する。 検証過程で学習した事実を除去するアルゴリズムを提案するが、証明自体には不要である。 概念的には,UNSATを推定するために使用する事実間の依存関係を分析し,寄与しない事実を除去する。 次に、2つの代替手順を用いて、残余の不要な依存関係を排除して証明をさらに最小化する。 提案アルゴリズムをDNN検証器の証明上に実装し,複数のベンチマークで評価した。 提案アルゴリズムは,検証プロセス自体に実行時のオーバヘッドを7%～20%導入した上で,証明サイズを37%～82%削減し,検証時間を30%～88%短縮することを示した。

関連論文リスト

• SoundnessBench: A Soundness Benchmark for Neural Network Verifiers [45.86647998712757]
  NN検証のための新しいベンチマーク「SoundnessBench」を開発した。 SoundnessBenchは、敵の攻撃から隠された意図的に挿入された反例を持つインスタンスで構成されている。 我々のトレーニングは,隠れた反例を効果的に生成し,SoundnessBenchは最先端のNN検証器のバグの同定に成功したことを実証する。
  論文  参考訳（メタデータ） (2024-12-04T09:24:33Z)
• A Certified Proof Checker for Deep Neural Network Verification in Imandra [0.9895793818721335]
  Imandra における Marabou 証明書チェックの代替実装を提案する。 これはマラブーに対してより強力な独立保証を与える。 これは、対話的定理証明において、DNN検証器を広く採用する道を開く。
  論文  参考訳（メタデータ） (2024-05-17T08:16:32Z)
• Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
  本稿では,DNN検証のための検証チェッカーの実装について述べる。 数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
  論文  参考訳（メタデータ） (2023-07-12T16:53:32Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Neural Network Verification with Proof Production [7.898605407936655]
  そこで本研究では,Simplex ベースの DNN 検証器を実証生産能力で拡張するための新しいメカニズムを提案する。 我々の証明生産は、よく知られたファルカスの補題の効率的な適応に基づいている。 航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースにおいて, 証明生産が成功することを示すものである。
  論文  参考訳（メタデータ） (2022-06-01T14:14:37Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)

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

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