An Abstraction-Based Framework for Neural Network Verification
An Abstraction-Based Framework for Neural Network Verification
复制标题
DOI：
10.1007/978-3-030-53288-8_3
复制
发表时间：
2020-06-13
期刊：
影响因子：
--
通讯作者：
Katz G
中科院分区：
文献类型：
--
作者：
Elboher YY;Gottschlich J;Katz G
深度神经网络越来越多地被用作安全关键系统的控制器。由于神经网络是不透明的，证明其正确性是一个巨大的挑战。为了解决这个问题，最近提出了几种神经网络验证方法。然而，这些方法提供的可扩展性有限，将它们应用于大型网络可能具有挑战性。在本文中，我们提出了一个框架，它可以通过使用过逼近来缩小网络的规模，从而增强神经网络验证技术，从而使其更易于验证。我们进行近似，如果该性质适用于较小的(抽象)网络，则它也适用于原始网络。过度近似可能太粗糙，在这种情况下，底层验证工具可能返回虚假的反例。在这种情况下，我们进行反例指导的求精来调整近似值，然后重复这个过程。我们的方法与许多现有的验证技术是正交的，并且可以与之集成。出于评估目的，我们将其与最近提出的Marabou框架进行了集成，并观察到Marabou的性能有了显著的改进。我们的实验证明了我们的方法在验证更大的神经网络方面的巨大潜力。
Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been proposed. However, these approaches afford limited scalability, and applying them to large networks can be challenging. In this paper, we propose a framework that can enhance neural network verification techniques by using over-approximation to reduce the size of the network—thus making it more amenable to verification. We perform the approximation such that if the property holds for the smaller (abstract) network, it holds for the original as well. The over-approximation may be too coarse, in which case the underlying verification tool might return a spurious counterexample. Under such conditions, we perform counterexample-guided refinement to adjust the approximation, and then repeat the process. Our approach is orthogonal to, and can be integrated with, many existing verification techniques. For evaluation purposes, we integrate it with the recently proposed Marabou framework, and observe a significant improvement in Marabou’s performance. Our experiments demonstrate the great potential of our approach for verifying larger neural networks.
影响因子：
14.9
作者：
Hinton, Geoffrey;Deng, Li;Kingsbury, Brian
通讯作者：
Kingsbury, Brian
DOI：
10.4204/eptcs.257.3
发表时间：
2017-01-01
影响因子：
--
作者：
Katz, Guy;Barrett, Clark;Kochenderfer, Mykel J.
通讯作者：
Kochenderfer, Mykel J.
影响因子：
22.7
作者：
Krizhevsky, Alex;Sutskever, Ilya;Hinton, Geoffrey E.
通讯作者：
Hinton, Geoffrey E.