DualApp：通过欠近似实现神经网络鲁棒性验证的紧过近似

神经网络的鲁棒性对宿主系统的可靠性和安全性至关重要。形式化验证已被证明能有效地提供可证明的鲁棒性保证。为提升验证可扩展性，广泛采用以线性约束过近似神经网络中的非线性激活函数，从而将验证问题转化为可高效求解的线性规划问题。由于过近似不可避免地引入高估，许多工作致力于定义尽可能紧的近似。然而近期研究表明，现有所谓最紧近似互有优劣。本文中，我们识别并报告了定义紧近似时的一个关键因素，即激活函数的近似域。我们观察到现有方法仅依赖被高估的域，而相应的紧近似在其实际域上未必紧。我们提出一种新颖的欠近似引导方法，称为对偶近似，用于定义紧过近似，以及两种基于采样和梯度下降的互补欠近似算法。被高估的域保证可靠性，而被低估的域引导紧度。我们将该方法实现为名为 DualApp 的工具，并在包含 84 个收集并训练的不同架构神经网络的综合基准上进行了广泛评估。实验结果表明，DualApp 优于最先进的基于近似的方法，对验证结果的改进最高达 71.22%。