通过状态空间约简与输入分割扩展深度神经网络分析的模型检测规模（扩展版）
机器学习
2023-07-04 v2
摘要
由于其卓越的学习能力和在现实应用中的性能，基于神经网络（NNs）的机器学习系统的使用在持续增加。然而，文献中的各种案例研究和实证结果表明，NN输入的微小变化可能导致错误和不良的NN行为。这引起了对其形式化分析的相当大兴趣，旨在提供关于给定NN行为的保证。现有框架使用可满足性求解和线性规划为训练后的NN提供鲁棒性和/或安全性保证。我们提出了FANNet，第一个基于模型检测的框架，用于分析更广泛的NN属性。然而，与模型检测相关的状态空间爆炸带来了可扩展性问题，使得FANNet仅适用于小型NN。本工作开发了状态空间约简和输入分割方法，以提高形式化NN分析的可扩展性和时间效率。与最先进的FANNet相比，这使得我们新的基于模型检测的框架将验证的时间开销降低了最高8000倍，使该框架可应用于网络参数大约多倍的NN。这反过来允许使用新框架分析NN安全属性，此外还包括FANNet已涵盖的所有NN属性。该框架被证明能够有效分析在医疗数据集上训练的NN以及公认的ACAS Xu NN的属性。
引用
@article{arxiv.2306.17323,
title = {Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)},
author = {Mahum Naseer and Osman Hasan and Muhammad Shafique},
journal= {arXiv preprint arXiv:2306.17323},
year = {2023}
}