神经网络分类器在安全关键领域中的鲁棒性至关重要，并可通过鲁棒性验证进行量化。目前，高效的可扩展验证技术总是正确但不完备，因此，验证鲁棒性的提升是评估不完备验证方法性能的关键标准。多变量函数MaxPool被广泛采用，但其验证具有挑战性。本文提出Ti-Lin，一种基于紧密线性逼近的MaxPool网络鲁棒性验证器。遵循最小化CNN非线性函数的过近似区域的思路，我们首次提出了对MaxPool函数而言理论上最紧密的神经元级线性边界。通过所提出的线性边界，我们可以为CNN认证更大的鲁棒性结果。我们在不同的开源基准框架下评估了Ti-Lin的有效性，包括LeNet、PointNet以及在MNIST、CIFAR-10、Tiny ImageNet和ModelNet40数据集上训练的网络。实验结果显示，Ti-Lin在所有网络上的认证准确率比最先进的方法提高了高达78.6%，而时间消耗几乎与最快工具相同。我们的代码可在https://github.com/xiaoyuanpigo/Ti-Lin-Hybrid-Lin获取。

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.