“Parallelization Techniques for Verifying Neural Networks” by Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett. In Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 128-137.
Inspired by recent successes of parallel techniques for solving Boolean satisfiability, we investigate a set of strategies and heuristics to leverage parallelism and improve the scalability of neural network verification. We present a general description of the Split-and-Conquer partitioning algorithm, implemented within the Marabou framework, and discuss its parameters and heuristic choices. In particular, we explore two novel partitioning strategies, that partition the input space or the phases of the neuron activations, respectively. We introduce a branching heuristic and a direction heuristic that are based on the notion of polarity. We also introduce a highly parallelizable pre-processing algorithm for simplifying neural network verification problems. An extensive experimental evaluation shows the benefit of these techniques on both existing and new benchmarks. A preliminary experiment ultra-scaling our algorithm using a large distributed cloud-based platform also shows promising results.
BibTeX entry:
@inproceedings{WOZ+20,
author = {Haoze Wu and Alex Ozdemir and Aleksandar Zelji{\'c} and Kyle
Julian and Ahmed Irfan and Divya Gopinath and Sadjad Fouladi and
Guy Katz and Corina Pasareanu and Clark Barrett},
editor = {Alexander Ivrii and Ofer Strichman},
title = {Parallelization Techniques for Verifying Neural Networks},
booktitle = {Proceedings of the {\it 20^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '20)},
pages = {128--137},
publisher = {TU Wien Academic Press},
month = sep,
year = {2020},
doi = {10.34727/2020/isbn.978-3-85448-042-6_20},
url = {http://theory.stanford.edu/~barrett/pubs/WOZ+20.pdf}
}
(This webpage was created with bibtex2web.)