論文の概要: Proof-Driven Clause Learning in Neural Network Verification
- arxiv url: http://arxiv.org/abs/2503.12083v1
- Date: Sat, 15 Mar 2025 11:05:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-03-18 12:28:08.041275
- Title: Proof-Driven Clause Learning in Neural Network Verification
- Title(参考訳): ニューラルネットワーク検証における証明駆動クロース学習
- Authors: Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz,
- Abstract要約: 衝突駆動クロース学習(CDCL)を用いたDNN検証器のスケーラビリティ向上のためのアプローチを提案する。
本論文では,UNSAT証明を用いた競合項の導出のための新しいアルゴリズムを提案する。
複数のベンチマークによる実装評価の結果,類似した手法による2X--3Xの改良が示唆された。
- 参考スコア(独自算出の注目度): 1.6036524120600033
- License:
- Abstract: The widespread adoption of deep neural networks (DNNs) requires efficient techniques for safety verification. Existing methods struggle to scale to real-world DNNs, and tremendous efforts are being put into improving their scalability. In this work, we propose an approach for improving the scalability of DNN verifiers using Conflict-Driven Clause Learning (CDCL) -- an approach that has proven highly successful in SAT and SMT solving. We present a novel algorithm for deriving conflict clauses using UNSAT proofs, and propose several optimizations for expediting it. Our approach allows a modular integration of SAT solvers and DNN verifiers, and we implement it on top of an interface designed for this purpose. The evaluation of our implementation over several benchmarks suggests a 2X--3X improvement over a similar approach, with specific cases outperforming the state of the art.
- Abstract(参考訳): ディープニューラルネットワーク(DNN)の普及は、安全性検証に効率的な技術を必要とする。
既存のメソッドは、現実世界のDNNにスケールするのに苦労しています。
本研究では,SAT と SMT の解法において高い成功を収めた CDCL (Conflict-Driven Clause Learning) を用いた DNN 検証のスケーラビリティ向上のためのアプローチを提案する。我々は UNSAT 証明を用いて競合節を導出するための新しいアルゴリズムを提案し,それを高速化するためのいくつかの最適化を提案している。本手法は SAT ソルバと DNN 検証器のモジュラー統合を可能にし,この目的のために設計されたインタフェース上に実装する。複数のベンチマークによる実装評価は,類似のアプローチよりも2X--3X の改善が示唆されている。
関連論文リスト
- Adversarially Robust Spiking Neural Networks Through Conversion [16.2319630026996]
スパイキングニューラルネットワーク(SNN)は、さまざまな人工知能ニューラルネットワーク(ANN)ベースのAIアプリケーションに対して、エネルギー効率のよい代替手段を提供する。
SNNによるニューロモルフィックコンピューティングの進歩がアプリケーションでの利用を拡大するにつれ、SNNの対角的堅牢性の問題はより顕著になる。
論文 参考訳(メタデータ) (2023-11-15T08:33:46Z) - A DPLL(T) Framework for Verifying Deep Neural Networks [9.422860826278788]
人手によるソフトウェアと同じように、Deep Neural Networks(DNN)にもバグがあり、攻撃できる。
我々は,現代のSMTソルバで広く使われているDPLL(T)アルゴリズムに適応する新しい検証手法であるNeuralSATを紹介する。
論文 参考訳(メタデータ) (2023-07-17T18:49:46Z) - Incremental Verification of Neural Networks [3.9661031279983896]
本稿では,新しい理論,データ構造,アルゴリズムの設計に基づく,インクリメンタルかつ完全なDNN検証のための新しい汎用フレームワークを提案する。
我々の貢献はIVANというツールに実装され、MNISTとCIFAR10の分類に挑戦する上での全体的な幾何平均スピードアップの2.4倍、最先端のベースライン上でのACAS-XU分類器の幾何平均スピードアップの3.8倍となる。
論文 参考訳(メタデータ) (2023-04-04T15:28:22Z) - Incremental Satisfiability Modulo Theory for Verification of Deep Neural
Networks [22.015676101940077]
本稿ではReluplexフレームワークに基づく漸進的満足度変調理論(SMT)を提案する。
我々は,DeepIncと呼ばれる漸進的な解法としてアルゴリズムを実装し,実験結果から,ほとんどの場合,DeepIncの方が効率的であることが示された。
論文 参考訳(メタデータ) (2023-02-10T04:31:28Z) - The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural
Networks [94.63547069706459]
#DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。
違反の正確な数を返す新しい手法を提案する。
安全クリティカルなベンチマークのセットに関する実験結果を示す。
論文 参考訳(メタデータ) (2023-01-17T18:32:01Z) - Improved Algorithms for Neural Active Learning [74.89097665112621]
非パラメトリックストリーミング設定のためのニューラルネットワーク(NN)ベースの能動学習アルゴリズムの理論的および経験的性能を改善する。
本研究では,SOTA(State-of-the-art (State-the-art)) 関連研究で使用されるものよりも,アクティブラーニングに適する人口減少を最小化することにより,2つの後悔の指標を導入する。
論文 参考訳(メタデータ) (2022-10-02T05:03:38Z) - Comparative Analysis of Interval Reachability for Robust Implicit and
Feedforward Neural Networks [64.23331120621118]
我々は、暗黙的ニューラルネットワーク(INN)の堅牢性を保証するために、区間到達可能性分析を用いる。
INNは暗黙の方程式をレイヤとして使用する暗黙の学習モデルのクラスである。
提案手法は, INNに最先端の区間境界伝搬法を適用するよりも, 少なくとも, 一般的には, 有効であることを示す。
論文 参考訳(メタデータ) (2022-04-01T03:31:27Z) - Automatic Mapping of the Best-Suited DNN Pruning Schemes for Real-Time
Mobile Acceleration [71.80326738527734]
本稿では,汎用的,きめ細かな構造化プルーニング手法とコンパイラの最適化を提案する。
提案手法は,より微細な構造化プルーニング手法とともに,最先端のDNN最適化フレームワークよりも優れていることを示す。
論文 参考訳(メタデータ) (2021-11-22T23:53:14Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Designing Interpretable Approximations to Deep Reinforcement Learning [14.007731268271902]
ディープニューラルネットワーク(DNN)は、アルゴリズムのパフォーマンスのバーを設定する。
実際にそのようなハイパフォーマンスなDNNを使うことは不可能かもしれない。
この研究は、所望のパフォーマンスレベルを保持するだけでなく、例えば、DNNで表される潜伏した知識を簡潔に説明できるような縮小モデルを特定することを目指している。
論文 参考訳(メタデータ) (2020-10-28T06:33:09Z) - Deep Multi-Task Learning for Cooperative NOMA: System Design and
Principles [52.79089414630366]
我々は,近年のディープラーニング(DL)の進歩を反映した,新しいディープ・コラボレーティブなNOMAスキームを開発する。
我々は,システム全体を包括的に最適化できるように,新しいハイブリッドカスケードディープニューラルネットワーク(DNN)アーキテクチャを開発した。
論文 参考訳(メタデータ) (2020-07-27T12:38:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。