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

Hao Chen; Hong-Ming Chiu; Huan Zhang; Richard Y. Zhang

REVIEW 2 major objections 3 minor 1 cited by

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

T0 review · 2 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper proposes SDP-CROWN, a verifier whose per-layer linear bound, derived from an SDP relaxation of the ReLU constraint with one scalar parameter per layer, captures $\ell_2$ inter-neuron coupling and is proved up to $\sqrt{n}$…

desk verdict The single-layer bound is a genuine contribution, but the multi-layer integration has an unsound L2-ball containment step that invalidates the headline empirical results. read the letter →

arxiv 2506.06665 v1 pith:6HE77SWK submitted 2025-06-07 cs.LG

Hong-Ming Chiu , Hao Chen , Huan Zhang , Richard Y. Zhang This is my paper

classification cs.LG MSC 68T0790C2268Q60

keywords neuralnetworkverificationsemidefiniteprogrammingrelaxationlinearboundpropagationl2adversarialrobustnessReLUnetworksLipschitzboundscertifiedLiRPA

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Linear bound propagation scales to huge networks but goes loose under $\ell_2$-norm adversaries, because it encloses the $\ell_2$ ball in an $\ell_\infty$ box and thereby inflates the effective attack radius by up to $\sqrt{n}$. SDP-CROWN replaces that step with a linear lower bound built directly on the $\ell_2$ ball: a per-layer offset derived from an SDP relaxation of the ReLU constraint, with only one new scalar parameter $\lambda$ per layer. The construction dualizes the SDP to a closed form and can be inserted into any linear bound-propagation verifier; inside $\alpha$-CROWN it reports verified accuracy close to expensive SDP methods on models up to 65,546 neurons. The paper proves that on a centered single-ReLU layer the relaxation is exactly tight and up to $\sqrt{n}$ tighter than per-neuron box bounds, and empirically demonstrates the gain persists in deep convolutional networks.

What carries the argument

The central object is the SDP-derived linear offset $h(g,\lambda)$ of Theorem 4.1, which encodes inter-neuron coupling through one scalar $\lambda$ per layer instead of the $n^2$ matrix of a full SDP relaxation. It is constructed by splitting each ReLU preactivation into positive and negative parts $x=u-v$ with $u\odot v=0$, lifting the constraint to the semidefinite condition $[1\ u_i\ v_i;\ u_i\ U_i\ 0;\ v_i\ 0\ V_i] \succeq 0$, passing to the Lagrangian dual, and simplifying the $2\times 2$ PSD constraints into a closed-form expression. This offset is what lets a standard LiRPA-style backward pass replace its box-based per-neuron terms with an $\ell_2$-aware term while keeping the pipeline linear and scalable.

What would settle it

Take $f(x)=\mathrm{ReLU}(\mathrm{ReLU}(x))$ with identity weights and input ball centered at $-10$ with radius $1$; the true second-layer preactivation is identically $0$, but the method's propagated ball is centered at $-10$ with radius $1$ and excludes $0$, so the per-layer offset in Appendix B.2 cannot be applied there. A direct test is to compute SDP-CROWN's certified margin on such saturated-ReLU networks and compare it with the true minimum obtained by exhaustive search, since any certified margin larger than the true minimum would falsify the claim that the bounds are valid for all $\ell_2$ perturbations.

Watch

Extended reading notes

Core claim

