Towards an effective and interpretable refinement approach for DNN verification
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 hinderin...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2023
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/8641 https://ink.library.smu.edu.sg/context/sis_research/article/9644/viewcontent/qrs23_Surgeon_av.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-9644 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-96442024-02-08T07:46:19Z Towards an effective and interpretable refinement approach for DNN verification LI, Jiaying BAI, Guangdong PHAM, Long H. SUN, Jun 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. 2023-10-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/8641 info:doi/10.1109/QRS60937.2023.00062 https://ink.library.smu.edu.sg/context/sis_research/article/9644/viewcontent/qrs23_Surgeon_av.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University abstraction debugging abstraction refinement neural network verification Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
abstraction debugging abstraction refinement neural network verification Software Engineering |
spellingShingle |
abstraction debugging abstraction refinement neural network verification Software Engineering LI, Jiaying BAI, Guangdong PHAM, Long H. SUN, Jun Towards an effective and interpretable refinement approach for DNN verification |
description |
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. |
format |
text |
author |
LI, Jiaying BAI, Guangdong PHAM, Long H. SUN, Jun |
author_facet |
LI, Jiaying BAI, Guangdong PHAM, Long H. SUN, Jun |
author_sort |
LI, Jiaying |
title |
Towards an effective and interpretable refinement approach for DNN verification |
title_short |
Towards an effective and interpretable refinement approach for DNN verification |
title_full |
Towards an effective and interpretable refinement approach for DNN verification |
title_fullStr |
Towards an effective and interpretable refinement approach for DNN verification |
title_full_unstemmed |
Towards an effective and interpretable refinement approach for DNN verification |
title_sort |
towards an effective and interpretable refinement approach for dnn verification |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2023 |
url |
https://ink.library.smu.edu.sg/sis_research/8641 https://ink.library.smu.edu.sg/context/sis_research/article/9644/viewcontent/qrs23_Surgeon_av.pdf |
_version_ |
1794549515941838848 |