Certifying the robustness of neural networks against adversarial attacks is
essential to their reliable adoption in safety-critical systems such as
autonomous driving and medical diagnosis. Unfortunately, state-of-the-art
verifiers either do not scale to bigger networks or are too imprecise to prove
robustness, limiting their practical adoption. In this work, we introduce
GPUPoly, a scalable verifier that can prove the robustness of significantly
larger deep neural networks than previously possible. The key technical insight
behind GPUPoly is the design of custom, sound polyhedra algorithms for neural
network verification on a GPU. Our algorithms leverage the available GPU
parallelism and inherent sparsity of the underlying verification task. GPUPoly
scales to large networks: for example, it can prove the robustness of a 1M
neuron, 34-layer deep residual network in approximately 34.5 ms. We believe
GPUPoly is a promising step towards practical verification of real-world neural
networks.