Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
10-2023
Abstract
Recently, several abstraction refinement techniques have been proposed to improve the verification precision for deep neural networks (DNNs). However, these techniques usually take many refinement steps to verify a property and the refinement decision in each step is hard to interpret, thus hindering their analysis, reasoning and optimization.In this work, we propose SURGEON, a novel DNN verification refinement approach that is both effective and interpretable, allowing analyst to understand why and how each refinement decision is made. The main insight is to leverage the ‘interpretable’ nature of debugging processes and formulate the verification refinement problem as a debugging problem. Given a failed verification procedure, SURGEON refines it in an iterative manner and, in each iteration, it effectively identifies the root cause of the failure and heuristically generates fixes according to abstract transformers.We have implemented SURGEON in a prototype and evaluated it using a set of local robustness verification problems. Besides the interpretability, the experimental results show our approach can improve the precision of base verification methods and is more effective than existing refinement techniques.
Keywords
abstraction debugging, abstraction refinement, neural network verification
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security (QRS): Chang Mai, October 22-26: Proceedings
First Page
569
Last Page
580
ISBN
9798350319583
Identifier
10.1109/QRS60937.2023.00062
Publisher
IEEE
City or Country
Piscataway, NJ
Citation
LI, Jiaying; BAI, Guangdong; PHAM, Long H.; and SUN, Jun.
Towards an effective and interpretable refinement approach for DNN verification. (2023). 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security (QRS): Chang Mai, October 22-26: Proceedings. 569-580.
Available at: https://ink.library.smu.edu.sg/sis_research/8641
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/QRS60937.2023.00062