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

arXiv: https://arxiv.org/abs/2306.17323 · HTML: https://mlsanity.com/paper/2306.17323/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 31 of its 79 references that are in the map.
- First posted on arXiv 29 Jun 2023.

## Builds on (most cited first, 30 of 31)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [Universal adversarial perturbations](https://mlsanity.com/paper/1610.08401/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Processing of Deep Neural Networks: A Tutorial and Survey](https://mlsanity.com/paper/1703.09039/) (2017)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Imbalanced-learn: A Python Toolbox to Tackle the Curse of Imbalanced Datasets in Machine Learning](https://mlsanity.com/paper/1609.06570/) (2016)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Technical Report on the CleverHans v2.1.0 Adversarial Examples Library](https://mlsanity.com/paper/1610.00768/) (2016)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Adversarial Example Detection for DNN Models: A Review and Experimental Comparison](https://mlsanity.com/paper/2105.00203/) (2021)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [DeepAbstract: Neural Network Abstraction for Accelerating Verification](https://mlsanity.com/paper/2006.13735/) (2020)
- [DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks](https://mlsanity.com/paper/1710.00486/) (2017)
- [Low Resolution Face Recognition Using a Two-Branch Deep Convolutional Neural Network Architecture](https://mlsanity.com/paper/1706.06247/) (2017)
- [A Deep Convolutional Neural Network for COVID-19 Detection Using Chest X-Rays](https://mlsanity.com/paper/2005.01578/) (2020)
- [TrISec: Training Data-Unaware Imperceptible Security Attacks on Deep Neural Networks](https://mlsanity.com/paper/1811.01031/) (2018)
- [FANNet: Formal Analysis of Noise Tolerance, Training Bias and Input Sensitivity in Neural Networks](https://mlsanity.com/paper/1912.01978/) (2019)

## Abstract (arXiv)

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.