{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/129276"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/129276","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"SDP-CROWN: Efficient bound propagation for neural network verification with tightness of semidefinite programming","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","abstract_has_math":false,"creators":["Chen, Hao"],"institution":"University of Illinois Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Zhang, Huan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-05-05","date_published":"2025-05-05","updated_at":"2026-07-22T22:25:04Z","subjects":["Trustworthy AI","Semi-definite Programming"],"languages":["en","eng"],"rights":["Copyright 2025 Hao Chen"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/129276","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Zhang, Huan"]},{"key":"dc:creator","label":"Author","values":["Chen, Hao"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025-05-05","2025-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Trustworthy AI","Semi-definite Programming"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2025 Hao Chen"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/129276"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Hao Chen, accepted the attached license on 2025-04-29 at 09:55.","The student, Hao Chen, submitted this Thesis for approval on 2025-04-29 at 10:18.","This Thesis was approved for publication on 2025-05-05 at 12:14.","DSpace SAF Submission Ingestion Package generated from Vireo submission #22069 on 2025-10-19 at 18:11:14","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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["SDP-CROWN: Efficient bound propagation for neural network verification with tightness of semidefinite programming"]}]}],"canonical_facts":{"dc:contributor":["Zhang, Huan"],"dc:creator":["Chen, Hao"],"dc:date":["2025-05-05","2025-05"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-10-19 without embargo terms","The student, Hao Chen, accepted the attached license on 2025-04-29 at 09:55.","The student, Hao Chen, submitted this Thesis for approval on 2025-04-29 at 10:18.","This Thesis was approved for publication on 2025-05-05 at 12:14.","DSpace SAF Submission Ingestion Package generated from Vireo submission #22069 on 2025-10-19 at 18:11:14","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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/129276"],"dc:language":["en","eng"],"dc:rights":["Copyright 2025 Hao Chen"],"dc:subject":["Trustworthy AI","Semi-definite Programming"],"dc:title":["SDP-CROWN: Efficient bound propagation for neural network verification with tightness of semidefinite programming"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:04Z"}