Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Guy Katz Clark Barrett David Dill Kyle Julian and Mykel Kochenderfer
Abstract
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.
中文速览
深度神经网络在自动驾驶、无人机防撞等安全关键领域越来越常用，但如何从数学上严格证明它的行为符合预期，一直是个几乎无从下手的难题。研究团队提出了一种名为 Reluplex 的新算法，核心思路是把求解线性规划的经典工具"单纯形法（simplex method）"加以扩展，使其能直接处理神经网络中最常见的非线性激活函数——线性整流单元（ReLU），从而把整个网络的验证问题转化为一个可搜索的约束满足问题，无需对网络做任何简化或近似。研究者以美国下一代无人机机载防撞系统（ACAS Xu）的45个原型神经网络为测试对象——每个网络有8层、300个ReLU节点——成功证明了"入侵者足够远时一定给出安全通行建议"等多条关键安全性质，所能处理的网络规模比已有方法大了整整一个数量级。这项工作为把深度神经网络真正部署到飞机、自动驾驶汽车等高风险场景提供了坚实的形式化验证基础。
原文 arXiv:1702.01135;中英对照 + 大白话阅读 https://aha.fim.ai/paper/1702.01135v2