DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting
This addresses the challenge of scalable verification for deep neural networks, which is crucial for safety-critical applications like image classification and reinforcement learning, though it is incremental in improving tractability over existing convex relaxation methods.
The paper tackles the problem of verifying worst-case performance of deep neural networks against input perturbations by proposing a novel operator splitting method that solves convex relaxations to high accuracy, demonstrating scalability to large convolutional networks and neural network dynamical systems.
Analyzing the worst-case performance of deep neural networks against input perturbations amounts to solving a large-scale non-convex optimization problem, for which several past works have proposed convex relaxations as a promising alternative. However, even for reasonably-sized neural networks, these relaxations are not tractable, and so must be replaced by even weaker relaxations in practice. In this work, we propose a novel operator splitting method that can directly solve a convex relaxation of the problem to high accuracy, by splitting it into smaller sub-problems that often have analytical solutions. The method is modular, scales to very large problem instances, and compromises operations that are amenable to fast parallelization with GPU acceleration. We demonstrate our method in bounding the worst-case performance of large convolutional networks in image classification and reinforcement learning settings, and in reachability analysis of neural network dynamical systems.