{"id":{"repo_id":"unsw","oai_identifier":"oai:unsworks.library.unsw.edu.au:1959.4/106703"},"canonical_url":"https://search.dev.ndltd.org/etd/unsw/oai:unsworks.library.unsw.edu.au:1959.4/106703","repository":{"repo_id":"unsw","name":"University of New South Wales","base_url":"https://unsworks.unsw.edu.au/oai/provider"},"display":{"title":"Order-Leading Branch and Bound for Neural Network Verification","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Zhang, Guanqin"],"institution":"UNSW, Sydney","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025","date_published":"2025","updated_at":"2026-07-24T05:32:27Z","subjects":["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"],"languages":["en"],"rights":["embargoed access","CC BY 4.0"],"rights_urls":["http://purl.org/coar/access_right/c_f1cf","https://creativecommons.org/licenses/by/4.0/"],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["https://doi.org/10.26190/unsworks/31922"],"render_values":[{"text":"https://doi.org/10.26190/unsworks/31922","href":"https://doi.org/10.26190/unsworks/31922","code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/1959.4/106703","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Zhang, Guanqin"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2025"]},{"key":"dc:publisher","label":"Institution","values":["UNSW, Sydney"]},{"key":"dc:type","label":"Dc Type","values":["doctoral thesis","http://purl.org/coar/resource_type/c_db06"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["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"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["embargoed access","http://purl.org/coar/access_right/c_f1cf","CC BY 4.0","https://creativecommons.org/licenses/by/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/1959.4/106703","https://doi.org/10.26190/unsworks/31922"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:title","label":"Title","values":["Order-Leading Branch and Bound for Neural Network Verification"]}]}],"canonical_facts":{"dc:creator":["Zhang, Guanqin"],"dc:date":["2025"],"dc:description":["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."],"dc:identifier":["http://hdl.handle.net/1959.4/106703","https://doi.org/10.26190/unsworks/31922"],"dc:language":["en"],"dc:publisher":["UNSW, Sydney"],"dc:rights":["embargoed access","http://purl.org/coar/access_right/c_f1cf","CC BY 4.0","https://creativecommons.org/licenses/by/4.0/"],"dc:subject":["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"],"dc:title":["Order-Leading Branch and Bound for Neural Network Verification"],"dc:type":["doctoral thesis","http://purl.org/coar/resource_type/c_db06"]},"updated_at":"2026-07-24T05:32:27Z"}