一句话：提出 PRIMA，用可扩展凸包近似实现通用且精确的神经网络形式认证。
神经网络的形式验证对其安全部署至关重要，但现有验证器难以兼顾精度、可扩展性、激活函数通用性和现实网络架构。本文提出 PRIMA 验证框架：它可处理任意非线性激活函数，并利用计算几何中的新凸包近似算法，对多神经元计算精确的凸抽象，从而在多项式复杂度下得到更少约束并最小化精度损失。作者在多种挑战性任务上评估 PRIMA，结果显示其在 ReLU、Sigmoid 和 Tanh 网络上分别比现有工作多验证最多 20%、30% 和 34% 的输入扰动鲁棒性图像；并首次在数分钟内完成对现实自动驾驶神经网络的精确验证。
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 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.
@article{paperbot1579,
title = {PRIMA: general and precise neural network certification via scalable convex hull approximations},
author = {Mark Niklas Müller and Gleb Makarchuk and Gagandeep Singh and Markus Püschel and Martin Vechev},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498704}
}