Fully Automatic Neural Network Reduction for Formal Verification

要約

安全性が重要なアプリケーションにニューラル ネットワークを導入する前に、ニューラル ネットワークを正式に検証することが不可欠です。
ただし、ニューラル ネットワークを正式に検証するための既存の方法は、多数のニューロンが関与する実際的な問題を処理できるほど拡張性がまだ不十分です。
私たちは、到達可能性分析を使用したニューラル ネットワークの完全自動かつ健全な削減を導入することで、この課題に対処します。
健全性により、縮小されたネットワークの検証には元のネットワークの検証が伴うことが保証されます。
私たちの知る限り、ReLU、シグモイド、tanh など、あらゆる種類の要素ごとの活性化関数を備えたニューラル ネットワークに適用できる最初のサウンド低減アプローチを紹介します。
ネットワークの削減は、元のネットワークとその仕様を同時に検証しながら、オンザフライで計算されます。
すべてのパラメータは、検証可能性を損なうことなくネットワーク サイズを最小限に抑えるために自動的に調整されます。
さらに、同様の隣接ピクセルを明示的に利用することにより、畳み込みニューラル ネットワークへのアプローチの適用可能性を示します。
私たちの評価では、私たちのアプローチは、わずかな外側近似によってニューロンの数を元のニューロンの数の一部に減らすことができ、したがって検証時間を同程度に短縮できることが示されています。

要約(オリジナル)

Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems involving a large number of neurons. We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. To the best of our knowledge, we present the first sound reduction approach that is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh. The network reduction is computed on the fly while simultaneously verifying the original network and its specifications. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach can reduce the number of neurons to a fraction of the original number of neurons with minor outer-approximation and thus reduce the verification time to a similar degree.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google