Tue 17 Jan 2023 10:00 - 10:30 at Arlington - Keynote and contribution paper Chair(s): Michael Emmi

As neural networks have taken on a critical role in real-world applications, formal verification is earnestly needed to guarantee the safety properties of the networks. However, it remains challenging to balance the trade-off between precision and efficiency in abstract interpretation based verification methods. In this paper, we propose an abstract refinement process that leverages the convex hull techniques to improve the analysis efficiency. Specifically, we introduce the double description method in the convex polytope domain to detect and eliminate multiple spurious adversarial labels simultaneously. We also combine the new activation relaxation technique with the iterative abstract refinement method to compensate for the precision loss during abstract interpretation. We have implemented our proposal into a verification framework named ARENA, and assessed its effectiveness by conducting a series of experiments. These experiments show that ARENA yields significantly better verification precision compared to the existing abstract-refinement-based tool DeepSRGR. It also identifies falsification by detecting adversarial examples, with reasonable execution efficiency. Lastly, it verifies more images than the state-of-the-art verifiers PRIMA (CPU-based) and alpha-beta-crown (GPU-based).

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Keynote and contribution paperVMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
Differential Verification of Deep Neural Networks
Chao Wang University of Southern California
ARENA: Enhancing Abstract Refinement for Neural Network Verification
Yuyi Zhong , Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore