Fugu-MT 論文翻訳(概要): Proof Minimization in Neural Network Verification

論文の概要: 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)
FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
FIREはエビデンス検索とクレーム検証を反復的に統合する新しいフレームワークである。大きな言語モデル(LLM)のコストを平均7.6倍、検索コストを16.5倍削減しながら、パフォーマンスが若干向上している。これらの結果から,FIREは大規模ファクトチェック業務における適用を約束していることが明らかとなった。
論文参考訳（メタデータ） (2024-10-17T06:44:18Z)
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)
Sound and Complete Verification of Polynomial Networks [55.9260539566555]
PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
論文参考訳（メタデータ） (2022-09-15T11:50:43Z)
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks [9.85360493553261]
ディープニューラルネットワーク(DNN)の実践はますます進んでいるが、ロバストさの欠如により、安全クリティカルなドメインへの応用が妨げられている。本稿では,スケーラブルで正確なDNN検証のための新しい抽象化・リファインメント手法を提案する。
論文参考訳（メタデータ） (2022-07-02T07:04:20Z)
Neural Network Verification with Proof Production [7.898605407936655]
そこで本研究では,Simplex ベースの DNN 検証器を実証生産能力で拡張するための新しいメカニズムを提案する。我々の証明生産は、よく知られたファルカスの補題の効率的な適応に基づいている。航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースにおいて, 証明生産が成功することを示すものである。
論文参考訳（メタデータ） (2022-06-01T14:14:37Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
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)

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

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