SDP-CROWN starts from the observation that bound propagation under an $\ell_2$ adversary becomes loose when it first encloses the $\ell_2$ ball in an $\ell_\infty$ box. The paper constructs a linear lower bound directly on the $\ell_2$ ball: for $f(x)=\mathrm{ReLU}(x)$, Theorem 4.1 gives $c^T \mathrm{ReLU}(x) \ge g^T x + h(g,\lambda)$ for all $x \in B_2(\hat{x},\rho)$, where $h(g,\lambda) = -\tfrac{1}{2}(\lambda(\rho^2 - \|\hat{x}\|_2^2) + \tfrac{1}{\lambda}\|\varphi(g,\lambda)\|_2^2)$ and $\varphi_i(g,\lambda)=\min\{c_i-g_i-\lambda\hat{x}_i,\, g_i+\lambda\hat{x}_i,\, 0\}$. The bound is derived by relaxing the nonconvex ReLU identity through a semidefinite constraint, taking the SDP dual, and solving the resulting $2\times 2$ PSD blocks in closed form. Setting $\hat{x}=0$, the paper proves the relaxation is exactly tight and that its offset is $-\rho\|\min\{c-g,g,0\}\|_2$ rather than the box-bound offset $-\rho\|\min\{g,0\}\|_1$, giving a factor up to $\sqrt{n}$ of tightening. Integrated into $\alpha$-CROWN, the method reports verified accuracies near SDP baselines on models with up to 65,546 neurons, e.g. 63.5% on the CIFAR-10 ConvLarge network versus 47.5% for LipNaive and 2.5% for $\alpha$-CROWN.

Load-bearing premise

The method assumes that at every layer the set of possible preactivations, given inputs in the $\ell_2$ ball, is contained in the $\ell_2$ ball centered at the value of the linear (non-ReLU) network with radius equal to the product of the layer spectral norms, and ReLU layers can break this containment.

Editorial extensions

If this is right

If the method is sound at every layer, every CROWN-family verifier can be upgraded to an $\ell_2$-aware verifier by adding one $\lambda$ per layer, with no dense coupling matrix and no cubic SDP solve.
For zero-centered $\ell_2$ balls on a single ReLU layer, the SDP-CROWN linear relaxation coincides with the optimal convex lower bound, so the reported $\sqrt{n}$ improvement over per-neuron triangle relaxation is not an artifact of a weak baseline.
On the 65,546-neuron CIFAR-10 ConvLarge network, SDP-CROWN certifies 63.5% of test images, compared with 2.5% for $\alpha$-CROWN, 5.0% for $\beta$-CROWN, 47.5% for LipNaive, and similarly low or costly values for other baselines, at 73 seconds per image.
The offset $h(g,\lambda)$ preserves its strength as the perturbation radius grows, whereas the box offset collapses, as shown by the average-offset curves in Figure 4.
The ellipsoid extension and the ellipsoid-intersect-box extension in Appendix C keep the one-parameter-per-layer structure while tightening the propagated input set, so the method is not tied to axis-aligned or spherical geometries.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

[Editorial inference] Because the core offset is a closed-form scalar function of $g$ and $\lambda$, it could double as a differentiable certified-training regularizer that penalizes the $\ell_2$ certified margin at training time without solving an SDP each step.
[Editorial inference] Combining SDP-CROWN as a node bound with branch-and-bound over unstable ReLUs may close most of the remaining gap to the PGD upper bound, a complete-verification direction the paper does not pursue.
[Editorial inference] The $\sqrt{n}$ tightening factor suggests the advantage should grow with layer width; this is testable by comparing SDP-CROWN against LipNaive on a family of networks whose width doubles, expecting a widening verified-accuracy gap.
[Editorial inference] The method's soundness depends on each layer's spectral-norm $\ell_2$ ball containing the true reachable preactivation set, and networks with many saturated ReLUs may violate this, so a practical fix is to recenter each layer's ball using the actual worst-case preactivation rather than the ReLU-free center.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: the paper has a real, clean idea—a closed-form per-layer linear bound for ReLU over an L2 ball, derived from the SDP dual, with a nice sqrt(n) tightness proof for the zero-centered single-layer case. Theorems 4.1, 5.2, and 5.3 are correct and are the strongest part of the paper. The exposition is clear, and the authors are honest about the limits of their analysis for general centers.

The problem is the multi-layer integration in Appendix B.2. The method requires an L2 ball around each preactivation, and the paper takes the center as the linear propagation zhat^(k)=W^(k)...W^(1)xhat and the radius as the product of spectral norms times rho. For k=1 this containment is true. For k>=2 it is false: ReLU shifts the reachable preactivations away from the linear center. The paper asserts (14) follows from Theorem 4.1 without proving the containment, and it isn't true.

The stress-test note's scalar example doesn't quite work out numerically—the propagated bound in that example is actually negative, not 9—but the structural concern is exactly right. Here is a cleaner counterexample. Take W1=I (2x2), W2=[1,1], W3=1, c=1, xhat=(-10,-10), rho=1. For every x in the L2 ball, z1 is coordinatewise <= -9, so ReLU(z1)=0 and z2=0; the true minimum of c^T f(x) is 0. SDP-CROWN, however, takes zhat2=W2 W1 xhat = -20, rho2=sqrt(2). At layer 2, the interval bound for z2 is [0,0], so the LiRPA slope g2=1. Optimizing the new offset over that wrong ball gives h2 ~ 18.6. Propagating to layer 1 yields a final certified lower bound of about 18.6, which exceeds the true minimum 0. So the algorithm is unsound as written.

This is a load-bearing flaw, not a minor gap. The single-layer theory survives, but the headline claims—Table 1, the verified accuracies, the "tightness approaching SDP" narrative—rest on the invalid multi-layer step. The paper should not be accepted in its current form.

Who is this for? Researchers in L2 verification will want to know about the single-layer bound; it could be the basis for a sound method if the propagation of L2 balls is redone, e.g., with forward-propagated centers or a more careful outer approximation. A serious referee should see it, and I'd bring it to a reading group as a cautionary example of an easy-to-miss containment failure.

Recommendation: reject for now, but let the authors revise with a correct multi-layer propagation and rerun the experiments.

Referee Report

2 major / 3 minor

Summary. The paper proposes SDP-CROWN, a hybrid verification method that aims to combine the tightness of semidefinite programming (SDP) relaxations with the scalability of linear bound propagation for certifying neural networks against L2-norm perturbations. The core idea is to replace the usual per-neuron linear relaxation offsets with a new offset derived from an SDP dual, which introduces one extra parameter per layer. The authors prove the new offset is valid and optimal for a single ReLU layer, show a sqrt(n) improvement over standard bound propagation in that setting, and report large empirical gains on models with up to 65k neurons.

Significance. If the method were sound, it would be a significant advance: it would provide SDP-like tightness in a bound-propagation framework that scales to much larger networks than traditional SDP solvers, with a provable sqrt(n) improvement for the single-layer case, and a public code repository. The single-layer theoretical derivations (Theorems 4.1, 5.2, 5.3) are internally consistent and appear correct. However, the multi-layer integration is invalid: the L2 ball used at each layer does not contain the actual reachable preactivations after ReLU clipping. This is a load-bearing error that undermines the core claim of sound verification, so the reported verified accuracies in Table 1 and the tightness comparisons are not supported.

major comments (2)

[Appendix B.2, Eq. (14)]
[Appendix B.2, construction of zhat^(k) and rho^(k)] Even if one replaced the linear center with the true forward center z^(k)(xhat), the paper would need to prove that the resulting ball contains the reachable set; simply asserting the linear form is not enough. The counterexample above shows the current construction fails, and the paper provides no alternative proof of containment for nonlinearly activated layers. This is not a minor gap in presentation but a fundamental correctness issue in the multi-layer composition that the paper claims to have solved.

minor comments (3)

[Eq. (1)] The recursion defines x^(0)=x, but the displayed line reads "x(0) = x(1)", which appears to be a typographical error that should be corrected to "x(0) = x".
[Section 3, last paragraph] The notation "B∞(xhat, 1ρ)" is confusing; it should be written as B∞(xhat, ρ·1) or explicitly state that 1 denotes the all-ones vector.
[Figure 4 caption] The caption "We compare the offset h(α) from α-CROWN to the offset h(g(α), λ) from SDP-CROWN" is grammatically awkward; consider rewording to "We compare the offset h(α) from α-CROWN with the offset h(g(α), λ) from SDP-CROWN".

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: SDP-CROWN's bound comes from an explicit Lagrangian dual, not from fitting; the Appendix B.2 containment gap is a soundness issue, not circularity.

full rationale

SDP-CROWN's central offset h(g, lambda) is not fitted or assumed equal to the target; it is produced by writing the tightest affine under-approximation problem (7), relaxing it to an SDP, deriving the Lagrangian dual (8), and optimizing over the dual variable mu in closed form. This is a standard weak-duality argument, so h(g, lambda) is a valid lower bound by derivation rather than by circular definition. Theorems 5.2 and 5.3 independently prove exactness for the single-ReLU, zero-center case, and the multi-layer extension in Appendix B.2 reuses Theorem 4.1 layer by layer rather than assuming its conclusion. No experimental parameter is calibrated to the reported verified accuracies; alpha and lambda are optimization variables inside a convex relaxation, and the method is evaluated against external baselines and benchmarks. The self-citations to Chiu & Zhang (2023) appear only as related-work context and as the BM-Full baseline; they are not load-bearing for the derivation. The real weakness is the unsupported containment claim in Appendix B.2: zhat(k) is taken as the linear image W(k)...W(1)xhat, but after ReLU the reachable set is centered at W(k)ReLU(...W(1)xhat), so the asserted inclusion is false in general and the propagated bound may be invalid. That is a soundness/correctness gap, not a circularity, and therefore does not raise the circularity score. Score 1 reflects only the presence of minor background self-citations.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters are fitted to data: lambda is an optimization variable in the bound, not a constant fit to the benchmark. The central derivation relies on standard SDP duality and chordal decomposition. The critical non-standard assumption is that the reachable preactivation set at each layer is contained in the L2 ball centered at the linear-propagated value; this is the load-bearing and false premise.

assumptions (3)

domain assumption The reachable preactivation set {z(k)(x): x in B2(xhat, rho)} is contained in B2(W(k)...W(1)xhat, ||W(k)||_2 ... ||W(1)||_2 rho)
Appendix B.2. False when ReLU clipping shifts the true forward center from the linear center; a scalar example with negative inputs shows the ball misses the reachable value 0.
standard math Standard SDP relaxation of ReLU and chordal decomposition (Theorem 9.2 of Vandenberghe & Andersen 2015)
Used to derive the dual problem (8) in Section 4.1 and Appendix D.
standard math ReLU is 1-Lipschitz and layer Lipschitz constants multiply as spectral norms
Used to compute the radius rho(k) in Appendix B.2; standard, but requires the center to be the actual forward output.

how reviews work

0 comments

Cite this review

Pith. "Pith review of SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming." pith.science (2026). https://pith.science/paper/6HE77SWK

@misc{pith2026250606665,
  author       = {Pith},
  title        = {Pith review of: SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6HE77SWK}},
  note         = {Machine review of arXiv:2506.06665}
}

abstract

Neural network verifiers based on linear bound propagation scale impressively to massive models but can be surprisingly loose when neuron coupling is crucial. Conversely, semidefinite programming (SDP) verifiers capture inter-neuron coupling naturally, but their cubic complexity restricts them to only small models. In this paper, we propose SDP-CROWN, a novel hybrid verification framework that combines the tightness of SDP relaxations with the scalability of bound-propagation verifiers. At the core of SDP-CROWN is a new linear bound, derived via SDP principles, that explicitly captures $\ell_{2}$-norm-based inter-neuron coupling while adding only one extra parameter per layer. This bound can be integrated seamlessly into any linear bound-propagation pipeline, preserving the inherent scalability of such methods yet significantly improving tightness. In theory, we prove that our inter-neuron bound can be up to a factor of $\sqrt{n}$ tighter than traditional per-neuron bounds. In practice, when incorporated into the state-of-the-art $\alpha$-CROWN verifier, we observe markedly improved verification performance on large models with up to 65 thousand neurons and 2.47 million parameters, achieving tightness that approaches that of costly SDP-based methods.

Figures

Figures reproduced from arXiv: 2506.06665 by the authors.

**Figure 1.** Verification of the ConvLarge network on the CIFAR-10 dataset (six convolutional layers + three fully connected layers, ≈2.47M parameters and 65k neurons) under ℓ2 adversaries. State-of-the-art bound propagation algorithms α-CROWN, β-CROWN and BICCOS yield surprisingly loose relaxations under ℓ2 adversaries (verified accuracy 2.5%, 5.0% and 6.0%, respectively) at high cost (up to 289s per example). A naive Lipschi… view at source ↗

**Figure 2.** Comparing linear relaxations within ℓ2-norm ball from our method and bound propagation. Consider a task of finding a linear relaxation of f(x) = − ReLU(x1) − ReLU(x2) on B2(0, 1). (Left.) Bound propagation finds the tightest possible linear relaxation on B∞(0, 1), however, such relaxation is not the tightest on B2(0, 1). (Right.) Our method finds the tightest possible linear relaxation on B2(0, 1), which is tighter … view at source ↗

**Figure 3.** Lower bounds on the robustness margin under ℓ2-norm perturbations. We compare the lower bounds on (2) computed from SDP-CROWN, α-CROWN, LipNaive and LP-All. The lower bounds are averages over 90 instances of (2). The upper bound on (2) is estimated projected gradient descent (PGD). The numbers in the figure indicate the ℓ2-norm perturbation level at which each lower bound crosses zero. Note that robustness verificat… view at source ↗

Figures from the paper (4 more)

**Figure 4.** Figure 4: Linear relaxation offsets under ℓ2-norm perturbations. We compare the offset h(α) from α-CROWN to the offset h(g(α), λ) from SDP-CROWN. The offsets are averages over 90 instances of (2). (Red line.) Smallscale model MLP (MNIST). (Green line.) Medium-scale model ConvS…

**Figure 5.** Figure 5: Illustration of the linear relaxation (11). (Left.) z˜ (k) i − ρ˜ (k) i ≥ 0. In this case, ReLU(z (k) i (x)) is simply upper and lower bounded by z (k) i (x). (Middle.) z˜ (k) i + ˜ρ (k) i ≤ 0. In this case, ReLU(z (k) i (x)) is simply upper and lower bounded by 0. (Ri…

**Figure 6.** Figure 6: Constructing the ℓ2-norm ball and the ellipsoid relaxation at z (1) for a one layer neural network with W(1) = [0.5, 0.5; 1.5, −0.5], xˆ = [0; 0] and ρ = 1. (Left.) The input set at z (1) with respect to the ℓ2-norm ball input set B2(ˆx, ρ) at x. The input set at z (1)…

**Figure 7.** Figure 7: Constructing the intersection between ellipsoid and elementwise bound as a relaxation at [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Learning to Optimize by Differentiable Programming
cs.MS 2026-01 unverdicted novelty 2.0 of 10

A tutorial survey of differentiable-programming-based first-order optimization, with dual-based PyTorch case studies and no new results.

Reference graph

Works this paper leans on

45 extracted references · 41 canonical work pages · cited by 1 Pith paper

[1]

Towards Optimal Branching of Linear and Semidefinite Relaxations for Neural Network Robustness Certification

Anderson, B. G., Ma, Z., Li, J., and Sojoudi, S. Partition-based convex relaxations for certifying the robustness of relu neural networks. arXiv preprint arXiv:2101.09306, 2021

work page Pith review arXiv 2021
[2]

J., Delattre, B., Allauzen, A., and Hu, B

Araujo, A., Havens, A. J., Delattre, B., Allauzen, A., and Hu, B. A unified algebraic perspective on lipschitz neural networks. In ICLR, 2023

work page 2023
[3]

Certifiably robust variational autoencoders

Barrett, B., Camuto, A., Willetts, M., and Rainforth, T. Certifiably robust variational autoencoders. In International Conference on Artificial Intelligence and Statistics, pp.\ 3663--3683. PMLR, 2022

work page 2022
[4]

Efficient neural network verification via layer-based semidefinite relaxations and linear cuts

Batten, B., Kouvaros, P., Lomuscio, A., and Zheng, Y. Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In IJCAI, pp.\ 2184--2190, 2021

work page 2021
[5]

N., Bak, S., Johnson, T

Brix, C., M \"u ller, M. N., Bak, S., Johnson, T. T., and Liu, C. First three years of the international verification of neural networks competition (vnn-comp). International Journal on Software Tools for Technology Transfer, 25 0 (3): 0 329--339, 2023

work page 2023
[6]

T., and Wu, H

Brix, C., Bak, S., Johnson, T. T., and Wu, H. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412.19985, 2024

arXiv 2024
[7]

A., Schmerling, E., Azizan, N., and Pavone, M

Brown, R. A., Schmerling, E., Azizan, N., and Pavone, M. A unified view of sdp-based neural network verification through completely positive programming. In International conference on artificial intelligence and statistics, pp.\ 9334--9355. PMLR, 2022

work page 2022
[8]

and Zhang, R

Chiu, H.-M. and Zhang, R. Y. Tight certification of adversarially trained neural networks via nonconvex low-rank semidefinite relaxations. In International Conference on Machine Learning, pp.\ 5631--5660. PMLR, 2023

work page 2023

Show all 45 references

[9]

Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming

Dathathri, S., Dvijotham, K., Kurakin, A., Raghunathan, A., Uesato, J., Bunel, R., Shankar, S., Steinhardt, J., Goodfellow, I., Liang, P., et al. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. In Advances in Neural Infor...

2020
[10]

S., Bunel, R., Torr, P., and Kumar, M

De Palma, A., Behl, H. S., Bunel, R., Torr, P., and Kumar, M. P. Scaling the convex barrier with active sets. In Proceedings of the ICLR 2021 Conference. Open Review, 2021

2021
[11]

A., and Kohli, P

Dvijotham, K., Stanforth, R., Gowal, S., Mann, T. A., and Kohli, P. A dual approach to scalable verification of deep networks. In UAI, volume 1, pp.\ 2, 2018

2018
[12]

Efficient and accurate estimation of lipschitz constants for deep neural networks

Fazlyab, M., Robey, A., Hassani, H., Morari, M., and Pappas, G. Efficient and accurate estimation of lipschitz constants for deep neural networks. Advances in neural information processing systems, 32, 2019

2019
[13]

Fazlyab, M., Morari, M., and Pappas, G. J. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control, 67 0 (1): 0 1--15, 2020

2020
[14]

N., Jovanovi \'c , N., and Vechev, M

Ferrari, C., Mueller, M. N., Jovanovi \'c , N., and Vechev, M. Complete verification via multi-neuron relaxation guided branch-and-bound. In International Conference on Learning Representations, 2022

2022
[15]

Gouk, H., Frank, E., Pfahringer, B., and Cree, M. J. Regularisation of neural networks by enforcing lipschitz continuity. Machine Learning, 110: 0 393--416, 2021

2021
[16]

D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., and Kohli, P

Gowal, S., Dvijotham, K. D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., and Kohli, P. Scalable verified training for provably robust image classification. In Proceedings of the IEEE/CVF International Conference on Computer Vision, pp.\ 4842--4851, 2019

2019
[17]

Osip: Tightened bound propagation for the verification of relu neural networks

Hashemi, V., Kouvaros, P., and Lomuscio, A. Osip: Tightened bound propagation for the verification of relu neural networks. In International Conference on Software Engineering and Formal Methods, pp.\ 463--480. Springer, 2021

2021
[18]

Unlocking deterministic robustness certification on imagenet

Hu, K., Zou, A., Wang, Z., Leino, K., and Fredrikson, M. Unlocking deterministic robustness certification on imagenet. Advances in Neural Information Processing Systems, 36: 0 42993--43011, 2023

2023
[19]

Z., and Anandkumar, A

Huang, Y., Zhang, H., Shi, Y., Kolter, J. Z., and Anandkumar, A. Training certifiably robust neural networks with efficient local lipschitz bounds. Advances in Neural Information Processing Systems, 34: 0 22745--22757, 2021

2021
[20]

Globally-robust neural networks

Leino, K., Wang, Z., and Fredrikson, M. Globally-robust neural networks. In International Conference on Machine Learning (ICML), 2021

2021
[21]

B., and Jacobsen, J.-H

Li, Q., Haque, S., Anil, C., Lucas, J., Grosse, R. B., and Jacobsen, J.-H. Preventing gradient attenuation in lipschitz constrained convolutional networks. Advances in neural information processing systems, 32, 2019

2019
[22]

and Sojoudi, S

Ma, Z. and Sojoudi, S. Strengthened sdp verification of neural network robustness via non-convex cuts. arXiv preprint arXiv:2010.08603, pp.\ 715--727, 2020

2010 arXiv
[23]

Towards deep learning models resistant to adversarial attacks

Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations, 2018

2018
[24]

J., Araujo, A., and Allauzen, A

Meunier, L., Delattre, B. J., Araujo, A., and Allauzen, A. A dynamical system perspective for lipschitz neural networks. In International Conference on Machine Learning, pp.\ 15484--15500. PMLR, 2022

2022
[25]

and Papachristodoulou, A

Newton, M. and Papachristodoulou, A. Exploiting sparsity for neural network verification. In Learning for dynamics and control, pp.\ 715--727. PMLR, 2021

2021
[26]

Raghunathan, A., Steinhardt, J., and Liang, P. S. Semidefinite relaxations for certifying robustness to adversarial examples. Advances in Neural Information Processing Systems, 31, 2018

2018
[27]

A convex relaxation barrier to tight robustness verification of neural networks

Salman, H., Yang, G., Zhang, H., Hsieh, C.-J., and Zhang, P. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems, 32, 2019

2019
[28]

Neural network verification with branch-and-bound for general nonlinearities

Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C.-J., and Zhang, H. Neural network verification with branch-and-bound for general nonlinearities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2025

2025
[29]

Fast and effective robustness certification

Singh, G., Gehr, T., Mirman, M., P \"u schel, M., and Vechev, M. Fast and effective robustness certification. In Advances in Neural Information Processing Systems, pp.\ 10802--10813, 2018

2018
[30]

An abstract domain for certifying neural networks

Singh, G., Gehr, T., P \"u schel, M., and Vechev, M. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3 0 (POPL): 0 1--30, 2019

2019
[31]

and Feizi, S

Singla, S. and Feizi, S. Improved deterministic l2 robustness on cifar-10 and cifar-100. In International Conference on Learning Representations (ICLR), 2022

2022
[32]

Intriguing properties of neural networks

Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., and Fergus, R. Intriguing properties of neural networks. In International Conference on Learning Representations, 2014

2014
[33]

and Kolter, J

Trockman, A. and Kolter, J. Z. Orthogonalizing convolutional layers with the cayley transform. In International Conference on Learning Representations, 2021

2021
[34]

and Andersen, M

Vandenberghe, L. and Andersen, M. S. Chordal graphs and semidefinite optimization. Foundations and Trends in Optimization, 1 0 (4): 0 241--433, 2015

2015
[35]

Efficient formal safety analysis of neural networks

Wang, S., Pei, K., Whitehouse, J., Yang, J., and Jana, S. Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31, 2018

2018
[36]

Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.-J., and Kolter, J. Z. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34: 0 29909--29921, 2021

2021
[37]

and Kolter, J

Wong, E. and Kolter, J. Z. Learning perturbation sets for robust machine learning. In International Conference on Learning Representations, 2021

2021
[38]

and Kolter, Z

Wong, E. and Kolter, Z. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp.\ 5286--5295, 2018

2018
[39]

Automatic perturbation analysis for scalable certified robustness and beyond

Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.-W., Huang, M., Kailkhura, B., Lin, X., and Hsieh, C.-J. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33: 0 1129--1141, 2020

2020
[40]

Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C.-J. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representation (ICLR), 2021

2021
[41]

Lot: Layer-wise orthogonal training on improving l2 certified robustness

Xu, X., Li, L., and Li, B. Lot: Layer-wise orthogonal training on improving l2 certified robustness. Advances in Neural Information Processing Systems, 35: 0 18904--18915, 2022

2022
[42]

Efficient neural network robustness certification with general activation functions

Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., and Daniel, L. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018

2018
[43]

Zhang, H., Wang, S., Xu, K., Li, L., Li, B., Jana, S., Hsieh, C.-J., and Kolter, J. Z. General cutting planes for bound-propagation-based neural network verification. Advances in Neural Information Processing Systems, 2022

2022
[44]

A., and Zhang, H

Zhou, D., Brix, C., Hanasusanto, G. A., and Zhang, H. Scalable neural network verification with branch-and-bound inferred cutting planes. In The Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024

2024
[45]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Towards Optimal Branching of Linear and Semidefinite Relaxations for Neural Network Robustness Certification

Anderson, B. G., Ma, Z., Li, J., and Sojoudi, S. Partition-based convex relaxations for certifying the robustness of relu neural networks. arXiv preprint arXiv:2101.09306, 2021

work page Pith review arXiv 2021

[2] [2]

J., Delattre, B., Allauzen, A., and Hu, B

Araujo, A., Havens, A. J., Delattre, B., Allauzen, A., and Hu, B. A unified algebraic perspective on lipschitz neural networks. In ICLR, 2023

work page 2023

[3] [3]

Certifiably robust variational autoencoders

Barrett, B., Camuto, A., Willetts, M., and Rainforth, T. Certifiably robust variational autoencoders. In International Conference on Artificial Intelligence and Statistics, pp.\ 3663--3683. PMLR, 2022

work page 2022

[4] [4]

Efficient neural network verification via layer-based semidefinite relaxations and linear cuts

Batten, B., Kouvaros, P., Lomuscio, A., and Zheng, Y. Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In IJCAI, pp.\ 2184--2190, 2021

work page 2021

[5] [5]

N., Bak, S., Johnson, T

Brix, C., M \"u ller, M. N., Bak, S., Johnson, T. T., and Liu, C. First three years of the international verification of neural networks competition (vnn-comp). International Journal on Software Tools for Technology Transfer, 25 0 (3): 0 329--339, 2023

work page 2023

[6] [6]

T., and Wu, H

Brix, C., Bak, S., Johnson, T. T., and Wu, H. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results. arXiv preprint arXiv:2412.19985, 2024

arXiv 2024

[7] [7]

A., Schmerling, E., Azizan, N., and Pavone, M

Brown, R. A., Schmerling, E., Azizan, N., and Pavone, M. A unified view of sdp-based neural network verification through completely positive programming. In International conference on artificial intelligence and statistics, pp.\ 9334--9355. PMLR, 2022

work page 2022

[8] [8]

and Zhang, R

Chiu, H.-M. and Zhang, R. Y. Tight certification of adversarially trained neural networks via nonconvex low-rank semidefinite relaxations. In International Conference on Machine Learning, pp.\ 5631--5660. PMLR, 2023

work page 2023