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.

本文介绍了一个名为PRIMA的新验证框架，它可以处理任何非线性激活函数，通过利用来自计算几何的新型凸包逼近算法计算多个神经元的精确凸性抽象，能够比现有技术更精确地验证ReLU、Sigmoid和Tanh网络，并且有助于实现对自动驾驶现实神经网络的精确验证。

PRIMA: 通过可扩展的凸包逼近实现通用和精确的神经网络认证