Formal verification of neural networks is essential before their deployment in safety-critical settings. However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems that involve a large number of neurons. In this work, we propose a novel approach to address this challenge: A conservative neural network reduction approach that ensures that the verification of the reduced network implies the verification of the original network. Our approach constructs the reduction on-the-fly, while simultaneously verifying the original network and its specifications. The reduction merges all neurons of a nonlinear layer with similar outputs and is applicable to neural networks with any type of activation function such as ReLU, sigmoid, and tanh. Our evaluation shows that our approach can reduce a network to less than 5% of the number of neurons and thus to a similar degree the verification time is reduced.

翻译：在安全关键环境中部署神经网络之前，对其进行形式化验证至关重要。然而，现有的神经网络形式化验证方法尚难以扩展到处理包含大量神经元的实际问题。本文提出了一种新颖的方法来解决这一挑战：一种保守的神经网络约简方法，确保对约简网络的验证蕴含对原始网络的验证。该方法在验证原始网络及其规范的同时，动态构建约简过程。该约简通过合并非线性层中输出相似的神经元，适用于任何类型激活函数（如ReLU、sigmoid和tanh）的神经网络。评估表明，该方法可将网络神经元数量缩减至不足5%，从而验证时间也相应缩减至类似程度。