論文の概要: Out of the Shadows: Exploring a Latent Space for Neural Network Verification

• arxiv url: http://arxiv.org/abs/2505.17854v1
• Date: Fri, 23 May 2025 13:05:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-26 18:08:34.087927
• Title: Out of the Shadows: Exploring a Latent Space for Neural Network Verification
• Title（参考訳）: 影の外 - ニューラルネットワーク検証のための潜伏空間を探る
• Authors: Lukas Koller, Tobias Ladner, Matthias Althoff,
• Abstract要約: 本稿では, 分岐・束縛手順におけるサブプロブレム数を大幅に削減するために, 繰り返し改良を用いたニューラルネットワークの効率的な検証ツールを提案する。 当社のツールは,前回のニューラルネットワーク検証コンペで上位のツールに位置づけられるような,競争力のあるパフォーマンスを実現していることを実証しています。
• 参考スコア（独自算出の注目度）: 8.97708612393722
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks are ubiquitous. However, they are often sensitive to small input changes. Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary. Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we design a novel latent space for formal verification that enables the transfer of output specifications to the input space for an iterative specification-driven input refinement, i.e., we iteratively reduce the set of possible inputs to only enclose the unsafe ones. The latent space is constructed from a novel view of projection-based set representations, e.g., zonotopes, which are commonly used in reachability analysis of neural networks. A projection-based set representation is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints. We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure. Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance, which would place it among the top-ranking tools of the last neural network verification competition (VNN-COMP'24).
• Abstract（参考訳）: ニューラルネットワークはユビキタスです。 しかし、しばしば小さな入力の変化に敏感である。 したがって、安全クリティカルなアプリケーションにおける予期せぬ動作を防止するためには、正式な検証 -- 悪名高い難しい問題 -- が必要である。 多くの最先端検証アルゴリズムは、到達可能性分析または抽象解釈を使用して、ニューラルネットワークの可能な出力のセットを囲む。 しばしば、封筒の保守性のために検証は不確定である。 この問題に対処するため、我々は、反復的な仕様駆動型入力精錬のための入力空間への出力仕様の転送を可能にする、形式検証のための新しい潜在空間、すなわち、安全でないものだけを囲む可能性のある入力のセットを反復的に削減する、形式検証のための新しい潜在空間を設計する。 潜在空間は、ニューラルネットワークの到達可能性解析に一般的に用いられる射影に基づく集合表現(例えば、ゾノトープ)の新しいビューから構築される。 プロジェクションベースの集合表現は、ニューラルネットワークを介してセットの伝搬中に変化しない高次元の集合(潜在空間)の「影」である。 したがって、入力集合と出力囲いは、制約を伝達するために使用できるのと同じ潜在空間の「影」である。 本稿では, 分岐・束縛手順におけるサブプロブレム数を大幅に削減するために, 繰り返し改良を用いたニューラルネットワークの効率的な検証ツールを提案する。 ゾノトープを集合表現として用いることは、他の多くの最先端アプローチとは異なり、我々のアプローチは行列演算のみを用いることで実現でき、効率の良いGPUアクセラレーションによる大幅な高速化が可能となる。 我々のツールは、最後のニューラルネットワーク検証コンテスト(VNN-COMP'24)の最上位ツールに位置づけられる競争性能を達成することを実証する。

関連論文リスト

• Set-Based Training for Neural Network Verification [8.97708612393722]
  小さな入力摂動はニューラルネットワークの出力に大きな影響を与える。 安全クリティカルな環境の安全性を確保するためには、ニューラルネットワークの堅牢性を検証する必要がある。 本稿では,可能な出力の集合を計算するための,新しいセットベーストレーニング手順を提案する。
  論文  参考訳（メタデータ） (2024-01-26T15:52:41Z)
• Provably Bounding Neural Network Preimages [18.810882386083655]
  InVPROPアルゴリズムは線形に制約された出力セットの事前画像上の特性を検証する。 他のアプローチとは対照的に、効率的なアルゴリズムはGPU加速であり、線形プログラミング解決器を必要としない。 その結果, 従来よりも2.5倍速く, 2500倍以上の過近似が得られていることがわかった。
  論文  参考訳（メタデータ） (2023-02-02T20:34:45Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Verifying Low-dimensional Input Neural Networks via Input Quantization [12.42030531015912]
  本稿では,ACAS Xu ネットワーク検証の当初の問題を再考する。 本稿では,入力量子化層をネットワークにプリペイドすることを提案する。 本手法は,浮動小数点誤差に耐性のない正確な検証結果を提供する。
  論文  参考訳（メタデータ） (2021-08-18T03:42:05Z)
• SignalNet: A Low Resolution Sinusoid Decomposition and Estimation Network [79.04274563889548]
  本稿では,正弦波数を検出するニューラルネットワークアーキテクチャであるSignalNetを提案する。 基礎となるデータ分布と比較して,ネットワークの結果を比較するための最悪の学習しきい値を導入する。 シミュレーションでは、我々のアルゴリズムは常に3ビットデータのしきい値を超えることができるが、しばしば1ビットデータのしきい値を超えることはできない。
  論文  参考訳（メタデータ） (2021-06-10T04:21:20Z)
• Artificial Neural Networks generated by Low Discrepancy Sequences [59.51653996175648]
  我々は、高密度ネットワークグラフ上のランダムウォーキングとして、人工ニューラルネットワークを生成する。 このようなネットワークはスクラッチからスパースを訓練することができ、高密度ネットワークをトレーニングし、その後圧縮する高価な手順を避けることができる。 我々は,低差分シーケンスで生成された人工ニューラルネットワークが,より低い計算複雑性で,密度の高いニューラルネットワークの到達範囲内で精度を達成できることを実証した。
  論文  参考訳（メタデータ） (2021-03-05T08:45:43Z)

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

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