論文の概要: A Certified Proof Checker for Deep Neural Network Verification

• arxiv url: http://arxiv.org/abs/2405.10611v1
• Date: Fri, 17 May 2024 08:16:32 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-20 16:42:27.391824
• Title: A Certified Proof Checker for Deep Neural Network Verification
• Title（参考訳）: ディープニューラルネットワーク検証のための証明証明チェッカー
• Authors: Remi Desmartin, Omri Isac, Ekaterina Komendantskaya, Kathrin Stark, Grant Passmore, Guy Katz,
• Abstract要約: Imandra における Marabou 検証アルゴリズムの代替実装を提案する。 これにより、アルゴリズムの基盤となる数学的結果の証明を含む、正式な保証付きの実装を得ることができる。
• 参考スコア（独自算出の注目度）: 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 broader usage of DNN verification technology in many application areas, including safety-critical ones. DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and imprecisions; 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 proofs of their results that are subject to independent algorithmic certification (proof checking). Formulations of proof production and proof checking already exist on top of the state-of-the-art Marabou DNN verifier. The native implementation of the proof checking algorithm for Marabou was done in C++ and itself raised the question of trust in the code (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou proof checking algorithm in Imandra -- an industrial functional programming language and prover -- that allows us to obtain an implementation with formal guarantees, including proofs of mathematical results underlying the algorithm, such as the use of the Farkas lemma.
• Abstract（参考訳）: ディープニューラルネットワーク(DNN)の検証の最近の進歩は、安全クリティカルなものを含む多くのアプリケーション領域で、DNN検証技術を広く活用するための道を開いた。 DNN検証プログラムは、それ自体がエラーや不正確性に影響を受けやすい複雑なプログラムである。 この問題に対処するための顕著な試みの1つは、独立したアルゴリズム認証(保護チェック)の対象となる結果の証明を生成する能力を備えたDNN検証の強化である。 証明生成と証明チェックの定式化は、最先端のマラブーDNN検証器の上にすでに存在する。 Marabouの証明チェックアルゴリズムのネイティブ実装はC++で行われ、コードに対する信頼の問題が提起された(例えば、浮動小数点演算の精度や実装の健全性の保証)。 本稿では,産業用関数型言語と証明器であるImandraにおけるMarabou検定アルゴリズムの代替実装について述べる。

関連論文リスト

• 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)

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

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