論文の概要: A Certified Proof Checker for Deep Neural Network Verification in Imandra
- arxiv url: http://arxiv.org/abs/2405.10611v2
- Date: Tue, 24 Jun 2025 15:45:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-25 19:48:23.223234
- Title: A Certified Proof Checker for Deep Neural Network Verification in Imandra
- Title（参考訳）: Imandraにおけるディープニューラルネットワーク検証のための証明証明チェッカー
- Authors: Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz,
- Abstract要約: Imandra における Marabou 証明書チェックの代替実装を提案する。
これはマラブーに対してより強力な独立保証を与える。
これは、対話的定理証明において、DNN検証器を広く採用する道を開く。
- 参考スコア（独自算出の注目度）: 0.9895793818721335
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra -- an industrial functional programming language and an interactive theorem prover (ITP) -- that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.
- Abstract（参考訳）: ディープニューラルネットワーク(DNN)の検証の最近の進歩は、安全クリティカルなものを含む多くのアプリケーション領域で、より広範なDNN検証技術の使用の道を開いた。
しかし、DNN検証はそれ自体、誤りや数値的な不正確さの影響を受けやすい複雑なプログラムであり、結果として、DNN検証に対する信頼の問題が提起されている。
この問題に対処するための顕著な試みの1つは、独立したアルゴリズムチェックの対象となる結果の証明書を生成する能力を備えたDNN検証の強化である。
Marabou証明書の定式化は、最先端のDNN検証ツールであるMarabouの上にすでに存在するが、C++で実装されており、コード自体が信頼の問題を提起している(例えば、浮動小数点演算の精度や実装の健全性を保証する)。
本稿では,産業用関数型言語と対話型定理証明器(ITP)であるImandraにおけるMarabou証明書チェックの代替実装について述べる。
結果の意義は2つある。
まず、マラブー証明に対してより強い独立保証を与える。
第二に、多くのIPPが既にSMTソルバを組み込んでいるのと同じように、対話的定理におけるDNN検証の広範な採用の道を開く。
関連論文リスト
- Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples [52.564617070814485]
本稿では,NN検証のための音響性ベンチマークを提案する。
私たちのベンチマークには、意図的に挿入された反例のインスタンスが含まれています。
我々のベンチマークでは、最先端のNN検証器のバグと合成バグの識別に成功している。
論文 参考訳（メタデータ） (2024-12-04T09:24:33Z) - Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
グラフニューラルネットワーク(GNN)におけるラベルフリップの正確な認証手法を提案する。
本稿では,ノード分類タスクにおける広範囲なGNNアーキテクチャの認証に本手法を適用した。
私たちの研究は、ニューラルネットワークによって引き起こされた毒殺攻撃に対する最初の正確な認証を提示します。
論文 参考訳（メタデータ） (2024-11-30T17:05:12Z) - Enumerating Safe Regions in Deep Neural Networks with Provable
Probabilistic Guarantees [86.1362094580439]
安全プロパティとDNNが与えられた場合、安全であるプロパティ入力領域のすべての領域の集合を列挙する。
この問題の #P-hardness のため,epsilon-ProVe と呼ばれる効率的な近似法を提案する。
提案手法は, 許容限界の統計的予測により得られた出力可到達集合の制御可能な過小評価を利用する。
論文 参考訳（メタデータ） (2023-08-18T22:30:35Z) - Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
本稿では,DNN検証のための検証チェッカーの実装について述べる。
数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
論文 参考訳（メタデータ） (2023-07-12T16:53:32Z) - 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) - 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 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) - Enhancing Graph Neural Network-based Fraud Detectors against Camouflaged
Fraudsters [78.53851936180348]
近年の実証研究,すなわち特徴カモフラージュと関係カモフラージュの2種類のカモフラージュを紹介した。
既存のGNNはこれらの2つのカモフラージュに対処していない。
カモフラージュ抵抗型GNN(CARE-GNN)と呼ばれる新しいモデルを提案し、カモフラージュに対する3つのユニークなモジュールを用いたGNN集約プロセスを強化する。
論文 参考訳（メタデータ） (2020-08-19T22:33:12Z) - CodNN -- Robust Neural Networks From Coded Classification [27.38642191854458]
ディープニューラルネットワーク(Deep Neural Networks、DNN)は、現在進行中の情報革命における革命的な力である。
DNNは、敵対的であろうとランダムであろうと、ノイズに非常に敏感である。
これは、DNNのハードウェア実装と、自律運転のような重要なアプリケーションへの展開において、根本的な課題となる。
提案手法により,DNNのデータ層あるいは内部層は誤り訂正符号で符号化され,ノイズ下での計算が成功することが保証される。
論文 参考訳（メタデータ） (2020-04-22T17:07:15Z) - GraN: An Efficient Gradient-Norm Based Detector for Adversarial and
Misclassified Examples [77.99182201815763]
ディープニューラルネットワーク(DNN)は、敵対的な例やその他のデータ摂動に対して脆弱である。
GraNは、どのDNNにも容易に適応できる時間およびパラメータ効率の手法である。
GraNは多くの問題セットで最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2020-04-20T10:09:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。