Speaker
Description
Abstract: Over the past 35 years, one branch of formal methods has pushed the envelope from discrete to continuous state spaces, to handle the verification and control of cyber-physical systems.
At the heart of these methods lie correctness certificates that are functions on continuous state spaces, such as abstraction, invariant, barrier, and progress functions.
Entirely independently, a particular data structure for representing continuous nonlinear functions has gained recent prominence: the neural network.
By using neural networks to jointly learn both controllers and correctness certificates for continuous and hybrid state spaces, the complexity of the residual verification tasks can be reduced.
We survey the resulting learner-verifier feedback architecture and explain why we believe that it offers great potential for a systematic symbiosis of deep learning and formal methods, to provide formal guarantees for an important class of AI systems such as robots and autopilots.