Specification-Driven Neural Network Reduction for Scalable Formal Verification

要約

タイトル：拡張可能な形式検証のための仕様駆動型ニューラルネットワークの削減

要約：

-ニューラルネットワークの形式検証は、安全を確保するために必要不可欠です。

-しかし、現在のニューラルネットワークの形式検証方法は、多数のニューロンを含む実用的な問題に対処するにはまだ拡張性が不十分です。

-本研究では、この課題に対処するために、未検証ネットワークのバージョン変換に基づくニューラルネットワークの削減手法を提案しています。この手法により、削減されたネットワークの検証が元のネットワークの検証に等しいことが保証されます。

-本手法は、非線形層の出力が似ているニューロンをまとめることにより、任意の活性化関数（ReLU、シグモイド、tanhなど）を持つニューラルネットワークに適用可能です。

-本研究の評価により、本手法を用いることでネットワークを通常の5％以下にまで削減でき、同様に検証時間も短縮されます。

要約(オリジナル)

Formal verification of neural networks is essential before their deployment in safety-critical settings. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems that involve a large number of neurons. In this work, we propose a novel approach to address this challenge: A conservative neural network reduction approach that ensures that the verification of the reduced network implies the verification of the original network. Our approach constructs the reduction on-the-fly, while simultaneously verifying the original network and its specifications. The reduction merges all neurons of a nonlinear layer with similar outputs and is applicable to neural networks with any type of activation function such as ReLU, sigmoid, and tanh. Our evaluation shows that our approach can reduce a network to less than 5% of the number of neurons and thus to a similar degree the verification time is reduced.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI