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

Chen, Hao

Permalink

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

Description

Title

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

Author(s)

Chen, Hao

Issue Date

2025-05-05

Director of Research (if dissertation) or Advisor (if thesis)

Zhang, Huan

Department of Study

Electrical & Computer Eng

Discipline

Electrical & Computer Engr

Degree Granting Institution

University of Illinois Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• Trustworthy AI
• Semi-definite Programming

Abstract

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.

Graduation Semester

2025-05

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2025 Hao Chen

Owning Collections