The robustness of neural network classifiers is important in the safety-critical domain and can be quantified by robustness verification. At present, efficient and scalable verification techniques are always sound but incomplete, and thus, the improvement of verified robustness results is the key criterion to evaluate the performance of incomplete verification approaches. The multi-variate function MaxPool is widely adopted yet challenging to verify. In this paper, we present Ti-Lin, a robustness verifier for MaxPool-based CNNs with Tight Linear Approximation. Following the sequel of minimizing the over-approximation zone of the non-linear function of CNNs, we are the first to propose the provably neuron-wise tightest linear bounds for the MaxPool function. By our proposed linear bounds, we can certify larger robustness results for CNNs. We evaluate the effectiveness of Ti-Lin on different verification frameworks with open-sourced benchmarks, including LeNet, PointNet, and networks trained on the MNIST, CIFAR-10, Tiny ImageNet and ModelNet40 datasets. Experimental results show that Ti-Lin significantly outperforms the state-of-the-art methods across all networks with up to 78.6% improvement in terms of the certified accuracy with almost the same time consumption as the fastest tool. Our code is available at https://github.com/xiaoyuanpigo/Ti-Lin-Hybrid-Lin.

翻译：神经网络分类器的鲁棒性在安全关键领域至关重要，可通过鲁棒性验证进行量化。目前，高效且可扩展的验证技术通常是可靠但不完备的，因此，已验证鲁棒性结果的提升是评估不完备验证方法性能的关键标准。多元函数MaxPool被广泛采用但验证具有挑战性。本文提出Ti-Lin，一种基于紧致线性近似的MaxPool型CNN鲁棒性验证器。遵循最小化CNN非线性函数过近似区域的思路，我们首次为MaxPool函数提出了可证明的神经元级最紧线性边界。通过我们提出的线性边界，能够为CNN认证更大的鲁棒性结果。我们在开源基准测试（包括LeNet、PointNet以及在MNIST、CIFAR-10、Tiny ImageNet和ModelNet40数据集上训练的网络）上，通过不同验证框架评估了Ti-Lin的有效性。实验结果表明，Ti-Lin在所有网络上均显著优于现有最优方法，在认证准确率方面最高提升78.6%，且时间消耗与最快工具几乎相同。我们的代码发布于https://github.com/xiaoyuanpigo/Ti-Lin-Hybrid-Lin。