論文の概要: Neural Network Verification with Proof Production

• arxiv url: http://arxiv.org/abs/2206.00512v1
• Date: Wed, 1 Jun 2022 14:14:37 GMT
• ステータス: 処理完了
• システム内更新日: 2022-06-02 13:39:43.879571
• Title: Neural Network Verification with Proof Production
• Title（参考訳）: 証明生産によるニューラルネットワークの検証
• Authors: Omri Isac and Clark Barrett and Min Zhang and Guy Katz
• Abstract要約: そこで本研究では,Simplex ベースの DNN 検証器を実証生産能力で拡張するための新しいメカニズムを提案する。 我々の証明生産は、よく知られたファルカスの補題の効率的な適応に基づいている。 航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースにおいて, 証明生産が成功することを示すものである。
• 参考スコア（独自算出の注目度）: 7.898605407936655
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep neural networks (DNNs) are increasingly being employed in safety-critical systems, and there is an urgent need to guarantee their correctness. Consequently, the verification community has devised multiple techniques and tools for verifying DNNs. When DNN verifiers discover an input that triggers an error, that is easy to confirm; but when they report that no error exists, there is no way to ensure that the verification tool itself is not flawed. As multiple errors have already been observed in DNN verification tools, this calls the applicability of DNN verification into question. In this work, we present a novel mechanism for enhancing Simplex-based DNN verifiers with proof production capabilities: the generation of an easy-to-check witness of unsatisfiability, which attests to the absence of errors. Our proof production is based on an efficient adaptation of the well-known Farkas' lemma, combined with mechanisms for handling piecewise-linear functions and numerical precision errors. As a proof of concept, we implemented our technique on top of the Marabou DNN verifier. Our evaluation on a safety-critical system for airborne collision avoidance shows that proof production succeeds in almost all cases and requires only minimal overhead.
• Abstract（参考訳）: ディープニューラルネットワーク(DNN)は、安全クリティカルなシステムにますます採用されており、それらの正確性を保証する必要がある。 その結果、検証コミュニティはDNNを検証するための複数の技術とツールを考案した。 DNN検証者がエラーを発生させるインプットを発見すると、それは容易に確認できますが、エラーが存在しないと報告した場合、検証ツール自体に欠陥がないことを保証する方法はありません。 DNN検証ツールですでに複数のエラーが観測されているため、この問題に対するDNN検証の適用性は疑問視されている。 本稿では,誤りの欠如を裏付ける,不満足さのチェックが容易な証人の生成という,simplexベースのdnn検証能力向上のための新しいメカニズムを提案する。 我々の証明生産は、よく知られたFarkasの補題の効率的な適応と、片方向線形関数と数値的精度誤差を扱う機構の組み合わせに基づいている。 概念実証として,マラブーDNN検証器上に本手法を実装した。 航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースで生産が成功し, 最小限のオーバーヘッドしか必要としないことを示す。

関連論文リスト

• A Certified Proof Checker for Deep Neural Network Verification [0.9895793818721335]
  Imandra における Marabou 検証アルゴリズムの代替実装を提案する。 これにより、アルゴリズムの基盤となる数学的結果の証明を含む、正式な保証付きの実装を得ることができる。
  論文  参考訳（メタデータ） (2024-05-17T08:16:32Z)
• Securing Graph Neural Networks in MLaaS: A Comprehensive Realization of Query-based Integrity Verification [68.86863899919358]
  我々は機械学習におけるGNNモデルをモデル中心の攻撃から保護するための画期的なアプローチを導入する。 提案手法は,GNNの完全性に対する包括的検証スキーマを含み,トランスダクティブとインダクティブGNNの両方を考慮している。 本稿では,革新的なノード指紋生成アルゴリズムを組み込んだクエリベースの検証手法を提案する。
  論文  参考訳（メタデータ） (2023-12-13T03:17:05Z)
• Cal-DETR: Calibrated Detection Transformer [67.75361289429013]
  本稿では,Deformable-DETR,UP-DETR,DINOのキャリブレーション検出トランス(Cal-DETR)のメカニズムを提案する。 我々は、不確実性を利用してクラスロジットを変調する不確実性誘導ロジット変調機構を開発する。 その結果、Cal-DETRは、ドメイン内およびドメイン外の両方を校正する競合する列車時間法に対して有効であることがわかった。
  論文  参考訳（メタデータ） (2023-11-06T22:13:10Z)
• ELEGANT: Certified Defense on the Fairness of Graph Neural Networks [94.10433608311604]
  グラフニューラルネットワーク(GNN)は,グラフベースのタスクにおいて,目立ったグラフ学習モデルとして登場した。 悪意のある攻撃者は、入力グラフデータに摂動を追加することで、予測の公平度を容易に損なうことができる。 本稿では, ELEGANT というフレームワークを提案し, GNN の公正度レベルにおける認証防御の新たな課題について検討する。
  論文  参考訳（メタデータ） (2023-11-05T20:29:40Z)
• Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
  本稿では,DNN検証のための検証チェッカーの実装について述べる。 数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
  論文  参考訳（メタデータ） (2023-07-12T16:53:32Z)
• DelBugV: Delta-Debugging Neural Network Verifiers [0.0]
  ディープニューラルネットワーク(DNN)は、ボード全体の多様なシステムにおいて重要なコンポーネントになりつつある。 彼らの成功にもかかわらず、しばしば悲惨な結果となり、これがそれらを正式に検証することに大きな関心を惹き付けている。 本稿では,DNN検証器上でデルタデバッギングを自動的に行うDelBugVという新しいツールを提案する。
  論文  参考訳（メタデータ） (2023-05-29T18:42:03Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Continuous Safety Verification of Neural Networks [1.7056768055368385]
  本稿では,前回のDNN安全検証問題から修正問題設定への移行結果のアプローチについて考察する。 全体的な概念は、認識された画像から視覚的方向を決定するために、DNNコントローラを装備する1/10ドルのスケールで評価される。
  論文  参考訳（メタデータ） (2020-10-12T13:28:04Z)
• Boosting Deep Neural Networks with Geometrical Prior Knowledge: A Survey [77.99182201815763]
  ディープニューラルネットワーク(DNN)は多くの異なる問題設定において最先端の結果を達成する。 DNNはしばしばブラックボックスシステムとして扱われ、評価と検証が複雑になる。 コンピュータビジョンタスクにおける畳み込みニューラルネットワーク(CNN)の成功に触発された、有望な分野のひとつは、対称幾何学的変換に関する知識を取り入れることである。
  論文  参考訳（メタデータ） (2020-06-30T14:56:05Z)
• GraN: An Efficient Gradient-Norm Based Detector for Adversarial and Misclassified Examples [77.99182201815763]
  ディープニューラルネットワーク(DNN)は、敵対的な例やその他のデータ摂動に対して脆弱である。 GraNは、どのDNNにも容易に適応できる時間およびパラメータ効率の手法である。 GraNは多くの問題セットで最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2020-04-20T10:09:27Z)

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

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