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.

本文提出了一种保守的神经网络缩减方法，该方法能够在验证减小的网络的同时，确保验证原始网络，可以适用于任何类型的激活函数，使得网络能够被缩小到不到原来的 5% 的大小，从而显著减少了验证时间。