影から脱却: ニューラルネットワークの検証のための隠れ空間の探求

arXiv:2505.17854v3 Announce Type: replace 要約: ニューラルネットワークは汎用性が高いが、入力値の微小な変化に対して敏感である。したがって、安全性が極めて重要なアプリケーションにおいて予期しない挙動を防ぐためには、形式検証という知られ難い課題の解決が必要となる。現在、最先端の検証アルゴリズムは、ニューラルネットワークの出力可能集合を囲み込むために到達性解析または抽象解釈を使用している。しばしば、この囲み込みの厳密性のために検証結果が結論が出ない場合がある。この問題を解決するため、我々は新しい仕様導出型入力洗浄手続きを提案した。具体的には、不安全性な出力に対するニューラルネットワークの逆写像を反復して囲み込み、入力可能集合のみが不安全性なものだけを囲み込めるように削減していく。そのために、投影ベースの集合表現がニューラルネットワークを通じて伝達される過程におけるアーチファクトである「隠れ空間」を活用し、出力仕様を入力空間に転移させる。投影ベースの集合表現（例えば、ゾノトープ）は、更高次元の集合、すなわち「隠れ空間」の「影」であり、その集合がニューラルネットワークを通じて伝達される過程において変化しない。したがって、入力集合と出力の囲み込みは、我々が制約を転移するために使用できる同一の「隠れ空間」の「影」である。我々は、この反復洗浄を利用し、枝探索手順における部分問題の数を大幅に削減する、ニューラルネットワーク用の効率的な検証ツールを提示した。ゾノトープを集合表現として使用する場合、我々のアプローチは他の多くの最先端のアプローチとは異なり、行列演算のみを使用して実現できるため、効率的な GPU アクセラレーションを通じて著しい速度向上を実現した。我々は、我々のツールが国際的なニューラルネットワーク検証コンペティションで上位を争うツールと比較して競争力のある性能を発揮することを示した。

arXiv:2505.17854v3 Announce Type: replace 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 propose a novel specification-driven input refinement procedure, i.e., we iteratively enclose the preimage of a neural network for all unsafe outputs to reduce the set of possible inputs to only enclose the unsafe ones. For that, we transfer output specifications to the input space by exploiting a latent space, which is an artifact of the propagation of a projection-based set representation through a neural network. A projection-based set representation, e.g., a zonotope, 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 compared to the top-ranking tools of the international neural network verification competition.