Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
复制标题
DOI：
10.1007/978-3-030-53288-8_4
复制
发表时间：
2020-06-13
期刊：
影响因子：
--
通讯作者：
Johnson TT
中科院分区：
文献类型：
--
作者：
Bak S;Tran HD;Hobbs K;Johnson TT
神经网络提供了对复杂函数的快速逼近，并且越来越多地用于感知和控制任务。然而，对于关键任务和安全关键应用，分析神经网络能做什么和不能做什么是很重要的。对于具有ReLU激活函数的前馈神经网络，虽然精确分析是np完备的，但最近提出的验证方法有时可以成功。神经网络验证的主要实际问题是分析运行时间过长。即使在小型网络上，理论上完整的工具有时也会运行几天而没有产生结果。在本文中，我们通过改进最近提出的几何路径枚举方法来解决运行时问题。通过一系列优化，其中一些是新的算法改进，我们证明了在经过充分研究的ACAS Xu基准上精确分析的显着速度提高，有时比原始实现快数百倍。在更困难的基准测试实例上，我们优化的方法通常是最快的，甚至优于利用过度近似和细化的不精确方法。
Neural networks provide quick approximations to complex functions, and have been increasingly used in perception as well as control tasks. For use in mission-critical and safety-critical applications, however, it is important to be able to analyze what a neural network can and cannot do. For feed-forward neural networks with ReLU activation functions, although exact analysis is NP-complete, recently-proposed verification methods can sometimes succeed. The main practical problem with neural network verification is excessive analysis runtime. Even on small networks, tools that are theoretically complete can sometimes run for days without producing a result. In this paper, we work to address the runtime problem by improving upon a recently-proposed geometric path enumeration method. Through a series of optimizations, several of which are new algorithmic improvements, we demonstrate significant speed improvement of exact analysis on the well-studied ACAS Xu benchmarks, sometimes hundreds of times faster than the original implementation. On more difficult benchmark instances, our optimized approach is often the fastest, even outperforming inexact methods that leverage overapproximation and refinement.
DOI：
10.1007/978-3-030-53288-8_1
发表时间：
2020-06-13
期刊：
Computer Aided Verification
影响因子：
--
作者：
Tran HD;Yang X;Manzanas Lopez D;Musau P;Nguyen LV;Xiang W;Bak S;Johnson TT
通讯作者：
Johnson TT
DOI：
10.1109/tnnls.2018.2808470
发表时间：
2018-11-01
影响因子：
10.4
作者：
Xiang, Weiming;Hoang-Dung Tran;Johnson, Taylor T.
通讯作者：
Johnson, Taylor T.