Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

3-2021

Abstract

We propose a spurious region guided refinement approach for robustness verification of deep neural networks. Our method starts with applying the DeepPoly abstract domain to analyze the network. If the robustness property cannot be verified, the result is inconclusive. Due to the over-approximation, the computed region in the abstraction may be spurious in the sense that it does not contain any true counterexample. Our goal is to identify such spurious regions and use them to guide the abstraction refinement. The core idea is to make use of the obtained constraints of the abstraction to infer new bounds for the neurons. This is achieved by linear programming techniques. With the new bounds, we iteratively apply DeepPoly, aiming to eliminate spurious regions. We have implemented our approach in a prototypical tool DeepSRGR. Experimental results show that a large amount of regions can be identified as spurious, and as a result, the precision of DeepPoly can be significantly improved. As a side contribution, we show that our approach can be applied to verify quantitative robustness properties.

Keywords

deep neural networks, spurious regions, DeepPoly

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Tools and Algorithms for the Construction and Analysis of Systems TACAS 2021: Proceedings: Virtual, March 27 - April 1

Volume

12651

First Page

389

Last Page

408

ISBN

9783030720162

Identifier

10.1007/978-3-030-72016-2_21

Publisher

Springer

City or Country

Cham

Embargo Period

8-25-2021

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-030-72016-2_21

Download

Share

COinS