論文の概要: Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples
- arxiv url: http://arxiv.org/abs/2412.03154v1
- Date: Wed, 04 Dec 2024 09:24:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-05 15:10:19.469908
- Title: Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples
- Title（参考訳）: ニューラルネットワーク検証器のテスト:隠れた反例を用いた音質ベンチマーク
- Authors: Xingjian Zhou, Hongji Xu, Andy Xu, Zhouxing Shi, Cho-Jui Hsieh, Huan Zhang,
- Abstract要約: 本稿では,NN検証のための音響性ベンチマークを提案する。
私たちのベンチマークには、意図的に挿入された反例のインスタンスが含まれています。
我々のベンチマークでは、最先端のNN検証器のバグと合成バグの識別に成功している。
- 参考スコア（独自算出の注目度）: 52.564617070814485
- License:
- Abstract: In recent years, many neural network (NN) verifiers have been developed to formally verify certain properties of neural networks such as robustness. Although many benchmarks have been constructed to evaluate the performance of NN verifiers, they typically lack a ground-truth for hard instances where no current verifier can verify and no counterexample can be found, which makes it difficult to check the soundness of a new verifier if it claims to verify hard instances which no other verifier can do. We propose to develop a soundness benchmark for NN verification. Our benchmark contains instances with deliberately inserted counterexamples while we also try to hide the counterexamples from regular adversarial attacks which can be used for finding counterexamples. We design a training method to produce neural networks with such hidden counterexamples. Our benchmark aims to be used for testing the soundness of NN verifiers and identifying falsely claimed verifiability when it is known that hidden counterexamples exist. We systematically construct our benchmark and generate instances across diverse model architectures, activation functions, input sizes, and perturbation radii. We demonstrate that our benchmark successfully identifies bugs in state-of-the-art NN verifiers, as well as synthetic bugs, providing a crucial step toward enhancing the reliability of testing NN verifiers. Our code is available at https://github.com/MVP-Harry/SoundnessBench and our benchmark is available at https://huggingface.co/datasets/SoundnessBench/SoundnessBench.
- Abstract（参考訳）: 近年、堅牢性などのニューラルネットワークの特定の特性を正式に検証するために、多くのニューラルネットワーク検証器が開発されている。
NN検証器の性能を評価するために多くのベンチマークが構築されているが、一般に、現在の検証器が検証できず、反例も見つからないハードインスタンスに対して基礎的真実を欠いているため、他の検証器ができないハードインスタンスを検証しようとする場合、新しい検証器の健全性を確認することは困難である。
本稿では,NN検証のための音響性ベンチマークを提案する。
我々のベンチマークには、意図的に挿入された反例のあるインスタンスが含まれており、また、反例を見つけるのに使用できる通常の敵攻撃から反例を隠そうとしています。
隠れた反例を持つニューラルネットワークを生成するためのトレーニング手法を設計する。
本ベンチマークは,NN検証者の正当性を検証し,隠れた反例が存在することを知れば,疑わしい検証可能性を確認することを目的としている。
ベンチマークを体系的に構築し、様々なモデルアーキテクチャ、アクティベーション関数、入力サイズ、摂動半径のインスタンスを生成する。
我々のベンチマークでは、最先端のNN検証器のバグと合成バグの識別に成功し、NN検証器のテストの信頼性を高めるための重要なステップとなることを実証している。
私たちのコードはhttps://github.com/MVP-Harry/SoundnessBenchで、ベンチマークはhttps://huggingface.co/datasets/SoundnessBench/SoundnessBenchで利用可能です。
関連論文リスト
- Revisiting Differential Verification: Equivalence Verification with Confidence [0.6562256987706128]
検証済みニューラルネットワーク(NN)がデプロイ前にプルーニング(および再トレーニング)されると、新しいNNが元のNNと同等に振る舞うことを証明することが望ましい。
本稿では,NN間の差異を推論する差分検証の考え方を再考する。
論文 参考訳（メタデータ） (2024-10-26T15:53:25Z) - A Certified Proof Checker for Deep Neural Network Verification [0.9895793818721335]
Imandra における Marabou 検証アルゴリズムの代替実装を提案する。
これにより、アルゴリズムの基盤となる数学的結果の証明を含む、正式な保証付きの実装を得ることができる。
論文 参考訳（メタデータ） (2024-05-17T08:16:32Z) - Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
NNCS検証のための制御理論の再利用を可能にする最初の一般手法を提案する。
dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。
本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
論文 参考訳（メタデータ） (2024-02-16T16:15:25Z) - Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
本稿では,DNN検証のための検証チェッカーの実装について述べる。
数値安定性と高い妥当性を提供することにより、既存の実装を改善する。
論文 参考訳（メタデータ） (2023-07-12T16:53:32Z) - Latent Feature Relation Consistency for Adversarial Robustness [80.24334635105829]
深層ニューラルネットワークは、人間の知覚できない敵のノイズを自然の例に付加する敵の例を予測するときに、誤分類が起こる。
textbfLatent textbfFeature textbfRelation textbfConsistency (textbfLFRC)を提案する。
LFRCは、潜在空間における逆例の関係を、自然例と整合性に制約する。
論文 参考訳（メタデータ） (2023-03-29T13:50:01Z) - 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) - VPN: Verification of Poisoning in Neural Networks [11.221552724154988]
我々は、別のニューラルネットワークセキュリティ問題、すなわちデータ中毒について研究する。
この場合、アタッカーがトレーニングデータのサブセットにトリガーを挿入するので、テスト時にこのトリガーが入力され、トレーニングされたモデルがターゲットクラスに誤って分類される。
我々は、市販の検証ツールでチェックできるプロパティとして、データ中毒のチェックを定式化する方法を示す。
論文 参考訳（メタデータ） (2022-05-08T15:16:05Z) - Spotting adversarial samples for speaker verification by neural vocoders [102.1486475058963]
我々は、自動話者検証(ASV)のための敵対サンプルを見つけるために、ニューラルボコーダを採用する。
元の音声と再合成音声のASVスコアの違いは、真正と逆正のサンプルの識別に良い指標であることがわかった。
私たちのコードは、将来的な比較作業のためにオープンソースにされます。
論文 参考訳（メタデータ） (2021-07-01T08:58:16Z) - Understanding Classifier Mistakes with Generative Models [88.20470690631372]
ディープニューラルネットワークは教師付き学習タスクに有効であるが、脆弱であることが示されている。
本稿では、生成モデルを利用して、分類器が一般化に失敗するインスタンスを特定し、特徴付ける。
我々のアプローチは、トレーニングセットのクラスラベルに依存しないため、半教師付きでトレーニングされたモデルに適用できる。
論文 参考訳（メタデータ） (2020-10-05T22:13:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。