Verifying Binary Neural Networks on Continuous Input Space using Star Reachability
Verifying Binary Neural Networks on Continuous Input Space using Star Reachability
复制标题
DOI：
10.1109/formalise58978.2023.00009
复制
发表时间：
2023-05
期刊：
影响因子：
--
通讯作者：
M. Ivashchenko;Sung-Woo Choi;L. V. Nguyen;Hoang-Dung Tran
中科院分区：
文献类型：
--
作者：
M. Ivashchenko;Sung-Woo Choi;L. V. Nguyen;Hoang-Dung Tran
深度神经网络（DNN）已成为解决各种现实问题的流行工具。 DNN 的复杂结构使它们能够学习复杂的表示和特征。因此，二元神经网络（BNN）广泛应用于边缘设备，例如微型计算机。然而，架构细节和浮点数的使用导致计算操作复杂性增加。与其他 DNN 一样，BNN 很容易受到对抗性攻击；即使对输入集的微小扰动也可能导致错误的输出。不幸的是，只有少数几种方法被提出来验证 BNN。本文提出了一种使用星可达性分析在连续输入空间上验证 BNN 的方法。我们的方法可以使用符号激活函数计算精确和过度近似的 BNN 可达集，并使用它们进行验证。在网络不安全的情况下，所提出的方法还可以有效地构建一套完整的反例。我们在 NNV 中实施了我们的方法，NNV 是一种用于 DNN 和支持学习的网络物理系统的神经网络验证工具。实验结果表明，与最近在 Marabou 中实现的基于 SMT 的方法相比，我们基于星型的方法保守性更低，效率更高，并且可扩展。我们还提供了与基于量化的工具 EEVBNN 的比较。
Deep Neural Networks (DNNs) have become a popular instrument for solving various real-world problems. DNNs’ sophisticated structure allows them to learn complex representations and features. For this reason, Binary Neural Networks (BNNs) are widely used on edge devices, such as microcomputers. However, architecture specifics and floating-point number usage result in an increased computational operations complexity. Like other DNNs, BNNs are vulnerable to adversarial attacks; even a small perturbation to the input set may lead to an errant output. Unfortunately, only a few approaches have been proposed for verifying BNNs.This paper proposes an approach to verify BNNs on continuous input space using star reachability analysis. Our approach can compute both exact and overapproximate reachable sets of BNNs with Sign activation functions and use them for verification. The proposed approach is also efficient in constructing a complete set of counterexamples in case a network is unsafe. We implemented our approach in NNV, a neural network verification tool for DNNs and learning-enabled Cyber-Physical Systems. The experimental results show that our star-based approach is less conservative, more efficient, and scalable than the recent SMT-based method implemented in Marabou. We also provide a comparison with a quantization-based tool EEVBNN.