A linear constraint driven approach to efficiently enhancing branch and bound in neural network verification

The verification of neural network systems is crucial as the adoption of these systems are considered for safety-critical tasks. A neural network system that works empirically well may not be robust, and when employed in areas such as cyber-security and cyber-physical systems, the guaranteed performance is a must. Formal verification is a rapidly growing field that delves into providing these guarantees, ensuring that properties on these networks can be assured. This thesis serves as an introduction into the common techniques used to provide such guarantees. There is a particular focus on bound propagation techniques as such techniques have fueled state-of-the-art, efficient verifiers. After covering the many advances that have been made in neural network verification, we will delve further into the branch-and-bound paradigm that typically accompanies many existing verifiers, as well as demonstrate an insightful algorithm that is capable of garnering further efficacy from bound propagation verifiers.

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

• Chavez, Jorge

Contributors dc:contributor

• Zhang, Huan

• Machine Learning
• Neural Network Verification

Statement dc:rights

• Copyright 2025 Jorge Chavez

Language dc:language

en, eng

Handle dc:identifier

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

OAI record oai:identifier

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