# A Unified View of SDP-based Neural Network Verification through Completely Positive Programming

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 36 references that are in the map.
- First posted on arXiv 6 Mar 2022.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Scaling provable adversarial defenses](https://mlsanity.com/paper/1805.12514/) (2018)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [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)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming](https://mlsanity.com/paper/2010.11645/) (2020)
- [Training verified learners with learned verifiers](https://mlsanity.com/paper/1805.10265/) (2018)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Deep Neural Networks as 0-1 Mixed Integer Linear Programs: A Feasibility Study](https://mlsanity.com/paper/1712.06174/) (2017)
- [DSOS and SDSOS Optimization: More Tractable Alternatives to Sum of Squares and Semidefinite Optimization](https://mlsanity.com/paper/1706.02586/) (2017)
- [On the Tightness of Semidefinite Relaxations for Certifying Robustness to Adversarial Examples](https://mlsanity.com/paper/2006.06759/) (2020)
- [Neural Network Branch-and-Bound for Neural Network Verification](https://mlsanity.com/paper/2107.12855/) (2021)

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

- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [SDP-CROWN: Efficient Bound Propagation for Neural Network Verification with Tightness of Semidefinite Programming](https://mlsanity.com/paper/2506.06665/) (2025)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Discovering Closed-Loop Failures of Vision-Based Controllers via Reachability Analysis](https://mlsanity.com/paper/2211.02736/) (2022)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Chordal Sparsity for SDP-based Neural Network Verification](https://mlsanity.com/paper/2206.03482/) (2022)
- [SAVER: A Toolbox for Sampling-Based, Probabilistic Verification of Neural Networks](https://mlsanity.com/paper/2412.02940/) (2024)
- [Learning to Optimize by Differentiable Programming](https://mlsanity.com/paper/2601.16510/) (2026)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Provably Safe, Yet Scalable Reinforcement Learning](https://mlsanity.com/paper/2606.14536/) (2026)
- [Training Safe Neural Networks with Global SDP Bounds](https://mlsanity.com/paper/2409.09687/) (2024)
- [(DNN)2: Doubly Non-Negative Relaxations for Deep Neural Networks](https://mlsanity.com/paper/2608.24743/) (2026)

## Abstract (arXiv)

Verifying that input-output relationships of a neural network conform to prescribed operational specifications is a key enabler towards deploying these networks in safety-critical applications. Semidefinite programming (SDP)-based approaches to Rectified Linear Unit (ReLU) network verification transcribe this problem into an optimization problem, where the accuracy of any such formulation reflects the level of fidelity in how the neural network computation is represented, as well as the relaxations of intractable constraints. While the literature contains much progress on improving the tightness of SDP formulations while maintaining tractability, comparatively little work has been devoted to the other extreme, i.e., how to most accurately capture the original verification problem before SDP relaxation. In this work, we develop an exact, convex formulation of verification as a completely positive program (CPP), and provide analysis showing that our formulation is minimal -- the removal of any constraint fundamentally misrepresents the neural network computation. We leverage our formulation to provide a unifying view of existing approaches, and give insight into the source of large relaxation gaps observed in some cases.