Formal verification of neural networks is critical for their safe  adoption in real-world applications. However, designing a  verifier which can handle realistic networks in a precise manner remains an open and difficult challenge. In this paper, we take a major step in addressing this challenge and present a new  framework, called PRIMA , that computes precise convex approximations of arbitrary non-linear activations. PRIMA is based on novel approximation algorithms that compute the convex hull of polytopes, leveraging concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss. We evaluate the effectiveness of PRIMA on challenging neural networks with ReLU, Sigmoid, and Tanh activations . Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness for up to 16 \%, 30\%, and 34\% more images than prior work on ReLU-, Sigmoid-, and Tanh-based networks, respectively  .
Formal verification of neural networks is critical for their safe and secure 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 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 approximations involving 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 image classifiers from prior work . Our results show that PRIMA is significantly more precise than state-of-the-art, verifying robustness for up to 14 \%, 30\%, and 34\% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively . Further, PRIMA enables, for the first time, precise verification of a realistic neural network for autonomous driving within a few minutes .
A
and secure
A
precise and scalable
R
realistic networks in a precise manner
different activation functions, realistic network architectures and relevant specifications
A
verification
R
, that
. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it
R
of arbitrary non-linear activations. PRIMA is based on novel
involving multiple neurons via novel convex hull
R
compute the convex hull of polytopes, leveraging
leverage
R
challenging neural networks with ReLU, Sigmoid, and Tanh activations
a variety of challenging image classifiers from prior work
D
the
R
16
14
R
prior
existing
A
. Further, PRIMA enables, for the first time, precise verification of a realistic neural network for autonomous driving within a few minutes