SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming

We want to thank reviewer zfFU for for your positive feedback and valuable comments. As suggested, we’ve added new experiments on GCP-CROWN [2] and BICCOS [3] (a follow-up work of GCP-CROWN), as well as a more sophisticated Lipschitz constant method (LipSDP [1]).

New experimental results

We provide additional comparisons with LipSDP [1], GCP-CROWN [2], and BICCOS [3] in the table below, using the same settings as Table 1 in our paper. We report the verified accuracy (%) and average per-sample verification time (in seconds), except for LipSDP, where we report the total time required to compute the Lipschitz constant.

Table A: Comparisons to new baselines

Since GCP-CROWN and BICCOS are all part of the $\alpha,\beta$-CROWN verifier, to avoid confusion, we renamed the original $\alpha,\beta$-CROWN baseline to $\beta$-CROWN (Wang et al., 2021). GCP-CROWN and BICCOS marginally improve over $\beta$-CROWN, although the gap to our method is still significant, especially on large models. LipSDP can outperform native Lipschitz but is still not competitive compared to our method, and computing the Lipschitz constant using SDP is also quite slow and not scalable.

[1] Fazlyab et al. "Efficient and accurate estimation of lipschitz constants for deep neural networks." NeurIPS 2019

[2] Zhang et al. "General cutting planes for bound-propagation-based neural network verification." NeurIPS 2020

[3] Zhou et al. "Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes." NeurIPS 2024

"Whether the chosen radius for L2-norm perturbation is reasonable"

While Table 1 only presents results for a single $\ell_2$ perturbation radius, we would like to highlight Figure 4 (c) (d) in Appendix (also linked here), which presents the certified lower bounds computed from different methods over a wide range of $\ell_2$ perturbation radii. As shown in Figure 4, our lower is consistently tighter than $\alpha$-CROWN and the naive Lipschitz approach across different perturbation radii, which demonstrates the effectiveness of our approach.

"More advanced methods beyond naive Lipschitz"

We agree that more advanced methods based on Lipschitz constant estimation can yield significantly tighter robustness bounds. To address this, we have added a comparison with LipSDP [1] in the Table A above, which employs SDP relaxation to estimate the network’s Lipschitz constant. This provides a stronger baseline for Lipschitz-based verification methods. Our method still significantly outperforms this baseline in all scenarios.

Response to Questions For Authors:

1. While our current work focuses on refining the bias term $h$, it is certainly possible to refine both the slope term $g$ and bias term $h$ simultaneously for tighter bounds. A key direction for future work is developing an efficient parameterization of $g$ that can be seamlessly integrated into existing bound propagation frameworks.

2. BM is an SDP-based method [4]. It exactly solves the SDP relaxation of the verification problem using specialized low-rank solvers. BM is one of the tightest SDP-based verifiers (as demonstrated in their paper) but is not scalable to CIFAR-10 models. We choose BM because it is a recently published SDP-based method with strong results.

3. We have added a comparison with GCP-CROWN [2] and BICCOS [3] above. The original GCP-CROWN implementation considers $\ell_\infty$ norm only, but we’ve able to extend the implementation to $\ell_2$ norm by finding cutting planes specifically for $\ell_2$ norm input constraints. It marginally improves performance and the gap between GCP-CROWN and our method is still large esepcially on bigger models.

4. We note that without $\mathrm{rank}(X_i)=1$, $X_i\succeq 0$ alone does not imply $u_iv_i = 0$, and the relaxation stems from dropping the constraint $\mathrm{rank}(X_i)=1$. Specifically, to derive SDP relaxation of ReLU activation: $x_i=u_i$, $u_iv_i=0$, $u_i\geq 0$, $v_i\geq 0$. We first add a redundant constraint $X_i=[1\ u_i\ v_i][1\ u_i\ v_i]^T\succeq 0$ and then set $U_i=u_i^2$, $V_i=v_i^2$, and $u_iv_i=0$ in $X_i$. It is clear that $X_i\succeq 0$ and $\mathrm{rank}(X_i)=1$ if and only if $u_iv_i=0$. Since $\mathrm{rank}(X_i)=1$ is nonconvex, we drop the rank-1 constraint to obtain the SDP relaxation: $x_i=u_i$, $u_i\geq 0$, $v_i\geq 0$, $X_i\succeq 0$.

