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

arXiv: https://arxiv.org/abs/2506.06665 · HTML: https://mlsanity.com/paper/2506.06665/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 42 references that are in the map.
- First posted on arXiv 7 Jun 2025.

## Builds on (most cited first, 24 of 24)

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Regularisation of Neural Networks by Enforcing Lipschitz Continuity](https://mlsanity.com/paper/1804.04368/) (2018)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks](https://mlsanity.com/paper/1902.08722/) (2019)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Orthogonalizing Convolutional Layers with the Cayley Transform](https://mlsanity.com/paper/2104.07167/) (2021)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Bounds](https://mlsanity.com/paper/2111.01395/) (2021)
- [A Dynamical System Perspective for Lipschitz Neural Networks](https://mlsanity.com/paper/2110.12690/) (2021)
- [A Unified Algebraic Perspective on Lipschitz Neural Networks](https://mlsanity.com/paper/2303.03169/) (2023)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Learning perturbation sets for robust machine learning](https://mlsanity.com/paper/2007.08450/) (2020)
- [Improved deterministic l2 robustness on CIFAR-10 and CIFAR-100](https://mlsanity.com/paper/2108.04062/) (2021)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Certifiably Robust Variational Autoencoders](https://mlsanity.com/paper/2102.07559/) (2021)
- [Unlocking Deterministic Robustness Certification on ImageNet](https://mlsanity.com/paper/2301.12549/) (2023)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)

## Built on by (most cited first, 12 of 12)

- [Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees](https://mlsanity.com/paper/2602.16823/) (2026)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Learning to Optimize by Differentiable Programming](https://mlsanity.com/paper/2601.16510/) (2026)
- [Cascading Robustness Verification: Toward Efficient Model-Agnostic Certification](https://mlsanity.com/paper/2602.04236/) (2026)
- [Provably Explaining Neural Additive Models](https://mlsanity.com/paper/2602.17530/) (2026)
- [Testing Between the Test Cases: Proving End-to-End Steering in Conditions You Never Drove](https://mlsanity.com/paper/2609.10951/) (2026)
- [Distributionally Robust Safety Verification of Neural Networks via Worst-Case CVaR](https://mlsanity.com/paper/2509.17413/) (2025)
- [Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement](https://mlsanity.com/paper/2511.07741/) (2025)
- [Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks](https://mlsanity.com/paper/2605.24084/) (2026)
- [Fast SDP certification of neural networks : towards large multi-class datasets](https://mlsanity.com/paper/2607.03232/) (2026)
- [CLAD: Constrained Abstract Domain for Neural Network Verification](https://mlsanity.com/paper/2609.34628/) (2026)
- [Certified Robustness via Sparse Second-Order Cone Relaxations](https://mlsanity.com/paper/2610.16016/) (2026)

## Abstract (arXiv)

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 ℓ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 √n tighter than traditional per-neuron bounds. In practice, when incorporated into the state-of-the-art α-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.