SDP-CROWN: Efficient bound propagation for neural network verification with tightness of semidefinite programming

As deep learning systems are increasingly deployed in safety-critical applications such as autonomous driving, medical diagnostics, and security, people are focusing on the safety and robustness of neural networks. Neural network verification provides the necessary guarantees about system behavior under adversarial conditions. Research in verification have shown that methods based on linear bound propagation scale remarkably well to large models. However, these approaches can yield very loose bounds when inter-neuron coupling plays a significant role, for example, when the input perturbation is in ℓ2 norm. In contrast, semidefinite programming (SDP) based verifiers naturally take advantage of such coupling, but are limited to small networks due to their cubic computational complexity. In this paper, we introduce SDP-CROWN, a hybrid verification framework that combines the precision of SDP relaxations with the scalability of linear bound propagation methods. The key idea of SDP-CROWN is a novel linear bound that explicitly incorporates ℓ2-norm-based inter-neuron coupling with only a few additional parameter per layer. It can integrate into α-Crown bound propagation pipeline easily and maintaining scalability. And it surprisingly enhances the tightness of the verification in ℓ2-norm perturbation. Our theoretical analysis shows that this inter-neuron bound can be up to a factor of √n tighter than traditional per-neuron bounds. Experimentally, when embedded into the state-of-the-art α-CROWN verifier, SDP-CROWN delivers notable improvements in verification performance on large-scale models with up to 65,000 neurons and 2.47 million parameters.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Electrical & Computer Engr

Grantor

University of Illinois Urbana-Champaign

Year dc:date

2025

Author dc:creator

• Chen, Hao

Contributors dc:contributor

• Zhang, Huan

• Trustworthy AI
• Semi-definite Programming

Statement dc:rights

• Copyright 2025 Hao Chen

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/129276

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F129276