Talks

Title: Formalisations of Q learning and logic as a loss function
Speaker: Mark Chevallier
Abstract:

Q learning is a form of reinforcement learning where we try to learn how to navigate through an environment where we can earn rewards by earning the biggest reward possible.

I have been working on its formalisation in the theorem prover Isabelle/HOL, and in this talk I will give details about the different ways I have tried to represent rewards and value, and the pitfalls I have discovered making progress along the way.

I will also be discussing a formalisation of a method of evaluating logical constraints as real numbers to use them as part of a loss function in a neural network. This method has been described by others, and by formalising their methods I uncovered a lack of rigour and a better way to approach some of the issues that arose.

I will demonstrate that I was able to use Isabelle/HOL to generate working code based on my formalisation to guarantee the code fulfils the specifications exactly and eliminate any possibility of human error in implementation.

Title: Towards a mechanisation of Euler's Infinite Analysis in the Proof Assistant Isabelle
Speaker: Imogen Morris
Abstract: 

In 1736 Euler published a proof of an astounding relation between π and the reciprocals of the squares.

π ² ⁄ 6 = 1+ 1⁄4 + 1/9 + 1/25 + ...

Until this point, π had not been part of any mathematical relation outside of geometry. This relation would have had an almost supernatural significance to the mathematicians of the time. But even more amazing is Euler's proof. He factorises a transcendental function as if it were a polynomial of infinite degree. He discards infinitely-many infinitely-small numbers. He substitutes 1 for the ratio of two distinct infinite numbers.

Nowadays Euler's proof is held up as an example of both genius intuition and flagrantly unrigorous method. In my talk I will describe how, with the aid of nonstandard analysis, which gives a consistent formal theory of infinitely-small and large numbers, and the proof assistant Isabelle, we are in the process of constructing a formal proof of the Basel problem which uses the method of Euler's original proof. We argue that Euler was consistent in his use of infinitely-large and infinitely-small numbers, and aim to show that his original reasoning provides the structure of a formal proof. We use the concept of "hidden lemmas", developed by McKinzie and Tuckey based on Lakatos and  Laugwitz, to formalise general principles which Euler's proof followed. Towards this end, we have developed a theory of infinite "hyperpolynomials", formal proofs of a version of convergence of the infinite polynomials used by Euler, formalisation of the factorisation and expansion of Euler's infinite polynomial and formal proofs of many steps in Euler's proof.

This talk is part of my 3rd year review and will describe my work done so far, as well as the planned work, which together will become my PhD thesis.

Title: Creating a framework for comparing and selecting process discovery algorithms
Speaker: Demetris Louca
Abstract: Process discovery is the part of Process mining that creates a model to describe the behaviour of an event-log. Whether it is for training future doctors or optimising business processes, finding the underlying model is essential in gaining an understanding of the occurring processes.

There have been multiple algorithms proposed, such as the alpha-miner, heuristic miner, and others. However, there has not been enough work comparing the algorithms or linking their performance to the properties of the data.

This talk aims to outline the main algorithms in process discovery. Then, the overall performance of the algorithms will be compared experimentally by using a varied set of artificial data. But the overall performance of the generated models is linked to the data used, thus the talk aims to associate some of the descriptive statistics of the data-sets to the performance of algorithms.

Title: Process Analytics for the Training of Future Doctors
Speaker: Yannan Huang
Abstract: Process Mining is an emerging discipline which is used to deal with process data: event log (the record of execution) and process model. Given the log of future doctor training and the referenced process model, this project is mainly split into two parts: the first part is an analytical methodology and a corresponding report for students and instructors. The second part is an automatic scoring framework for the training process using conformance checking techniques in process mining: Token-based and Alignment Conformance Checking. Besides, the performance of techniques, such as robustness, will be evaluated and compared.

Title: Formalising Minkowski Spacetime
Speaker: Richard Schmoetten
Abstract: My MSc project proposes to formalise an axiomatic system for Minkowski spacetime in the proof assistant Isabelle. I will outline the axioms as originally published by John Schutz in 1997, contrasting them with our current formalisation in Isar. The procedure of de-sugaring and converting a prosaic definition to a workable Isabelle/Isar object is illustrated with an example central to many of the results we are interested in. Using some of our proofs (finished and otherwise) as examples, I will expand on the difficulties I have encountered so far as a novice to automated reasoning.

Title: Building an Interpretable Classifier for Brain Tumour Prediction
Speaker: Colleen Charlton
Abstract: Patients with a brain tumour may present with general non-specific symptoms that vary depending on the location and size of the tumour. Thus diagnosis of a brain tumour is difficult, which is compounded by the rarity of the condition.  My project aims to build an interpretable rule-based machine learning model using a UK dataset that can assess a patient’s likelihood of a brain tumour based on their presenting symptoms.  The final interpretable model may act as a second opinion to assist general practitioners in patient referral and diagnosis.

Title: Applying Process Mining to Healthcare Data for Use with DataLoch
Speaker: Anita Klementiev
Abstract: 

Process mining is a set of techniques for extracting knowledge about processes from timestamped event log data. When applied to hospital information system (HIS) data, process mining can be used to find the most frequently followed patient care paths, investigate differences in care paths followed by different patient groups, analyse compliance with internal and external guidelines, and identify bottlenecks. This talk will give an overview of these different use-cases for process mining, along with a selection of case studies where process mining has been applied to HIS data. Additionally, this talk will cover my applications of process mining using the MIMIC III Intensive Care dataset and the resulting process models. Finally, I will discuss what kind of insights we hope to gain from this experimentation in order to inform meaningful use of process mining with the Edinburgh and South East Scotland data repository known as DataLoch, which is currently under development at the Usher Institute.

Title: Network Motifs - the Building Blocks of Networks
Speaker: Valerio Restocchi
Abstract: Networks are an exceptional way to describe a number of different complex systems, from viruses to social networks. The introduction of network motifs (i.e. small, repeating subgraphs) around 15 years ago, has opened up many new ways to look at the relational information embedded in networks, and started a new field of research. In this talk, I will give an overview of motifs, show some of the many interesting applications, and give some practical information about how to include them in (almost) any kind of research.

Title: The Suboptimal Principle of Optimality
Speaker: Mark Chevallier
Abstract: How proving the principle of optimality, within the context of reinforcement learning, has led to me rewriting how I calculate the Q value of a state-action twice in Isabelle - the original proof, intuitive and easy on paper, is much more difficult formally. I will also discuss my current approach to calculating Q values and how it should make proving the Principle of Optimality easier.

Title: Formal Verification of Reinforcement Learning (Practice Talk)
Speaker: Mark Chevallier
Abstract:

I will discuss my research into formal verification of discrete reinforcement learning, with particular emphasis on the possible benefits of this approach. This 10 minutes talk is intended for an audience familiar with reinforcement learning but perhaps not so familiar with formal verification or theorem proving.