使用符号区间的神经网络形式化安全分析

由于深度神经网络日益被部署在包括自动驾驶汽车和防碰撞系统在内的现实世界安全关键领域，形式化地检查 DNN 的安全属性，尤其是在不同的攻击者能力下，正变得至关重要。现有的大多数 DNN 安全测试技术试图寻找对抗样本，而未提供关于此类对抗样本不存在的任何形式化安全保证。最近，几个项目使用了不同类型的可满足性模理论求解器来形式化地检查 DNN 的安全属性。然而，所有这些方法都受到求解器引起的高开销的限制。在本文中，我们提出了一种不使用 SMT 求解器形式化地检查 DNN 安全属性的新方向。相反，我们利用区间算术来计算 DNN 输出的严格边界。与现有的基于求解器的方法不同，我们的方法易于并行化。我们进一步提出了符号区间分析以及几种其他优化方法，以最小化输出边界的过估计。我们设计、实现并评估了我们的方法，作为 ReluVal 的一部分，这是一个用于形式化检查基于 Relu 的 DNN 安全属性的系统。我们广泛的实证结果表明，ReluVal 平均比最先进的基于求解器的系统 Reluplex 快 200 倍。在一台没有 GPU 的单台 8 核机器上，ReluVal 能够在 4 小时内验证一个安全属性，而 Reluplex 在运行超过 5 天后因超时而判定该属性无法确定。我们的实验表明，符号区间分析是严格分析 DNN 不同安全属性的一个有前景的新方向。