DeepGalaxy：通过二维的输入空间探索测试神经网络验证器
DeepGalaxy: Testing Neural Network Verifiers via Two-Dimensional Input Space Exploration
摘要：
深度神经网络（DNN）在许多领域得到了广泛的发展和应用，DNN的质量保证至关重要。神经网络验证（NNV）的目的是为DNN模型提供形式化的保证。与传统软件类似，神经网络验证器也可能包含错误，这将产生关键和严重的影响，特别是在安全关键领域。然而，很少有工作存在的神经网络验证。在这项工作中，我们提出了DeepGalaxy，一种基于差分测试的自动化方法来解决这个问题。具体而言，我们（1）提出了一系列变异规则，包括模型级变异和规格说明级变异，以有效地探索神经网络验证器的二维的【形】输入空间;和（2）提出启发式策略来选择测试用例。我们利用DeepGalaxy的实现来测试三个最先进的神经网络验证，Marabou，Eran和Neuriify。实验结果支持DeepGalaxy的效率和有效性。此外，还发现了五种独特的未知错误，
英文摘要：
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
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
