Abstract
Neural networks are widely used in many applications ranging from classification to control. While these networks are composed of simple arithmetic operations, they are challenging to formally verify for properties such as reachability due to the presence of nonlinear activation functions. In this paper, we make the observation that Lipschitz continuity of a neural network not only can play a major role in the construction of reachable sets for neural-network controlled systems but also can be systematically controlled during training of the neural network. We build on this observation to develop a novel verification-aware knowledge distillation framework that transfers the knowledge of a trained network to a new and easier-to-verify network. Experimental results show that our method can substantially improve reachability analysis of neural-network controlled systems for several state-of-the-art tools.
Original language | English (US) |
---|---|
Title of host publication | 2019 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2019 - Digest of Technical Papers |
Publisher | Institute of Electrical and Electronics Engineers Inc. |
ISBN (Electronic) | 9781728123509 |
DOIs | |
State | Published - Nov 2019 |
Event | 38th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2019 - Westin Westminster, United States Duration: Nov 4 2019 → Nov 7 2019 |
Publication series
Name | IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD |
---|---|
Volume | 2019-November |
ISSN (Print) | 1092-3152 |
Conference
Conference | 38th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2019 |
---|---|
Country/Territory | United States |
City | Westin Westminster |
Period | 11/4/19 → 11/7/19 |
Funding
ACKNOWLEDGMENT This work was supported in part by the DARPA BRASS program under agreement number FA8750-16-C-0043, NSF under award number 1834701, 1834324, 1839511, 1724341 and 1646497, and by the Air Force Research Laboratory (AFRL).
ASJC Scopus subject areas
- Software
- Computer Science Applications
- Computer Graphics and Computer-Aided Design