Formal verification and certified training of neural networks
File(s)
Author(s)
Brückner, Benedikt
Type
Thesis or dissertation
Abstract
Deep neural networks deployed in safety-critical computer vision applications remain highly vulnerable to input perturbations and spurious correlations. While formal verification provides rigorous safety guarantees, existing methods often focus on simplistic threat models such as norm-bounded perturbations and fail to scale to complex architectures. This thesis addresses these limitations by developing novel verification, Certified Training, and validation frameworks that tackle realistic perturbations and scale to large object detection models.
First, we address convolutional perturbations, such as camera shake and motion blur, by introducing an efficient symbolic encoding based on linearly parameterised perturbation kernels that enables the formal verification of neural networks against these effects. By combining this encoding with ideas from Certified Training, we develop a method for training models that are verifiably robust to convolutional perturbations.
Next, we tackle the challenge of spurious correlations caused by background variations. We propose a framework that leverages Variational Autoencoders to generate continuous, latent-bounded sets of natural backgrounds. By combining this with Certified Training, we produce classifiers that are provably invariant to continuous background shifts, outperforming discrete data augmentation approaches.
Finally, we extend robustness guarantees to object detection, a critical task for autonomous systems. We introduce IoUCert, an architecture-aware verification framework that derives optimal Intersection-over-Union bounds, enabling the formal verification of anchor-based detectors like SSD, YOLOv2, and YOLOv3 for the first time. To support modern, large-scale architectures, we then present H2V-A, a global optimisation framework with spatial branching. H2V-A successfully handles complex non-linearities like SiLU and self-attention, scaling robustness validation to state-of-the-art models with up to 59 million trainable parameters.
Together, these contributions significantly advance the practical applicability of neural network safety, providing scalable methods to ensure robustness against real-world perturbations.
First, we address convolutional perturbations, such as camera shake and motion blur, by introducing an efficient symbolic encoding based on linearly parameterised perturbation kernels that enables the formal verification of neural networks against these effects. By combining this encoding with ideas from Certified Training, we develop a method for training models that are verifiably robust to convolutional perturbations.
Next, we tackle the challenge of spurious correlations caused by background variations. We propose a framework that leverages Variational Autoencoders to generate continuous, latent-bounded sets of natural backgrounds. By combining this with Certified Training, we produce classifiers that are provably invariant to continuous background shifts, outperforming discrete data augmentation approaches.
Finally, we extend robustness guarantees to object detection, a critical task for autonomous systems. We introduce IoUCert, an architecture-aware verification framework that derives optimal Intersection-over-Union bounds, enabling the formal verification of anchor-based detectors like SSD, YOLOv2, and YOLOv3 for the first time. To support modern, large-scale architectures, we then present H2V-A, a global optimisation framework with spatial branching. H2V-A successfully handles complex non-linearities like SiLU and self-attention, scaling robustness validation to state-of-the-art models with up to 59 million trainable parameters.
Together, these contributions significantly advance the practical applicability of neural network safety, providing scalable methods to ensure robustness against real-world perturbations.
Version
Open Access
Date Issued
2026-04-14
Date Awarded
2026-08-01
Copyright Statement
Attribution-NonCommercial 4.0 International Licence (CC BY-NC)
License URL
Advisor
Lomuscio, Alessio
Sponsor
UK Research and Innovation
Grant Number
EP/S023356/1
Publisher Department
Department of Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)