Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone

Yuan Xiao, Yuchen Chen, Shiqing Ma, Chunrong Fang, Tongtong Bai, Mingzheng Gu, Yuxin Cheng, Yanwei Chen, Zhenyu Chen

TL;DR

This work tackles the challenge of robustness verification for MaxPool-based CNNs by introducing Ti-Lin, a verifier that uses neuron-wise tightest linear bounds for MaxPool. By analytically deriving the tightest upper and lower linear bounds for MaxPool with input bounds, Ti-Lin minimizes the over-approximation zone and can be integrated into existing verifiers (CNN-Cert, DeepPoly, ERAN, and $\alpha,\beta$-CROWN). Across MNIST, CIFAR-10, Tiny ImageNet, and ModelNet40 benchmarks, Ti-Lin achieves substantial gains in certified accuracy—up to $78.6\%$—while maintaining comparable runtime to the fastest baselines. The results demonstrate that replacing MaxPool bounds with neuron-wise tightest linear bounds significantly tightens robustness estimates, and that the MaxPool->ReLU transforms can degrade performance, underscoring the value of direct MaxPool linearization in practice.

Abstract

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.

Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone

TL;DR

This work tackles the challenge of robustness verification for MaxPool-based CNNs by introducing Ti-Lin, a verifier that uses neuron-wise tightest linear bounds for MaxPool. By analytically deriving the tightest upper and lower linear bounds for MaxPool with input bounds, Ti-Lin minimizes the over-approximation zone and can be integrated into existing verifiers (CNN-Cert, DeepPoly, ERAN, and -CROWN). Across MNIST, CIFAR-10, Tiny ImageNet, and ModelNet40 benchmarks, Ti-Lin achieves substantial gains in certified accuracy—up to —while maintaining comparable runtime to the fastest baselines. The results demonstrate that replacing MaxPool bounds with neuron-wise tightest linear bounds significantly tightens robustness estimates, and that the MaxPool->ReLU transforms can degrade performance, underscoring the value of direct MaxPool linearization in practice.

Abstract

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.
Paper Structure (31 sections, 3 theorems, 25 equations, 6 figures, 7 tables)

This paper contains 31 sections, 3 theorems, 25 equations, 6 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Adversarial attacks and defenses
  4. Robustness verification for MaxPool-based neural networks
  5. Preliminaries
  6. Certified robustness bound
  7. Linear approximation
  8. Computing certified results
  9. Certified accuracy
  10. Certified robustness bounds
  11. Ti-Lin: A robustness verifier for MaxPool-based networks
  12. Tight linear approximation for MaxPool
  13. Neuron-wise tightest property
  14. Experimental evaluation
  15. Experimental setup
  16. ...and 16 more sections

Key Result

Theorem 1

Given $f(x_1,\cdots,x_n)=max\{x_1,\cdots,x_n\}, x_i\in[l_i,u_i]$, we first select the first, second, and third largest elements of $\{u_i|i=1,\cdots,n\}$, whose indexes are denoted as $i,j,k$, respectively. We then choose the largest element of $\{l_i|i=1,\cdots,n\}$ and denote it as $l_{max}$. Defi

Figures (6)

  • Figure 1: An illustration for the neuron-wise tightest linear bounds for bivariate MaxPool function. From left to right, the subfigures are the MaxPool function, upper linear bound plane $u(x_1,x_2)$, and lower linear bound plane $l(x_1,x_2)$, respectively. The red dots are $u(l_1,u_2), u(u_1,l_2), u(m_1,m_2),$and $l(m_1,m_2)$, where $m_i=\frac{1}{2}(l_i+u_i), i=1,2$. $\mathcal{L}$ and $\mathcal{U}$ are the sets of all lower and upper linear bounds for MaxPool, respectively.
  • Figure 2: Toy examples of the neuron-wise tightest linear bounds for the four cases in Theorem \ref{['theoremMaxPool']}.
  • Figure 3: Visualization of the global lower bounds verified by DeepPoly, 3DCertify, $\alpha,\beta$-CROWN, and Ti-Lin. Red dots represent the deviation of the global bounds $\boldsymbol{L}-\boldsymbol{L'}$, where $\boldsymbol{L}$ and $\boldsymbol{L'}$ represent the global bounds of Ti-Lin and other methods testing on 100 inputs, respectively. Black lines represent the mean of the deviations.
  • Figure 4: Visualization of the global lower bound verified by MaxLin and Ti-Lin, both of which are built upon the framework of $\alpha,\beta$-CROWN.
  • Figure 5: The deviation in global bounds between MaxLin and Ti-Lin when using the CROWN and $\alpha$-CROWN frameworks.
  • ...and 1 more figures

Theorems & Definitions (10)

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