nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement
nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement
复制标题
DOI：
10.1007/978-3-030-76384-8_2
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Stanley Bak
中科院分区：
文献类型：
--
作者：
Stanley Bak
对深度神经网络应用的兴趣激增导致了对此类架构的验证方法的兴趣激增。2020年夏季，举办了首届神经网络验证国际竞赛。本文介绍并评估了在thenvision工具中使用的主要优化，这些优化优于ACAS Xu基准类别中的所有其他工具，有时甚至是几个数量级。该方法使用快速抽象来提高速度，并通过ReLU拆分进行细化，以在无法证明属性时提高准确性。虽然抽象细化过程是形式化方法中的经典方法，但直接将其应用于神经网络验证问题实际上会降低性能，因为使用抽象时会产生级联的过度近似错误。这使得优化及其系统评估对于高性能至关重要。
The surge of interest in applications of deep neural networks has led to a surge of interest in verification methods for such architectures. In summer 2020, the first international competition on neural network verification was held. This paper presents and evaluates the main optimizations used in thennenumtool, which outperformed all other tools in the ACAS Xu benchmark category, sometimes by orders of magnitude. The method uses fast abstractions for speed, combined with refinement through ReLU splitting to increase accuracy when properties cannot be proven. Although the abstraction refinement process is a classic approach in formal methods, directly applying it to the neural network verification problem actually reduces performance, due to a cascade of overapproxmation error when using abstraction. This makes optimizations and their systematic evaluation essential for high performance.