Towards General Robustness Verification of MaxPool-based Convolutional Neural Networks via Tightening Linear Approximation

TL;DR

This work tackles robustness verification for MaxPool-based CNNs by tightening the linear approximation of MaxPool, enabling larger certified lower bounds under adversarial perturbations. It introduces MaxLin, a verifier that achieves block-wise tightest upper bounds and integrates with CNN-Cert and ERAN to cover diverse architectures and perturbation forms. Empirical results show significant gains in tightness (up to 110.60% improvement) and speed (up to 5.13×) across MNIST, CIFAR-10, Tiny ImageNet, and even PointNet models, demonstrating broad applicability and practical impact for safety-critical deployments. The approach advances scalable, precise robustness verification for complex MaxPool-based systems, offering a practical path toward provable guarantees in real-world applications.

Abstract

The robustness of convolutional neural networks (CNNs) is vital to modern AI-driven systems. It can be quantified by formal verification by providing a certified lower bound, within which any perturbation does not alter the original input's classification result. It is challenging due to nonlinear components, such as MaxPool. At present, many verification methods are sound but risk losing some precision to enhance efficiency and scalability, and thus, a certified lower bound is a crucial criterion for evaluating the performance of verification tools. In this paper, we present MaxLin, a robustness verifier for MaxPool-based CNNs with tight linear approximation. By tightening the linear approximation of the MaxPool function, we can certify larger certified lower bounds of CNNs. We evaluate MaxLin with open-sourced benchmarks, including LeNet and networks trained on the MNIST, CIFAR-10, and Tiny ImageNet datasets. The results show that MaxLin outperforms state-of-the-art tools with up to 110.60% improvement regarding the certified lower bound and 5.13 $\times$ speedup for the same neural networks. Our code is available at https://github.com/xiaoyuanpigo/maxlin.

Figures (6)

• Figure 1: A toy example of MaxLin linear approximation. To simplify, the input size is two, and the perturbation radius is one. $l^k_i(x^k_i)$ and $u_i^k(x^k_i)$ are the lower and upper linear bounds of the output of the $i$-th neuron($x^k_i$) in the $k$-th layer, respectively. $L^k_i(x_1,x_2)$ and $U_i^k(x_1,x_2)$ are the global lower and upper linear bounds of the output of the $i$-th neuron in the $k$-th layer, respectively. The blue surface is the output of the current neuron, and the activation function here is the Tanh function.
• Figure 2: A toy example of how MaxLin computing global bounds $\boldsymbol{l^K}$ and $\boldsymbol{u^K}$ against $l_\infty$ adversary. The first, second, third, and fourth hidden layers are the affine, ReLU, MaxPool, and affine functions, respectively.
• Figure 3: The average volume of the Activation+MaxPool block computed by CNN-Cert, DeepPoly, 3DCertify, Ti-Lin and MaxLin.
• Figure 4: Visualization of the output intervals verified by MaxLin and Ti-Lin. $(\boldsymbol{l},\boldsymbol{u})$ and $(\boldsymbol{l'},\boldsymbol{u'})$ represent the output bound of Ti-Lin and MaxLin testing on 100 inputs, respectively. Red and blue dots represent $\boldsymbol{u}-\boldsymbol{u'}$ and $\boldsymbol{l}-\boldsymbol{l'}$, respectively.
• Figure 5: Certified accuracy(%) and average per-example verification time(s) on CIFAR_Conv_MaxPool tested by MN-BaB, $\alpha$,$\beta$-CROWN, ERAN, and MaxLin(using single-neuron techniques for ReLU).

Theorems & Definitions (10)

• Definition 1: Local robustness bound
• Definition 2: Certified lower bound
• Definition 3: Upper/Lower linear bounds
• Theorem 1
• Definition 4: Block-wise Tightest
• Theorem 2
• proof
• Theorem 3
• proof
• proof