论文标题
针对神经网络验证的优化符号间隔传播
Optimized Symbolic Interval Propagation for Neural Network Verification
论文作者
论文摘要
神经网络越来越多地应用于安全关键领域，因此它们的验证变得重要。用于证明前馈神经网络的投入输出关系的最新算法是基于线性放松和符号间隔的传播。但是，由于依赖性变化，近似值随着网络深度的增加而恶化。在本文中，我们介绍了DPNeurifyFV，这是一种用于较低尺寸输入空间的Relu网络的新型分支和结合的求解器，基于符号间隔的传播，并具有新鲜的变量和输入分解。选择新鲜变量的新启发式方法可以改善依赖性问题，而我们的新颖的启发式启发式启发式，再加上其他一些改进，加快了分支和结合程序的速度。我们评估了我们在空中碰撞避免网络ACAS XU上的方法，与最先进的工具相比，我们证明了运行时的改进。
Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks are based on linear relaxations and symbolic interval propagation. However, due to variable dependencies, the approximations deteriorate with increasing depth of the network. In this paper we present DPNeurifyFV, a novel branch-and-bound solver for ReLU networks with low dimensional input-space that is based on symbolic interval propagation with fresh variables and input-splitting. A new heuristic for choosing the fresh variables allows to ameliorate the dependency problem, while our novel splitting heuristic, in combination with several other improvements, speeds up the branch-and-bound procedure. We evaluate our approach on the airborne collision avoidance networks ACAS Xu and demonstrate runtime improvements compared to state-of-the-art tools.
