# Chordal Sparsity for SDP-based Neural Network Verification

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 50 references that are in the map.
- First posted on arXiv 7 Jun 2022.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [CARLA: An Open Urban Driving Simulator](https://mlsanity.com/paper/1711.03938/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Learning Deep Neural Network Representations for Koopman Operators of Nonlinear Dynamical Systems](https://mlsanity.com/paper/1708.06850/) (2017)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Training robust neural networks using Lipschitz bounds](https://mlsanity.com/paper/2005.02929/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [JuMP: A Modeling Language for Mathematical Optimization](https://mlsanity.com/paper/1508.01982/) (2015)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networks](https://mlsanity.com/paper/2204.00846/) (2022)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [A Unified View of SDP-based Neural Network Verification through Completely Positive Programming](https://mlsanity.com/paper/2203.03034/) (2022)
- [DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting](https://mlsanity.com/paper/2106.09117/) (2021)
- [Sparse Polynomial Optimisation for Neural Network Verification](https://mlsanity.com/paper/2202.02241/) (2022)
- [Verifying Quantized Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2106.05997/) (2021)
- [QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking](https://mlsanity.com/paper/2111.13110/) (2021)
- [Chordal Decomposition for Spectral Coarsening](https://mlsanity.com/paper/2009.02294/) (2020)

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

- [Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization](https://mlsanity.com/paper/2405.17049/) (2024)
- [A Scalable Approach for Safe and Robust Learning via Lipschitz-Constrained Networks](https://mlsanity.com/paper/2506.23977/) (2025)
- [Convex training of Lipschitz-regularized shallow neural networks](https://mlsanity.com/paper/2606.19652/) (2026)
- [Scalable Incremental Robustness Analysis of Neural Network Feedback Systems](https://mlsanity.com/paper/2609.22576/) (2026)

## Abstract (arXiv)

Neural networks are central to many emerging technologies, but verifying their correctness remains a major challenge. It is known that network outputs can be sensitive and fragile to even small input perturbations, thereby increasing the risk of unpredictable and undesirable behavior. Fast and accurate verification of neural networks is therefore critical to their widespread adoption, and in recent years, various methods have been developed as a response to this problem. In this paper, we focus on improving semidefinite programming (SDP) based techniques for neural network verification. Such techniques offer the power of expressing complex geometric constraints while retaining a convex problem formulation, but scalability remains a major issue in practice. Our starting point is the DeepSDP framework proposed by Fazlyab et al., which uses quadratic constraints to abstract the verification problem into a large-scale SDP. However, solving this SDP quickly becomes intractable when the network grows. Our key observation is that by leveraging chordal sparsity, we can decompose the primary computational bottleneck of DeepSDP -- a large linear matrix inequality (LMI) -- into an equivalent collection of smaller LMIs. We call our chordally sparse optimization program Chordal-DeepSDP and prove that its construction is identically expressive as that of DeepSDP. Moreover, we show that additional analysis of Chordal-DeepSDP allows us to further rewrite its collection of LMIs in a second level of decomposition that we call Chordal-DeepSDP-2 -- which results in another significant computational gain. Finally, we provide numerical experiments on real networks of learned cart-pole dynamics, showcasing the computational advantage of Chordal-DeepSDP and Chordal-DeepSDP-2 over DeepSDP.