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

TL;DR

This paper introduces a scalable model checking framework for neural network analysis that employs state-space reduction and input segmentation, significantly improving efficiency and enabling analysis of larger, real-world neural networks.

Contribution

It develops novel state-space reduction and input segmentation techniques that enhance the scalability of model checking for neural network analysis, extending applicability to larger networks.

Findings

Reduces verification time by up to 8000 times compared to FANNet.

Enables analysis of neural networks with approximately 80 times more parameters.

Successfully analyzes properties of healthcare and ACAS Xu neural networks.

Abstract

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.