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

• arxiv url: http://arxiv.org/abs/2307.06299v2
• Date: Tue, 13 Feb 2024 15:51:50 GMT
• ステータス: 処理完了
• システム内更新日: 2024-02-14 19:42:31.728437
• Title: Towards a Certified Proof Checker for Deep Neural Network Verification
• Title（参考訳）: ディープニューラルネットワーク検証のための認証証明チェッカーを目指して
• Authors: Remi Desmartin, Omri Isac, Grant Passmore, Kathrin Stark, Guy Katz and Ekaterina Komendantskaya
• Abstract要約: 本稿では,DNN検証のための検証チェッカーの実装について述べる。 数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
• 参考スコア（独自算出の注目度）: 1.0485739694839669
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance.
• Abstract（参考訳）: 近年のディープニューラルネットワーク(dnn)の発展により、安全性クリティカルなシステムへの採用が進み、安全性の保証の必要性が高まっている。 これらのDNNの安全性特性は、検証コミュニティが開発したツールを用いて証明することができる。 しかし、これらのツール自体が実装バグや数値安定性の問題を起こしやすいため、信頼性が疑わしい。 これを解決するために、一部の検証者は、信頼できるチェッカーによってチェックできる結果の証明を生成する。 本稿では,DNN検証のための検証チェッカーの実装について述べる。 数値安定性と高い妥当性を提供することにより、既存の実装を改善する。 これを実現するために、工業的定理証明器であるimandraの2つの重要な能力、すなわち無限精度実数演算とその形式的検証基盤を活用した。 これまでのところ、我々はImandraに証明チェッカーを実装し、その正当性を規定し、チェッカーのコンプライアンスを検証し始めた。 現在進行中の作業は、チェッカーの正式な検証を完了し、パフォーマンスをさらに最適化することに集中しています。

関連論文リスト

• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• A Certified Proof Checker for Deep Neural Network Verification [0.9895793818721335]
  Imandra における Marabou 検証アルゴリズムの代替実装を提案する。 これにより、アルゴリズムの基盤となる数学的結果の証明を含む、正式な保証付きの実装を得ることができる。
  論文  参考訳（メタデータ） (2024-05-17T08:16:32Z)
• The Decisive Power of Indecision: Low-Variance Risk-Limiting Audits and Election Contestation via Marginal Mark Recording [51.82772358241505]
  リスクリミット監査(リスクリミット監査、RLA)は、大規模な選挙の結果を検証する技術である。 我々は、効率を改善し、統計力の進歩を提供する監査の新たなファミリーを定めている。 新しい監査は、複数の可能なマーク解釈を宣言できるように、キャストボイトレコードの標準概念を再考することで実現される。
  論文  参考訳（メタデータ） (2024-02-09T16:23:54Z)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees [3.208888890455612]
  VNN(Verification-Friendly Neural Networks)を生成するための新しいフレームワークを提案する。 本稿では,予測性能と検証親和性とのバランスをとるための学習後最適化フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-12-15T12:39:27Z)
• Cal-DETR: Calibrated Detection Transformer [67.75361289429013]
  本稿では,Deformable-DETR,UP-DETR,DINOのキャリブレーション検出トランス(Cal-DETR)のメカニズムを提案する。 我々は、不確実性を利用してクラスロジットを変調する不確実性誘導ロジット変調機構を開発する。 その結果、Cal-DETRは、ドメイン内およびドメイン外の両方を校正する競合する列車時間法に対して有効であることがわかった。
  論文  参考訳（メタデータ） (2023-11-06T22:13:10Z)
• Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees [86.1362094580439]
  安全プロパティとDNNが与えられた場合、安全であるプロパティ入力領域のすべての領域の集合を列挙する。 この問題の #P-hardness のため,epsilon-ProVe と呼ばれる効率的な近似法を提案する。 提案手法は, 許容限界の統計的予測により得られた出力可到達集合の制御可能な過小評価を利用する。
  論文  参考訳（メタデータ） (2023-08-18T22:30:35Z)
• 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)
• Neural Network Verification with Proof Production [7.898605407936655]
  そこで本研究では,Simplex ベースの DNN 検証器を実証生産能力で拡張するための新しいメカニズムを提案する。 我々の証明生産は、よく知られたファルカスの補題の効率的な適応に基づいている。 航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースにおいて, 証明生産が成功することを示すものである。
  論文  参考訳（メタデータ） (2022-06-01T14:14:37Z)
• Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
  ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。 本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。 われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
  論文  参考訳（メタデータ） (2020-02-17T09:53:50Z)

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

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