Pareto DNN Verification: Fast for Most Queries

Formal verification of deep neural networks (DNNs) faces a fundamental scalability challenge: verifying robustness is NP-hard and state-of-the-art tools often time out on modern architectures. We propose PAreto VErification, or PAVE: by augmenting DNNs with early exits (EEs) and verifying exit-by-exit, we solve the vast majority of robustness queries---roughly 80\%---in a small fraction of the total time. The key insight is that most inputs in a robustness neighborhood exit at an early layer, a provably tractable sub-problem, so verification terminates far before analyzing the full network. EEs can be added to any DNN without degrading accuracy (within 0.3\% across all tested architectures). We formalize the novel robustness property for EE networks, prove it is Fixed-Parameter Tractable under a trace stability condition (which commonly holds in practice), and present a sound and complete verification algorithm. Two sound optimizations---$break$ (early termination when the winner dominates) and $continue$ (skipping the inner loop when no runner-up can win)---reduce SAFE-case verification time by up to $10 \times$. Experiments on MNIST, CIFAR-10, and CIFAR-100 with networks from 600K to 33M parameters demonstrate that PAVE enables solving queries that were not solved otherwise, including formal verification of ResNet-18 on CIFAR-100.