Marta Kwiatkowska – Safety Verification of Deep Neural Networks

October 19th, 2017

Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. This lecture will describe progress with developing a novel automated verification framework for deep neural networks to ensure safety of their classification decisions with respect to image manipulations, for example scratches or changes to camera angle or lighting conditions, that should not affect the classification. The techniques work directly with the network code and, in contrast to existing methods, can offer guarantees that adversarial examples are found if they exist. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples.

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (, the leading software tool in the area and winner of the HVC Award 2016. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, game theory, planning and systems biology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska gave the Milner Lecture in 2012 in recognition of « excellent and original theoretical work which has a perceived significance for practical computing » and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm in 2014. Her research has been supported by the ERC Advanced Grant VERIWARE « From software verification to everyware verification » and the EPSRC Programme Grant on Mobile Autonomy. She is a Fellow of ACM, Member of Academia Europea and Fellow of EATCS.

Richard Szeliski – Visual Reconstruction and Image-Based Rendering

September 12th 2017 The reconstruction of 3D scenes and their appearance from imagery is one of the longest-standing problems in computer vision. Originally developed to support robotics and artificial intelligence applications, it has found some of its most widespread use in the support of interactive 3D scene visualization. One of…

Continue reading

Valérie Berthé – Numbers, computers and dynamical systems

March 9, 2017 A discrete dynamical system is defined as a set of states on which a transformation acts, considered as an evolution rule. The terminology discrete refers to the time that is discretized: at time n corresponds the nth iteration of this transformation. Dynamical systems are widely studied, for…

Continue reading

Gabriel Peyré – Numerical Optimal Transport and Applications

January 19th, 2017 Optimal transport (OT) has become a fundamental mathematical theoretical tool at the interface between calculus of variations, partial differential equations and probability. It took however much more time for this notion to become mainstream in numerical applications. This situation is in large part due to the high…

Continue reading