Title: Formal Verification for Reinforcement Learning
Speaker: Mark Chevallier
Abstract:

I’m going to talk about my work on finding useful interactions between reinforcement learning and interactive theorem proving.
Several approaches will be discussed, primarily using reinforcement learning methods to improve automation in interactive theorem proving and also formalising various different kinds of reinforcement learning methods using an interactive theorem proving model, with a particular focus on the convergence of the value or policy function to the underlying values. The theorem proving tools used are Isabelle/HOL.

Some of my early work I will talk about focused on attempting to use a simple reinforcement learning agent to prove theorems automatically, work which succeeded in proving some very simple theorems only. In addition, I’ll speak about the successful modelling of a reinforcement learning agent that worked with a deterministic Markov Decision Process and did not engage in exploration without manual intervention.

I will also talk about my decision to focus on formalisation as the most practical and potentially fruitful avenue of research.