[4] Chiu et al. "Tight certification of adversarially trained neural networks via nonconvex low-rank semidefinite relaxations." ICML 2023.

We thank you for the detailed review. We added additional experiments on GCP-CROWN and BICCOS, as well as LipSDP [5] (another SDP method) for all models as requested. We hope you can reevaluate our paper based on our response.

Clarifying Figure 1

We apologize for the confusion and will correct Figure 1. The model name should be ConvLarge, not ConvBig. ConvLarge is trained on CIFAR-10 and has 4 convolutional and 3 linear layers, totaling 24.6M parameters. The whiskers in Figure 1 illustrate the uncertainty gap where the true certified accuracy lies; blue numbers represent lower bounds on certified accuracy from different methods, and red numbers represent the PGD upper bound. A smaller gap indicates stronger verification.

Comparison to GCP-CROWN and BICCOS

During the rebuttal period, we implement $\ell_2$ norm support into GCP-CROWN and BICCOS. Particularly, the cutting planes found were using precise $\ell_2$ norm constraints rather than directly constructing an enclosing $\ell_\infty$ ball. This shows the best GCP-CROWN and BICCOS can do. We included comparisons to GCP-CROWN and BICCOS on all benchmarks in Table A below.

Table A: Comparisons to new baselines

Since GCP-CROWN and BICCOS are all part of the $\alpha,\beta$-CROWN verifier, to avoid confusion, we renamed the original $\alpha,\beta$-CROWN baseline to $\beta$-CROWN (Wang et al., 2021). GCP-CROWN and BICCOS marginally improve over $\beta$-CROWN, although the gap to our method is still large especially on bigger models.

Explain BM method

BM is an SDP-based method [6]. It exactly solves the SDP relaxation of the verification problem using specialized low-rank solvers. BM is one of the tightest SDP-based verifiers (as demonstrated in their paper) but is not scalable to CIFAR-10 models. We choose BM because it is a recently published SDP-based method with strong results. BM is tighter than our method because our approach remains LP-based as the SDP relaxation is only used to refine the offset of linear bounds. However, our method is orders of magnitude more scalable; our ConvLarge is a factor of 100x larger than the models considered in BM. Our comparisons with BM demonstrate that the substantial improvement in scalability achieved by our method comes with only a mild loss of tightness.

Comparison to SDP-based methods

Besides the BM SDP-based method already reported in our paper, we conduct additional experiments on LipSDP [5] in Table A.

Table A: Comparisons to new baselines

For a fair comparison, we run LipSDP with multiple configurations by splitting original networks into subnetworks. We show the results in Table A. The verified accuracy by LipSDP is significantly lower than ours, even in the tightest (slowest) setting with no split.

We also considered additional SDP baselines that can scale to the networks we evaluated, such as SDP-FO (Dathathri et al., 2020). However, we found that their algorithm and implementation support $\ell_\infty$ norm only, and it is not straightforward to adapt their implementation to our setting.

Add new references

Thank you for bringing these references to our attention. We will incorporate these works into the final version to provide a more comprehensive discussion of related research. We’ve added an experimental comparison to GCP-CROWN [1], BICCOS [2], Lip-SDP [5] above, and [6] is the BM in our paper. We will cite and discuss [3] (a survey paper) and [4] (focusing on training certifiable networks with special architectures).

Response to Questions For Authors:

1. Given $c^T\textrm{ReLU}(x)\geq g^Tx+h$ that holds within $\Vert x-\hat x\Vert_\infty \leq \rho$. Observe that from bound propagation $g_i=c_i$ if $\hat x_i>\rho$, and $g_i=0$ if $\hat x_i<\rho$. Hence, $c_i\textrm{ReLU}(x_i)-g_ix_i=0$ if $|\hat x_i|>\rho$. Therefore $x_i^\star=\hat x_i$ is a minimizer of $\min_x c^T\textrm{ReLU}(x)-g^Tx\text{ s.t. } \Vert x-\hat x\Vert_2 \leq \rho$ if $|\hat x_i|>\rho$, and $x_i$ can be removed by substituting $x_i=\hat x_i$. It follows from positive/negative splitting $x_i^\star=u_i^\star - v_i^\star$ that $u_i^\star=\max\lbrace\hat x_i,0\rbrace$ and $v_i^\star=\min\lbrace\hat x_i,0\rbrace$.

