Talks

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.

Title: Mechanising Euler's Infinite Analysis in the Proof Assistant Isabelle
Speaker: Imogen Morris
Abstract:

I will describe my work this year on formalising Euler's proof of the Basel problem . The proof which I have partially formalised is from Euler's textbook `Introduction to the Analysis of the Infinite', in which he aims to show that the manipulation of infinitely small and infinitely large quantities can be accomplished using `ordinary algebra'. Euler's arguments using infinity and his theory of infinitesimals are not considered rigorous by present-day mathematicians. However, there is a modern theory of infinities and infinitesimals called nonstandard analysis, which captures many of the properties that 18th century mathematicians ascribed to infinite and infinitesimal numbers. I use this theory and the proof assistant Isabelle, as the framework to mechanise Euler's proof. My project aims to demonstrate that Euler's reasoning can be made consistent and that Euler appreciated the subtleties of infinitesimals. In my talk, I will also outline my plans for further research which include other arguments from Euler's textbook e.g. the infinite product for sine in terms of its roots and generalisations of the Basel problem.

Title: Formalising the correct termination, fairness, and tractability of Meek's method of STV in Isabelle/HOL
Speaker: Jake Palmer
Abstract:

I will present my work on formalising various properties of Meek's method of STV. So far I have represented and proved the quantities, assumptions, and theorems in the paper "Algorithm 123: Single transferable vote by Meek's method", wherein they provide a proof that when some number of candidates are elected at some stage of the process, they remain elected and their votes converge on the quota (i.e. what a candidate needs to be elected) and this converged-to state is unique. I will briefly present some ideas on a more complete proof of correct termination which takes into account filling seats, and some ideas on how to go beyond that to making the notions of fairness and "wasted votes" in Meek rigorous and formally proving they are satisfied by the method. Finally, I will finish off the work by proving the tractability of the method in terms of its time complexity, and extract the verified algorithm.

Title: L'Hopital's Theorems and Euler's Notions of Orders of Infinity in Isabelle/HOL
Speaker: Kyriakos Katsamaktsis
Abstract:
In his paper on "Orders of Infinity" Euler writes, without rigorous proofs, about "infinitely large" and "infinitely small" quantities and how they relate to one another. For example, he writes that if x is infinite, then its logarithm is also infinite, and the ratio of the logarithm of x divided by x is infinitely small. Such statements can be put on a rigorous footing using nonstandard analysis, which treats infinity as a number (or more than one) without using limits. We will describe the formalisation of parts of Euler's paper in Isabelle using nonstandard analysis. We will shed light on a few vague statements and show how fairly standard modern mathematics plus some nonstandard analysis can resolve them.

Title: Hybrid Process Mining: Combining Imperative & Declarative Paradigms
Speaker: Christoffer Olling Back (PhD Fellow, Department of Computer Science, University of Copenhagen)
Abstract:

Modern organisations generate enormous amounts of data related to their business processes via IT systems such as Enterprise Resource Planning (ERP) systems. Mining process related data presents the opportunity for a truly data-driven approach to streamlining operations and building an intelligent enterprise. Depending on the use case, process mining may be employed with the aim of detecting deviations from a well-defined process, identifying areas for process enhancement (detecting bottlenecks, unnecessary rework), and in the case of pure process discovery – where the underlying process is not known – the task essentially becomes comparable to unsupervised learning.

In this talk, I will begin with a brief introduction to process mining generally, positioning the field in relation to data mining and machine learning. Afterwards, I will discuss different process modelling paradigms in more detail, and their strengths and weaknesses. In particular, the distinction between declarative (constraint-based) and imperative (flow-based) languages, and how they can be combined to form hybrid process models which combine the strengths of both. Time permitting, I will discuss my ongoing work on developing process mining algorithms which generate hybrid models by identifying pockets of regularity using an information theoretic approach, as well as challenges in empirically evaluating process mining algorithms.

Title: Predicting graft and patient survival following liver transplantation
Speaker: Simon Thorogood
Abstract:
I'll aim to cover a bit of the medical background (Why do people need liver transplants? What are the challenges when allocating livers?). I'll also talk about the NHSBT dataset I am using and some of the traditional statistical approaches to survival prediction (specifically, the field of Survival Analysis). Finally I'll discuss some of the machine learning approaches that I will be applying to the problem.

Title: Formal Resource Flow Composition
Speaker: Petros Papapanagiotou
Abstract:
Resource flows are models of how resources travel across connected processes. They offer a different perspective to more typical workflow models (e.g. flow charts) where the focus is on control flow (the order of execution). Formal composition involves the rigorous, logic-based combination of processes to build resource flows with guaranteed properties, particularly systematic resource accounting (so that resources do no appear from/disappear into thin air). I will describe the problem in the context of the WorkflowFM system developed over the past 11 years. This relies on the HOL Light theorem prover to perform compositions via proof in Classical Linear Logic. In this particular talk I will focus on practical examples to demonstrate the conceptual challenges. Describing this work has been a challenge in itself, as WorkflowFM can fit may different contexts and paradigms (program synthesis, scientific workflows, Business Process Management, data streams handling, etc.). I am hoping to gather some feedback after the talk on your understanding and perspective, towards improving how these concepts can be better presented.

Title: Nonstandard analysis for Euler’s proof of the Basel Problem
Speaker: Imogen Morris
Abstract: I will describe the background theory of nonstandard analysis which I am using to formalise the proof of the Basel problem from Euler's `Introduction to the Analysis of the Infinite'. Euler's arguments using infinity and his theory of infinitesimals are not considered rigorous by present-day mathematicians. However, there is a modern theory of infinities and infinitesimals called nonstandard analysis, which captures many of the properties that 18th century mathematicians ascribed to infinite and infinitesimal numbers. I will explain some of the properties of these numbers and how they can be constructed. I will also explain hyperfinite sums and internal functions, which are both necessary to for my theory of 'infinite polynomials'. I will describe some of the relevant theorems which I have formalised in the proof assistant Isabelle.

Title: Learning over Isabelle's Dependency Graphs
Speaker: James Vaughn

Title: Formalising the correct convergence of Meek's method of STV in Isabelle/HOL
Speaker: Jake Palmer
Abstract: I will present an overview of my work so far on formalising a representation of the surplus transfer phase of Meek's method of STV. I have represented the assumptions characterising the way in which the quota, excess, and votes update given a single update to a candidate's weight, where the weights represent the current state. I will present some convergence and ordering theorems on weights as well as the theorem in Isabelle characterising the first part of Theorem 1 in the paper "Algorithm 123: Single transferable vote by Meek's method". I will briefly present some ideas on the work which will make up the rest of the PhD such as implementing Meek's method in Isabelle, situating the method within the framework of social choice theory, showing that the method is not susceptible to the butterfly effect in voting, and producing Meek's method automatically as the output of generating a method/policy for minimising wasted votes in the context of STV.