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

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

## Key facts

- Cited by 66 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Oct 2020.

## Built on by (most cited first, 30 of 66)

- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Natural Language Descriptions of Deep Visual Features](https://mlsanity.com/paper/2201.11114/) (2022)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [Boosting Randomized Smoothing with Variance Reduced Classifiers](https://mlsanity.com/paper/2106.06946/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Partition-based formulations for mixed-integer optimization of trained ReLU neural networks](https://mlsanity.com/paper/2102.04373/) (2021)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [OMLT: Optimization & Machine Learning Toolkit](https://mlsanity.com/paper/2202.02414/) (2022)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Boosting the Certified Robustness of L-infinity Distance Nets](https://mlsanity.com/paper/2110.06850/) (2021)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [Safe Control with Neural Network Dynamic Models](https://mlsanity.com/paper/2110.01110/) (2021)
- [Certified Robustness via Dynamic Margin Maximization and Improved Lipschitz Regularization](https://mlsanity.com/paper/2310.00116/) (2023)
- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [Provably Robust Detection of Out-of-distribution Data (almost) for free](https://mlsanity.com/paper/2106.04260/) (2021)
- [Wasserstein distributional robustness of neural networks](https://mlsanity.com/paper/2306.09844/) (2023)
- [Towards Evaluating and Training Verifiably Robust Neural Networks](https://mlsanity.com/paper/2104.00447/) (2021)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [On the Paradox of Certified Training](https://mlsanity.com/paper/2102.06700/) (2021)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)
- [Adversarial robustness of sparse local Lipschitz predictors](https://mlsanity.com/paper/2202.13216/) (2022)
- [Optimizing Objective Functions from Trained ReLU Neural Networks via Sampling](https://mlsanity.com/paper/2205.14189/) (2022)
- [TAPS: Connecting Certified and Adversarial Training](https://mlsanity.com/paper/2305.04574/) (2023)
- [Linearity Grafting: Relaxed Neuron Pruning Helps Certifiable Robustness](https://mlsanity.com/paper/2206.07839/) (2022)
- [Closing the Loop: A Framework for Trustworthy Machine Learning in Power Systems](https://mlsanity.com/paper/2203.07505/) (2022)
- [Improved techniques for deterministic l2 robustness](https://mlsanity.com/paper/2211.08453/) (2022)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)

## Abstract (arXiv)

Convex relaxations have emerged as a promising approach for verifying desirable properties of neural networks like robustness to adversarial perturbations. Widely used Linear Programming (LP) relaxations only work well when networks are trained to facilitate verification. This precludes applications that involve verification-agnostic networks, i.e., networks not specially trained for verification. On the other hand, semidefinite programming (SDP) relaxations have successfully be applied to verification-agnostic networks, but do not currently scale beyond small networks due to poor time and space asymptotics. In this work, we propose a first-order dual SDP algorithm that (1) requires memory only linear in the total number of network activations, (2) only requires a fixed number of forward/backward passes through the network per iteration. By exploiting iterative eigenvector methods, we express all solver operations in terms of forward and backward passes through the network, enabling efficient use of hardware like GPUs/TPUs. For two verification-agnostic networks on MNIST and CIFAR-10, we significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.