Formal verification of neural networks is critical for their safe adoption in real-world applications. However, designing a precise and scalable verifier which can handle different activation functions, realistic network architectures and relevant specifications remains an open and difficult challenge.

In this paper, we take a major step forward in addressing this challenge and present a new verification framework, called PRIMA. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it computes precise convex abstractions involving \emph{multiple} neurons via novel convex hull approximation algorithms that leverage concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss.

We evaluate the effectiveness of PRIMA on a variety of challenging tasks from prior work. Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness to input perturbations for up to 20%, 30%, and 34% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively. Further, PRIMA enables, for the first time, the precise verification of a realistic neural network for autonomous driving within a few minutes.

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Foundation and Verification of Machine-Learning SystemsPOPL at Salon I
Chair(s): Gilbert Louis Bernstein University of California at Berkeley
10:20
25m
Research paper
A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson
POPL
Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI Media Attached
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore
DOI Media Attached
11:10
25m
Research paper
Interval Universal Approximation for Neural NetworksInPerson
POPL
Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin
DOI Media Attached
11:35
25m
Research paper
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson
POPL
Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
DOI Media Attached