Order-Leading Branch and Bound for Neural Network Verification

Certifying the correctness, robustness, and safety of deep neural networks has become a pressing imperative. Despite their ubiquitous deployment in image classification, software engineering, and bug detection, the field still lacks rigorous methodologies to verify their behavior. Although high-level principles for safe and responsible AI are now widely endorsed, existing techniques that analyze each model in isolation often fall short, facing opaque behaviors, cascading errors across continual retraining, pruning, or unlearning throughout the lifecycle. This thesis addresses that gap by reconceiving deep learning model verification as a scalable, life-cycle-aware service rather than a one-off, model-centric exercise. The thesis is reasoning and opening the black box of the model, and delivers three advances: - End-to-end robustness profiling. Two empirical studies trace how data drift, weak labels, configuration nondeterminism and large-scale unlearning jointly erode both empirical accuracy and formal safety margins. A proposed search-based variance framework pinpoints robustness issues and distils actionable guidelines for AI pipelines. - Order-leading branch-and-bound (Oliva). Conventional sound-and-complete verifiers explore BaB subproblems equally. Oliva assigns subproblems a prioritized ``counterexample potentiality'' and schedules the most promising branches first. Greedy, deterministic Monte-Carlo-search and stochastic simulated-annealing variants accelerate falsification by up to 80x and improve the efficiency of neural network verification without sacrificing completeness. - Template-reuse verification (TroV). As industrial models are rarely static, TroV treats the fully explored BaB tree of a previously certified/falsified model history as a reusable template. When weights change through pruning, quantization or machine-unlearning, only subtrees whose bounds are invalidated are reopened. Our new scheduling approach speeds verification up to 42x compared with the best previous incremental tool and achieves higher verification scalability. Overall, the three contributions establish a lifecycle-oriented verification service. Robustness profiling diagnoses weaknesses early; Oliva uncovers violations efficiently; and TroV accelerates re-verification as models evolve. Taken as a whole, they provide practitioners with an end-to-end, scalable framework for building, evaluating, and maintaining trustworthy neural networks across successive development cycles.

Grantor dc:publisher

UNSW, Sydney

Year dc:date

2025

Author dc:creator

• Zhang, Guanqin

• Formal verification
• Machine learning
• Software engineering
• anzsrc-for: 46 INFORMATION AND COMPUTING SCIENCES
• anzsrc-for: 461203 Formal methods for software
• anzsrc-for: 460210 Satisfiability and optimisation
• anzsrc-for: 4602 Artificial intelligence

Statement dc:rights

• embargoed access
• CC BY 4.0

Licence

• http://purl.org/coar/access_right/c_f1cf
• https://creativecommons.org/licenses/by/4.0/

Language dc:language

en

Identifier

https://doi.org/10.26190/unsworks/31922

OAI identifier oai:identifier

oai:unsworks.library.unsw.edu.au:1959.4/106703