論文の概要: SoundnessBench: A Soundness Benchmark for Neural Network Verifiers
- arxiv url: http://arxiv.org/abs/2412.03154v2
- Date: Tue, 14 Oct 2025 19:22:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-16 20:13:28.243996
- Title: SoundnessBench: A Soundness Benchmark for Neural Network Verifiers
- Title（参考訳）: SoundnessBench: ニューラルネットワーク検証のためのサウンドネスベンチマーク
- Authors: Xingjian Zhou, Keyi Shen, Andy Xu, Hongji Xu, Cho-Jui Hsieh, Huan Zhang, Zhouxing Shi,
- Abstract要約: NN検証のための新しいベンチマーク「SoundnessBench」を開発した。
SoundnessBenchは、敵の攻撃から隠された意図的に挿入された反例を持つインスタンスで構成されている。
我々のトレーニングは,隠れた反例を効果的に生成し,SoundnessBenchは最先端のNN検証器のバグの同定に成功したことを実証する。
- 参考スコア（独自算出の注目度）: 45.86647998712757
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Neural network (NN) verification aims to formally verify properties of NNs, which is crucial for ensuring the behavior of NN-based models in safety-critical applications. In recent years, the community has developed many NN verifiers and benchmarks to evaluate them. However, existing benchmarks typically lack ground-truth for hard instances where no current verifier can verify the property and no counterexample can be found. This makes it difficult to validate the soundness of a verifier, when it claims verification on such challenging instances that no other verifier can handle. In this work, we develop a new benchmark for NN verification, named "SoundnessBench", specifically for testing the soundness of NN verifiers. SoundnessBench consists of instances with deliberately inserted counterexamples that are hidden from adversarial attacks commonly used to find counterexamples. Thereby, it can identify false verification claims when hidden counterexamples are known to exist. We design a training method to produce NNs with hidden counterexamples and systematically construct our SoundnessBench with instances across various model architectures, activation functions, and input data. We demonstrate that our training effectively produces hidden counterexamples and our SoundnessBench successfully identifies bugs in state-of-the-art 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検証の健全性をテストするため,新しいNN検証ベンチマーク "SoundnessBench" を開発した。
SoundnessBenchは、意図的に挿入された反例を持つインスタンスで構成されており、反例を見つけるために一般的に使用される敵攻撃から隠されている。
これにより、隠れた反例が存在することがわかっている場合に、偽の検証のクレームを識別することができる。
我々は,隠れた反例を持つNNを設計し,様々なモデルアーキテクチャ,アクティベーション関数,入力データにまたがるインスタンスを用いたSoundnessBenchを体系的に構築する訓練手法を設計する。
我々のトレーニングは,隠れた反例を効果的に生成し,SoundnessBenchは最先端のNN検証器のバグの同定に成功したことを実証する。
私たちのコードはhttps://github.com/MVP-Harry/SoundnessBenchで、ベンチマークはhttps://huggingface.co/datasets/SoundnessBench/SoundnessBenchで利用可能です。
関連論文リスト
- Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
グラフニューラルネットワーク(GNN)におけるラベルフリップの正確な認証手法を提案する。
本稿では,ノード分類タスクにおける広範囲なGNNアーキテクチャの認証に本手法を適用した。
私たちの研究は、ニューラルネットワークによって引き起こされた毒殺攻撃に対する最初の正確な認証を提示します。
論文 参考訳（メタデータ） (2024-11-30T17:05:12Z) - 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) - 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) - Adversarial Examples Detection with Bayesian Neural Network [57.185482121807716]
本稿では,ランダムな成分が予測器の滑らかさを向上できるという観測によって動機づけられた敵の例を検出するための新しい枠組みを提案する。
本稿では,BATer を略した新しいベイズ対向型サンプル検出器を提案し,対向型サンプル検出の性能を向上させる。
論文 参考訳（メタデータ） (2021-05-18T15:51:24Z) - Understanding Classifier Mistakes with Generative Models [88.20470690631372]
ディープニューラルネットワークは教師付き学習タスクに有効であるが、脆弱であることが示されている。
本稿では、生成モデルを利用して、分類器が一般化に失敗するインスタンスを特定し、特徴付ける。
我々のアプローチは、トレーニングセットのクラスラベルに依存しないため、半教師付きでトレーニングされたモデルに適用できる。
論文 参考訳（メタデータ） (2020-10-05T22:13:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。