Expressive specifications for neural network verification and certified training
File(s)
Author(s)
Hanspal, Harleen
Type
Thesis
Abstract
As neural networks increasingly underpin critical applications such as autonomous driving, healthcare, and security, ensuring their robustness and trustworthiness has become imperative. Formal verification addresses this need by providing deterministic guarantees on network performance against specified perturbations. Most existing verification approaches focus on pixel-space perturbations bounded either by ℓp norms or mathematical transforms. While mathematically convenient, these formulations fail to precisely capture the diverse variations ubiquitous in the real world, such as illumination changes, background shifts, or semantic variations.
Motivated by this shortcoming, the overarching goal of this thesis is to design precise and expressive specifications that allow better modeling of realistic perturbations, and enable more efficient verification and certified training of networks for these specifications than currently possible. To this end, we introduce two complementary frameworks. The first introduces Fourier-domain specifications, enabling verification and certified training against frequency-characterised perturbations. This framework extends verification and certified training to a wide range of spectral variations, from low-frequency illumination patterns, sharpness variations, and style changes to high-frequency noise. The second framework leverages latent variable models and invertible networks to define specifications in learned latent manifolds, thereby capturing semantically meaningful variations such as object appearance and pose. Building on this, we employ certified training to enhance robustness to continuous background variations in images. Beyond supervised robustness, we formulate novel certifiably-robust contrastive learning objectives for unsupervised representation learning, yielding robust feature encoders that generalise across datasets.
Collectively, these contributions advance verifiable robustness along three dimensions: what perturbations can be verified, which networks can be verified, and how networks can be trained to maintain verifiable guarantees without excessive regularisation. By grounding verification to structured and semantically meaningful specifications, this thesis bridges the gap between theoretical verification capabilities and practical robustness requirements, offering insights into the development of efficient and practically relevant certified vision systems.
Motivated by this shortcoming, the overarching goal of this thesis is to design precise and expressive specifications that allow better modeling of realistic perturbations, and enable more efficient verification and certified training of networks for these specifications than currently possible. To this end, we introduce two complementary frameworks. The first introduces Fourier-domain specifications, enabling verification and certified training against frequency-characterised perturbations. This framework extends verification and certified training to a wide range of spectral variations, from low-frequency illumination patterns, sharpness variations, and style changes to high-frequency noise. The second framework leverages latent variable models and invertible networks to define specifications in learned latent manifolds, thereby capturing semantically meaningful variations such as object appearance and pose. Building on this, we employ certified training to enhance robustness to continuous background variations in images. Beyond supervised robustness, we formulate novel certifiably-robust contrastive learning objectives for unsupervised representation learning, yielding robust feature encoders that generalise across datasets.
Collectively, these contributions advance verifiable robustness along three dimensions: what perturbations can be verified, which networks can be verified, and how networks can be trained to maintain verifiable guarantees without excessive regularisation. By grounding verification to structured and semantically meaningful specifications, this thesis bridges the gap between theoretical verification capabilities and practical robustness requirements, offering insights into the development of efficient and practically relevant certified vision systems.
Version
Open Access
Date Issued
2026-01-04
Date Awarded
2026-05-01
Copyright Statement
Attribution-NonCommercial 4.0 International Licence (CC BY-NC)
License URL
Advisor
Lomuscio, Alessio
Publisher Department
Department of Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)