一句话：提出面向 DNN 的可扩展定量验证框架 PROVERO，用测试驱动方式证明概率性质，并可验证大规模网络的鲁棒性。
深度神经网络虽功能强大，但其可信性仍待解决。现有测试方法可扩展到大规模网络却缺乏形式保证，而验证方法有保证但难扩展。本文提出可扩展的定量验证框架：一种测试驱动方法，通过执行足够测试直至能够证明目标概率性质成立，从而兼得可扩展性与形式保证；该框架可认证确定性和随机化 DNN 的性质，并实现为 PROVERO。作者将其用于认证 DNN 的对抗鲁棒性：提出一种与攻击无关的鲁棒性度量，为大规模 DNN 生成鲁棒性证书，而现有最先进验证工具在此无法给出结论。该工作还支持黑盒访问场景。
Despite the functional success of deep Neural Networks, their trustworthiness remains a crucial open challenge. To address this challenge, both testing and verification techniques have been proposed. But these existing techniques provide either scalability to large networks or formal guarantees, not both. In this paper, we propose a scalable quantitative verification framework for deep Neural Networks, i.e., a test-driven approach that comes with formal guarantees that a desired probabilistic property is satisfied. Our technique performs enough tests until soundness of a formal probabilistic property can be proven. It can be used to certify properties of both deterministic and randomized DNNs. We implement our approach in a tool called PROVERO and apply it in the context of certifying adversarial robustness of DNNs. In this context, we first show a new attack-agnostic measure of robustness which offers an alternative to purely attack-based methodology of evaluating robustness being reported today. Second, PROVERO provides certificates of robustness for large DNNs, where existing state-of-the-art verification tools fail to produce conclusive results. Our work paves the way forward for verifying properties of distributions captured by real-world deep Neural Networks, with provable guarantees, even where testers only have black-box access to the neural network.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{BalutaCMS21,
title = {Scalable Quantitative Verification for Deep Neural Networks},
author = {Teodora Baluta and Zheng Leong Chua and Kuldeep S. Meel and Prateek Saxena},
booktitle = {ICSE},
year = {2021},
doi = {10.1109/icse43902.2021.00039}
}