A wide range of verification methods have been proposed to verify the safety properties of deep neural networks ensuring that the networks function correctly in critical applications. However, many well-known verification tools still struggle with complicated network architectures and large network sizes. In this work, we propose a network reduction technique as a pre-processing method prior to verification. The proposed method reduces neural networks via eliminating stable ReLU neurons, and transforming them into a sequential neural network consisting of ReLU and Affine layers which can be handled by the most verification tools. We instantiate the reduction technique on the state-of-the-art complete and incomplete verification tools, including alpha-beta-crown, VeriNet and PRIMA. Our experiments on a large set of benchmarks indicate that the proposed technique can significantly reduce neural networks and speed up existing verification tools. Furthermore, the experiment results also show that network reduction can improve the availability of existing verification tools on many networks by reducing them into sequential neural networks.
Slides (ASE2023.pptx) | 7.88MiB |
Thu 14 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Program Verification 2Research Papers / Tool Demonstrations / NIER Track at Room E Chair(s): Martin Kellogg New Jersey Institute of Technology | ||
10:30 12mTalk | Expediting Neural Network Verification via Network Reduction Research Papers Yuyi Zhong National University of Singapore, Singapore, Ruiwei Wang School of Computing, National University of Singapore, Siau-Cheng Khoo National University of Singapore Pre-print File Attached | ||
10:42 12mTalk | SMT Solver Validation Empowered by Large Pre-trained Language Models Research Papers Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Yang Wang National Key Laboratory for Novel Software Technology, Nanjing University, Ming Wen Huazhong University of Science and Technology, Haoxiang Jia Huazhong University of Science and Technology, Yuming Zhou Nanjing University Pre-print File Attached | ||
10:54 12mTalk | LIV: Invariant Validation Using Straight-Line Programs Tool Demonstrations Pre-print Media Attached File Attached | ||
11:06 12mTalk | CEGAR-PT: A Tool for Abstraction by Program Transformation Tool Demonstrations Pre-print Media Attached File Attached | ||
11:18 12mTalk | Symbolic Verification of Fuzzy Logic ModelsRecorded talk NIER Track Siang Zhao School of Computer, National University of Defense Technology, China, Zhongyang Li School of Computer, National University of Defense Technology, China, Zhenbang Chen National University of Defense Technology, Ji Wang School of Computer, National University of Defense Technology, China Pre-print Media Attached | ||
11:30 12mTalk | HOBAT: Batch Verification for Homogeneous Structural Neural NetworksRecorded talk Research Papers Media Attached File Attached |