抽象与精化：面向可扩展且精确的神经网络验证
软件工程
2022-07-05 v1 机器学习
摘要
作为一种新的编程范式，深度神经网络（DNN）已日益在实践中部署，但缺乏鲁棒性阻碍其在安全关键领域的应用。尽管存在具有形式化保证的 DNN 验证技术，它们在可扩展性和准确性上受限。本文中，我们提出一种新颖的抽象-精化方法，用于可扩展且精确的 DNN 验证。具体而言，我们提出一种新颖的抽象，通过过近似来分解 DNN 的规模。若未报告伪反例，验证抽象 DNN 的结果总是确定的。为消除抽象引入的伪反例，我们提出一种新颖的反例引导精化，将抽象 DNN 精化以排除给定伪反例，同时仍过近似原始 DNN。我们的方法与许多现有验证技术正交且可集成。为演示，我们使用两个有前景且精确的工具 Marabou 和 Planet 作为底层验证引擎实现我们的方法，并在广泛使用的基准 ACAS Xu、MNIST 和 CIFAR-10 上评估。结果显示我们的方法可通过解决更多问题并分别减少多达 86.3% 和 78.0% 的验证时间以提升其性能。与最相关的抽象-精化方法相比，我们的方法快 11.6-26.6 倍。
引用
@article{arxiv.2207.00759,
title = {Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks},
author = {Jiaxiang Liu and Yunhan Xing and Xiaomu Shi and Fu Song and Zhiwu Xu and Zhong Ming},
journal= {arXiv preprint arXiv:2207.00759},
year = {2022}
}