Neural network verification: proving and enforcing adversarial robustness, and beyond

The infamous brittleness of neural networks prompts the need to provide formal guarantees on neural network behaviour.
This is particularly relevant in the context of adversarial attacks: imperceptible input perturbations that induce misclassifications.
In this talk, I will first show how these guarantees can be obtained through so-called neural network verification algorithms, which amount to solving a global optimisation problem over a trained neural network. I will then present effective algorithms to enforce these guarantees at training time, known as certified training, demonstrating that specialised network design is crucial to meaningfully scale verification to even moderate network sizes. Finally, I will conclude the talk by showcasing the wider applicability of these techniques.