Talks

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.

Title:  Euler the Mathemagician
Speaker: Imogen Morris
Abstract:

I will give a practice talk for the 3 minute thesis competition. This will be a description of my PhD work on formalising Euler's use of the infinitely-small and large, but aimed at an intelligent lay-audience and designed to capture their interest and attention. I will do it as a complete dry-run this time e.g. remaining within 3 minutes and without notes. I would appreciate feedback on my delivery including but not limited to eye-contact, enthusiasm, use of gestures, speed, articulation and movement.

Title:  Explainable AI for the healthcare domain
Speaker: Jorge Gaete
Abstract:

Different machine learning (ML) techniques have been used in the healthcare domain for tasks such as prognosis and diagnostic  of diseases. But as tasks in the medical domain are typically critical, medical staff have the need to understand the ML model and its outcomes. This is a problem since ML techniques are generally black boxes, giving rise to the the topic of Explainable AI. In this first year review talk I will introduce the topic of XAI in the medical domain, some of the main approaches for XAI, and my current work in the topic. I will put special attention to the use of Bayesian methods for XAI. Finally I will present some of the future research directions and a work plan for the next year

Title:  Euler the Mathemagician
Speaker: Imogen Morris
Abstract:

As practice for the 3 minute thesis competition, I will give a description of my thesis in terms accessible to ordinary people, with one slide and aiming for 3 minutes. I will motivate my work on formalising some of Euler's proofs and give a description of infinitely-small and infinitely-large numbers as well as explaining some of the process of formalisation.