論文の概要: A Formally Verified Robustness Certifier for Neural Networks (Extended Version)

• arxiv url: http://arxiv.org/abs/2505.06958v1
• Date: Sun, 11 May 2025 12:05:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-13 20:21:49.132886
• Title: A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
• Title（参考訳）: ニューラルネットワーク用形式検証ロバスト性証明器(拡張版)
• Authors: James Tobler, Hira Taqdees Syeda, Toby Murray,
• Abstract要約: ニューラルネットワークは入力中の小さな摂動の影響を受けやすいため、それらが誤分類される。 グローバルなロバストニューラルネットワークは、入力の分類がそのような摂動によって変更できないことを証明するために機能を使用する。 本稿では,プログラムとその仕様,実装と検証に要する重要な設計決定について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called certified robust. However, to the authors' knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.
• Abstract（参考訳）: ニューラルネットワークは入力中の小さな摂動の影響を受けやすいことが多く、それが誤分類を引き起こしている。 この問題に対する最近の解決策は、入力の分類がそのような摂動によって変更できないことを証明する関数を使用する、グローバルロバストニューラルネットワークの使用である。 このテストに合格したアウトプットは、認証されたロバストと呼ばれる。 しかし、著者の知識では、これらの認証機能は実装レベルではまだ検証されていない。 これまでの未検証実装が、ある状況下では、どう有効に正しくないかを実証する。 さらに、パワーイテレーションのような近似ベースのアルゴリズムをしばしば頼りにしており、(意外なことに)音質は保証されない。 与えられた出力が堅牢であることを保証するため,ダフニーのグローバルロバストニューラルネットワークの認証機能を実装し,正式に検証した。 我々は,プログラムとその仕様,実装と検証に要する重要な設計決定,および実際に適用した経験について述べる。

関連論文リスト

• Verifying Global Neural Network Specifications using Hyperproperties [0.0]
  すべての潜在的な入力の保証を提供するグローバル仕様について研究する。 私たちのフォーマリズムは、既存のニューラルネットワーク検証アプローチを使用して、グローバル仕様の検証を可能にします。 特定のグローバルな仕様を検証する最近の成功は、すべての潜在的なデータポイントに対する強力な保証が実現可能であることを示している。
  論文  参考訳（メタデータ） (2023-06-21T18:08:55Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。 近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。 本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
  論文  参考訳（メタデータ） (2022-11-29T13:32:38Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  我々は, 正規サンプルの分布を低次元多様体で支持する異常検出において, 特定のユースケースに焦点を当てた。 我々は、訓練中に識別情報を活用する自己指導型学習体制に適応するが、通常の例のサブ多様体に焦点をあてる。 製造領域における視覚異常検出のための挑戦的なベンチマークであるMVTec ADデータセットで、最先端の新たな結果を達成する。
  論文  参考訳（メタデータ） (2022-06-23T14:16:30Z)
• Fast Falsification of Neural Networks using Property Directed Testing [0.1529342790344802]
  本稿では,反例の探索を指示するニューラルネットワークの偽造アルゴリズムを提案する。 提案アルゴリズムは, 微分自由サンプリングに基づく最適化手法を用いる。 フェールシフィケーション手順は、他の検証ツールが安全でないと報告しているすべての安全でないインスタンスを検出する。
  論文  参考訳（メタデータ） (2021-04-26T09:16:27Z)
• Data-Driven Assessment of Deep Neural Networks with Random Input Uncertainty [14.191310794366075]
  我々は,ネットワーク出力の安全性を同時に証明し,ローカライズ可能なデータ駆動最適化手法を開発した。 深部ReLUネットワークにおける提案手法の有効性とトラクタビリティを実験的に実証した。
  論文  参考訳（メタデータ） (2020-10-02T19:13:35Z)
• Exploiting Verified Neural Networks via Floating Point Numerical Error [15.639601066641099]
  検証者は、ニューラルネットワークが空間内のすべての入力に対して特定の特性を保証するかどうかに答えようとしている。 浮動小数点誤差の無視は、実際に体系的に活用できる不健全な検証につながることを示す。
  論文  参考訳（メタデータ） (2020-03-06T03:58:26Z)
• Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
  ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。 本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。 われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
  論文  参考訳（メタデータ） (2020-02-17T09:53:50Z)

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

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