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.

翻译：由于神经网络（NN）在现实应用中展现出的卓越学习能力与性能，基于神经网络的机器学习系统使用量持续增长。然而，文献中的多项案例研究与实证发现表明，NN输入的微小变化可能导致错误及非期望行为。这一现象引发了对其形式化分析的广泛关注，旨在为给定NN的行为提供保障。现有框架通过可满足性求解与线性规划方法，为已训练NN提供鲁棒性和/或安全性保证。我们提出了FANNet，首个基于模型检测的框架，用于分析更广泛的NN属性。但模型检测固有的状态空间爆炸问题导致其可扩展性受限，使FANNet仅适用于小型NN。本研究开发了状态空间缩减与输入分割方法，以提升形式化NN分析的可扩展性与时间效率。相较于最先进的FANNet，我们的新型模型检测框架可将验证时间开销降低最高达8000倍，使框架适用于网络参数数量约为原框架80倍的NN。这进一步使得新框架除支持FANNet已涵盖的全部NN属性外，还能分析NN的安全属性。实验表明，该框架能高效分析医疗数据集训练所得NN的属性，以及广受认可的ACAS Xu NN的属性。