SDP-CROWN: Efficient bound propagation for neural network verification with tightness of semidefinite programming
Chen, Hao
Loading…
Permalink
https://hdl.handle.net/2142/129276
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
Language
eng
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
