SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Sun 22 Oct 2023 16:30 - 17:00 at Room I - Quantum, neural Chair(s): Roberto Giacobazzi

Formal verification of neural networks is essential for their deployment in safety-critical real-world applications, such as autonomous driving and cyber-physical controlling. Multi-neuron convex relaxation is one of the mainstream methods to improve verification precision. However, existing techniques rely on empirically selecting neuron groups before performing multi-neuron convex relaxation, which may yield redundant yet expensive convex hull computations. This paper proposes a volume approximation-based approach for selecting neuron groups. We approximate the volumes of convex hulls for all group candidates, without calculating their convex hulls. The group candidates with small volumes are then selected for convex hull computation, aiming at ruling out unnecessary convex hulls with loose relaxation. We implement our approach as the neural network verification tool FaGMR, and evaluate it with state-of-the-art tools on neural networks trained by MNIST and CIFAR-10. The experimental results demonstrate that FaGMR is more efficient than the state-of-the-art works, yet with better precision in most of the cases.

Sun 22 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
Quantum, neuralSAS 2023 at Room I
Chair(s): Roberto Giacobazzi University of Arizona
16:00
30m
Talk
Quantum Constant Propagation
SAS 2023
Yanbin Chen TUM School of Computation, Information and Technology, Technical University of Munich, Yannick Stade TUM School of Computation, Information and Technology, Technical University of Munich
Pre-print
16:30
30m
Talk
Boosting Multi-Neuron Convex Relaxation for Neural Network Verification
SAS 2023
Xuezhou Tang ShenZhen University, Ye Zheng Shenzhen University, Jiaxiang Liu Shenzhen University
Pre-print