Parallelization Techniques for Verifying Neural Networks

Abstract

Inspired by recent successes with parallel optimization techniques for solving Boolean satisfiability, we investigate a set of strategies and heuristics that aim to leverage parallel computing to improve the scalability of neural network verification. We introduce an algorithm based on partitioning the verification problem in an iterative manner and explore two partitioning strategies, that work by partitioning the input space or by case splitting on the phases of the neuron activations, respectively. We also introduce a highly parallelizable pre-processing algorithm that uses the neuron activation phases to simplify the neural network verification problems. An extensive experimental evaluation shows the benefit of these techniques on both existing benchmarks and new benchmarks from the aviation domain. A preliminary experiment with ultra-scaling our algorithm using a large distributed cloud-based platform also shows promising results.

References in corpus (7)

• Formal Security Analysis of Neural Networks using Symbolic Intervals
• Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
• Deep Neural Network Compression for Aircraft Collision Avoidance Systems
• Efficient Formal Safety Analysis of Neural Networks
• Houdini: Fooling Deep Structured Prediction Models
• Towards Proving the Adversarial Robustness of Deep Neural Networks
• Algorithms for Verifying Deep Neural Networks

Cited by in corpus (2)

• UnbiasedNets: A Dataset Diversification Framework for Robustness Bias Alleviation in Neural Networks
• Pruning and Slicing Neural Networks using Formal Verification