| Title | Scalable Quantitative Verification for Deep Neural Networks |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Baluta, Teodora, Chua, Zheng Leong, Meel, Kuldeep S., Saxena, Prateek |
| Conference Name | 2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) |
| Keywords | compositionality, deep-neural-networks, Metrics, Neural networks, probabilistic, Probabilistic logic, pubcrawl, quantitative-verification, resilience, Resiliency, Robustness, Scalability, scalable verification, software engineering, Testing, Tools |
| Abstract | Despite the functional success of deep neural networks (DNNs), their trustworthiness remains a crucial open challenge. To address this challenge, both testing and verification techniques have been proposed. But these existing techniques pro- vide 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 PROVERO1 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 | 10.1109/ICSE-Companion52605.2021.00115 |
| Citation Key | baluta_scalable_2021 |
Scalable Quantitative Verification for Deep Neural Networks