CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual
Deep neural networks (DNNs) have achieved remarkable performance in a myriad of complex tasks. However, lack of robustness and black-box nature hinder their deployment in safety-critical systems. A large number of testing and formal verification techniques have been proposed recently, aiming to provide quality assurance for DNNs. Generally speaking, testing is a fast and simple way to disprove—but not to prove—certain properties of DNNs, while formal verification can provide correctness guarantees but often suffers from scalability and efficiency issues. In this work, we present a novel methodology, CLEVEREST, to accelerate formal verification of DNNs by synergistically combining testing and formal verification techniques based on the counterexample guided abstraction refinement (CEGAR) framework. We instantiate our methodology by leveraging CEGAR-NN, which is a CEGAR-based neural network verification method, and a representative adversarial attack method for testing. We conduct extensive experiments on the widely-used ACAS Xu DNN benchmark. The experimental results show that the testing can effectively reduce the usage of formal verification in the check-refine loop, hence significantly improves the efficiency.
Mon 5 DecDisplayed time zone: Auckland, Wellington change
13:30 - 15:00 | Numerical Static AnalysesSAS at AMRF Auditorium Chair(s): Isabella Mastroeni University of Verona, Italy | ||
13:30 30mTalk | CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual SAS Zhe Zhao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Jiaxiang Liu Shenzhen University | ||
14:00 30mTalk | Boosting Robustness Verification of Semantic Feature Neighborhoods SAS | ||
14:30 30mTalk | Lifting Numeric Relational Domains to Algebraic Data Types SAS Santiago Bautista Univ Rennes, Inria, CNRS, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria Pre-print File Attached |