2 & 3. See our comparison to GCP-CROWN, BICCOS, LipSDP and BM above.

4. Our method is a hybrid framework that tightens bound propagation using SDP relaxations specifically for ReLU activations. Our approach is complementary to existing work on leveraging specialized architectures, offering an alternative route to achieve certified robustness. We will add a paragraph to discuss methods that leverage specialized architectures, such as [4], Cayley layers, AOL, SLL, etc. While a direct comparison is not feasible due to the different aims of these approaches, we will explore the design of verification-friendly architectures that can utilize the strengths of both bound propagation and specialized architectures in future work.

We want to thank reviewer 4cg2 for valuable comments and for recognizing the key contributions of our paper. We hope our response would adequately address your questions and concerns.

"They claim that their bounds can be up to $\sqrt{n}$ better compared to standard single-neuron bounds. While this is clear for the input - for the output this can be larger or smaller i would assume. (imprecisions can accumulate) "

The input bound improvement by a factor of $\sqrt{n}$ follows directly from the fact that the volume of an $\ell_2$ ball is smaller than that of an $\ell_\infty$ box by this factor.

Regarding the output bound, we prove that our method can achieve up to a $\sqrt{n}$ improvement vs traditional bound propagation (Theorem 5.2). However, this proof applies specifically to as simple network $\mathrm{ReLU(x)}$ under $\ell_2$ perturbations of the form $\Vert x\Vert_2\leq\rho$.

For general multi-layer neural networks, the extent of improvement is hard to quantify theoretically. To address this, we provide empirical results demonstrating that our method consistently outperforms bound propagation methods, especially on large neworks.

"The experimental design is standard. That said, I would be curious how far one could push the method. "

Thank you for your insightful comment. In this paper, we utilize SDP to tighten the offset of the linear bounds in bound propagation. Our method has been integrated into $\alpha$-CROWN with minimal overhead, as it only introduces one additional variable $\lambda$ per postactivation neuron.

Our next step is to integrate our method into the $\alpha,\beta$-CROWN codebase, hence allowing our method to work with powerful branch-and-bound based methods and a wide range of neural network architecture. Our current algorithm already outperformed the existing branch-and-bound based approaches (including GCP-CROWN, BICCOS and beta-CROWN, as presented in the new table we added during rebuttal), and additional improvements can be further demonstrated once we finish this integration. Additionally, we aim to extend our approach to jointly optimize both the slope and offset terms, with the goal of developing optimal linear relaxations for $\ell_2$ perturbations. We expect these two future directions to yield tighter results on an even larger scale than considered in the present paper.

"Most related work I know of is adequately discussed. What I find curious about the work here is that the offset adjustment here is exactly the opposite of what is done in [A] and [B], where unsound bounds are adjusted to be sound. Here, sound bounds are adjusted to be more tight but still sound."

We appreciate the reviewer for bringing these references to our attention. We will include a discussion of these works in the final version of our paper.

[A] presents a method for certifying robustness against geometric transformations. This approach begins with potentially unsound bounds and subsequently adjusts them to be sound through a combination of sampling and optimization techniques. In contrast, our method operates in the opposite manner; we start with sound bounds and refine them to be tighter while ensuring they remain valid. Regarding [B], we believe this reference may have been included by mistake, as it presents a framework for robotic tissue manipulation using deep learning for feature extraction, which does not appear relevant to the context of our work. We will be happy to discuss any additional works you suggest.

"I have the feeling that the limits regarding the most optimal linear bounds (Salman et al 2019) regarding the expressivity also apply here. Specifically, just restricting $\ell_2$ to $\ell_\infty$ and adjustment of the offset do not address fundamental expressivity shortcomings."

Our critical contribution is to introduce multi-neuron SDP relaxations into bound propagation. This allowed us to overcome the “convex relaxation barrier” faced by traditional single-neuron LP relaxations underlying the vast majority of prior work. It also improved upon prior work on multi-neuron relaxations, which were either too loose (i.e. LP-based) or limited to tiny models (i.e. SDP-based). Addressing $\ell_2$-norm constraints is a crucial first step, but we anticipate further work to greatly expand the applicability of models and new threat models (beyond $\ell_p$ norm) using our key idea of combining SDP with bound propagation. We will also cite the paper on the Expressivity of ReLU networks in our final version.