Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)

要約

その卓越した学習能力と実世界アプリケーションにおける性能により、ニューラルネットワーク（NN）に基づく機械学習システムの利用は継続的に増加している。しかし、様々な事例研究や経験的知見から、NNの入力にわずかな変化を加えるだけで、誤った望ましくないNNの動作につながることが示唆されている。このため、与えられたNNの動作に関する保証を提供することを目的とした、NNの形式的解析に大きな関心が集まっています。既存のフレームワークは、充足可能性解法や線形計画法を用いて、学習済みNNのロバスト性や安全性を保証している。我々は、より広範なNNの特性を解析するために、モデル検査に基づく最初のフレームワークであるFANNetを提案した。しかし、モデル検査に伴う状態空間の爆発はスケーラビリティの問題を伴い、FANNetは小規模なNNにしか適用できない。本研究では、形式的なNN解析のスケーラビリティとタイミング効率を改善するために、状態空間削減と入力分割のアプローチを開発する。これにより、最先端のFANNetと比較して、検証のタイミングオーバーヘッドを最大8000分の1に削減し、約80$倍のネットワークパラメータを持つNNにも適用できる。これにより、FANNetにすでに含まれているすべてのNNの特性に加えて、新しいフレームワークを用いたNNの安全特性の解析が可能になる。このフレームワークは、よく知られているACAS Xu NNsと同様に、ヘルスケアデータセットで訓練されたNNの特性を効率的に分析できることが示されている。

要約(オリジナル)

Owing to their remarkable learning capabilities and performance in real-world applications, the use of machine learning systems based on Neural Networks (NNs) has been continuously increasing. However, various case studies and empirical findings in the literature suggest that slight variations to NN inputs can lead to erroneous and undesirable NN behavior. This has led to considerable interest in their formal analysis, aiming to provide guarantees regarding a given NN’s behavior. Existing frameworks provide robustness and/or safety guarantees for the trained NNs, using satisfiability solving and linear programming. We proposed FANNet, the first model checking-based framework for analyzing a broader range of NN properties. However, the state-space explosion associated with model checking entails a scalability problem, making the FANNet applicable only to small NNs. This work develops state-space reduction and input segmentation approaches, to improve the scalability and timing efficiency of formal NN analysis. Compared to the state-of-the-art FANNet, this enables our new model checking-based framework to reduce the verification’s timing overhead by a factor of up to 8000, making the framework applicable to NNs even with approximately $80$ times more network parameters. This in turn allows the analysis of NN safety properties using the new framework, in addition to all the NN properties already included with FANNet. The framework is shown to be efficiently able to analyze properties of NNs trained on healthcare datasets as well as the well–acknowledged ACAS Xu NNs.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL