Research map / Learning theory and algorithms / Combinatorial and search optimization
SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes SDP-CROWN, a hybrid that adds an SDP-derived l2-inter-neuron linear bound (one extra parameter per layer) to alpha-CROWN for tighter l2 robustness verification of large ReLU networks.
Problem
Linear bound propagation verifiers are loose under l2-norm input perturbations because they relax the l2 ball into an l_inf box, losing inter-neuron coupling, while SDP verifiers are tight but cubic in cost and do not scale.
Approach
Derive a closed-form linear relaxation of c^T ReLU(x) valid over the l2 ball, obtained by dualizing the SDP relaxation of the ReLU and l2-ball constraints, which replaces the offset of the box-based bound with a term involving one scalar lambda per layer; this is plugged into the backward bound propagation pass.
Key results
- On CIFAR-10 ConvLarge (2.47M params, 65,546 neurons), SDP-CROWN verifies 63.5% vs 2.5% for alpha-CROWN and 6% for beta-CROWN at rho=8/255, with ~73 s per instance.
- On MNIST ConvSmall at rho=0.3, SDP-CROWN achieves 81.5% verified accuracy vs 84.5% PGD upper bound, versus 19.5% for GCP-CROWN.
- Theory: the l2 offset is up to sqrt(n) tighter than the l_inf box-based offset for zero-centered input (one-neuron example and bound proof).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use SDP-CROWN instead of BM-Full | MNIST MLP · MNIST MLP | verified accuracy: 53% -> 32.5% | Hurt |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | MNIST ConvSmall · MNIST ConvSmall | verified accuracy: 78.5% -> 81.5% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | MNIST ConvLarge · MNIST ConvLarge | verified accuracy: 77% -> 79.5% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 CNN-A · CIFAR-10 CNN-A | verified accuracy: 39% -> 49% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 CNN-B · CIFAR-10 CNN-B | verified accuracy: 33% -> 49.5% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 CNN-C · CIFAR-10 CNN-C | verified accuracy: 38.5% -> 42.5% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 ConvSmall · CIFAR-10 ConvSmall | verified accuracy: 33.5% -> 43.5% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 ConvDeep · CIFAR-10 ConvDeep | verified accuracy: 39.5% -> 46% | Helped |
| Add SDP-derived inter-neuron coupling bounds to bound propagation | CIFAR-10 ConvLarge · CIFAR-10 ConvLarge | verified accuracy: 47.5% -> 63.5% | Helped |
Surprising findings
- Lipschitz-based LipNaive is consistently tighter than the state-of-the-art bound-propagation verifiers alpha-CROWN, beta-CROWN, GCP-CROWN and BICCOS on the l2 benchmarks.
Limitations
- Tightness for nonzero input center (hat x != 0) cannot be analyzed analytically; only empirical evidence.
- Models must be retrained to have small global Lipschitz constant to make l2 verification non-vacuous.
- Some baselines (LP-All, BM-Full, LipSDP) fail to run on larger models, so comparisons are limited to smaller models.
Experimental setup
Datasets: MNIST CIFAR-10
Benchmarks: MNIST verified accuracy under l2 perturbation CIFAR-10 verified accuracy under l2 perturbation
Metrics: verified accuracy (%) verification time lower bound on robustness margin offset tightness
Baselines: alpha-CROWN beta-CROWN GCP-CROWN BICCOS LipNaive LipSDP LP-All BM-Full
Builds on: alpha-CROWN CROWN LiRPA SDP relaxation of ReLU (Raghunathan et al.) LipSDP
Closest papers by meaning
- Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification (NeurIPS 2021 · similarity 0.94)
- Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.90)
- Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (NeurIPS 2024 · similarity 0.89)
- Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification (AAAI 2025 · similarity 0.88)
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.87)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.