论文标题
DeepGalaxy：通过二维输入空间探索测试神经网络验证器
DeepGalaxy: Testing Neural Network Verifiers via Two-Dimensional Input Space Exploration
论文作者
论文摘要
深度神经网络（DNN）在许多领域都广泛开发和应用，DNN的质量保证至关重要。神经网络验证（NNV）旨在为DNN模型提供正式的保证。与传统软件类似，神经网络验证器也可能包含错误，这将产生严重和严重的影响，尤其是在安全领域。但是，在验证神经网络验证符方面几乎没有工作。在这项工作中，我们提出了DeepGalaxy，这是一种基于差异测试的自动化方法，以解决此问题。具体而言，我们（1）提出了一系列突变规则，包括模型水平突变和规范水平突变，以有效地探索神经网络验证器的二维输入空间； （2）提出启发式策略以选择测试用例。我们利用我们对Deepgalaxy的实施来测试三个最先进的神经网络验证Marabou，Eran和Neurify。实验结果支持深galaxy的效率和有效性。此外，发现了五个独特的未知错误
Deep neural networks (DNNs) are widely developed and applied in many areas, and the quality assurance of DNNs is critical. Neural network verification (NNV) aims to provide formal guarantees to DNN models. Similar to traditional software, neural network verifiers could also contain bugs, which would have a critical and serious impact, especially in safety-critical areas. However, little work exists on validating neural network verifiers. In this work, we propose DeepGalaxy, an automated approach based on differential testing to tackle this problem. Specifically, we (1) propose a line of mutation rules, including model level mutation and specification level mutation, to effectively explore the two-dimensional input space of neural network verifiers; and (2) propose heuristic strategies to select test cases. We leveraged our implementation of DeepGalaxy to test three state-of-the-art neural network verifies, Marabou, Eran, and Neurify. The experimental results support the efficiency and effectiveness of DeepGalaxy. Moreover, five unique unknown bugs were discovered
