Talks

Title: Improving the explainability of machine learning techniques in the healthcare domain
Speaker: Jorge Gaete Villegas
Abstract:

The critical nature of medical tasks makes explainability an essential quality for any support system in healthcare. Despite various techniques to provide explainable ML models, challenges still exist. Issues such as model selection, interpretation of results or user interaction with the models are important areas of research to achieve more understandable models and improve their adoption. In this talk, I will present our approach to tackle some of these issues, our current work and its application to patients in the Intensive Care Unit and plans for the rest of my PhD. Special attention will be paid to the use of community detection as an alternative to traditional clustering, and to the potential of leveraging our current results by using Probabilistic Logic Programming to create explainable predictive models.

Title: Understanding Processes
Speaker: Filip Smola
Abstract:

In this talk I will give a high-level overview of my work on mechanising linear resources and process models. I will focus on what we can express and do with these models rather than how the mechanisation is set up. This includes how we can use specific kinds of resources and basic actions to express different domains, as well as tools for formally relating such domains. The simpler applications I will demonstrate are built around automatically deriving information about complex compositions of processes in domains inspired by two simulation games. For more interesting applications I'll go over how process compositions relate to event sequences. And to conclude I'll highlight two pieces of work currently in progress: expressing distributions in non-deterministic resources and a labelled process transition system.

Title: Challenges in predicting rehabilitation requirements for older patients
Speaker: Konstantin Georgiev
Abstract:
An ageing population is a major success of modern healthcare, but this challenges the NHS to better support increasingly frail hospitalisations. One third of older people acquire a new disability by discharge, leaving hospital with less independence than before getting ill. Rehabilitation attempts to maximise recovery, but this is not well targeted to people at the highest risk of disability, as the true contributing factors are poorly understood. However, electronic health records now routinely hold information about rehabilitation progress. This brings forward a new opportunity to utilise this data and build structured care pathways using Machine Learning, Process Mining and Explainable AI tools.

In this talk, I will give an introduction to the current challenges in rehab, particularly the complexity in deciding the duration, intensity and type of treatment for frail and multimorbid patients. We will also briefly look at one case study involving rehab patterns for patients recovering from COVID-19.

Title: Neurosymbolic AI for Reasoning on Graph Structures
Speaker: Lauren DeLong
Abstract:
In this short talk, I'll present my idea for a survey paper on using neurosymbolic methods for reasoning on graph structures. Neurosymbolic methods are increasing in popularity as they combine the scalability and performance of neural network-based methods with the interpretability of symbolic methods. Subsequently, recent works have attempted to extend and apply the ideas of neurosymbolic methods to reasoning on graph structures, often for the purpose of knowledge graph completion. I will explain the ideas and motivation behind these methods, the categories to which I have classified the respective papers, and the general structure of the paper which I plan to write. I would appreciate any feedback and suggestions you might have. Additionally, if any particular sections stand out as interesting to anyone, I welcome volunteers to help co-author the paper.

Title: You can survive the maze of death
Speaker: Mark Chevallier
Abstract:
Every turn you take in the maze of death might lead to fortune or disaster. And you don't know which way to go! But we can prove, beyond any doubt, that by following some simple rules, you will be able to learn the absolute best way to navigate the maze. Want to know the rules? Better listen to the talk.

Title: Proactive Side Effect Prediction: Using AI to Race Against Time
Speaker: Lauren DeLong
Abstract:
Imagine going to the doctor to treat an eye infection, then ending up with itchy hives, or going for pain relief, but now your medicine causes stomach cramps! Such side effects can upset patients, dampen trust in doctors, and cost medical companies loads of money. To predict these side effects before they happen, we used network prediction methods, similar to those which generate friend recommendations for you on social media. Novel predictions can help to identify harmful side effects before a patient like you might experience them.

Title: Prove that your car won't crash
Speaker: Ramon Fernández-Mir
Abstract:
In this talk, we explain how you can convince your computer (and yourself) that an autonomous system will behave safely.

Title:  Explaining machine answers to human questions.
Speaker: Jorge Gaete Villegas
Abstract:
The field of artificial intelligence has accomplished much in recent years and its applications are everyday more embedded into our daily life. But can we really trust these systems and their predictions? Are we willing to put in the hands of a machine things like the healthcare of our loved ones? In this talk I explain our quest to provide a bridge between AI and decision makers via explanations.

Title: Human Action Recognition
Speaker: Zonglin Ji
Abstract:
Recognising human actions from a video has been considered a challenging task as it requires identifications of both spatial and temporal features to consider. In this project, I have built a classification model using deep learning that can distinguish and classify 100 plus different actions in daily life from a human skeleton-based dataset.

Title: Euler the Mathemagician
Speaker: Imogen Morris
Abstract:
Euler was infamous for using 'impossible' numbers that are smaller than any other number, yet bigger than zero, and using his almost magical intuition to arrive at the right answer, like a magician pulling a rabbit out of a hat. Using a proof-assistant, and a modern theory of infinitely-small numbers, I aim to show the real magic was in Euler's reasoning.

Title: Trusting the Transfer: From Scotland to the Antipodes
Speaker: Jake Palmer
Abstract:
Single Transferable Vote (STV) is a family of algorithms for counting ranked ballots in multi-winner elections, typically carried out by hand. We verify using a general characterisation of STV that, regardless of the existing or not-yet-existing variant used, it is correct and terminates. This extends to covering Meek's method of STV -- a computer-counting variant that relies on the convergence of a vector under iteration of a specific function -- used in several places including some elections in New Zealand.

Title: The silent epidemic: Role of networks in tobacco control.
Speaker: Adarsh Prabhakaran
Abstract:
Smoking behaviour can spread in a population through social ties. We are trying to model the spread of smoking and develop strategies to control the spread using an Agent-based model on a network.

Title: Foundations for Physics
Speaker: Richard Schmoetten
Abstract:
The physical theories describing the subatomic world have been experimentally verified to famously high degrees of accuracy. Yet conceptual problems remain: in fact, it is doubtful that the standard formulation of these theories is entirely well-defined. I aim to study one candidate remedy to these troubles, the Haag-Kastler axioms, and investigate well-founded models of reality with the help of a proof assistant.

Title: Flowing Resources
Speaker: Filip Smola
Abstract:
Resources are important to the activities we all do. We can use them to talk about what we are working with or what we are working towards. And then we can look at whole processes of activities and see how these resources flow through them. I am working to make a computer understand what we mean by these resources, so that together we can better understand the processes they control.

Title: Here be Dragons - Navigating Formal Mathematics with Knowledge Graphs
Speaker: James Vaughan
Abstract:
Unfortunately, the formal mathematics contained within interactive theorem provers is a world of its own. Although there is definite correspondence between these digitised theories and their pen-and-paper counterparts, it is not obvious to simple machines. Using knowledge graphs, we may bring back the human context to formal proofs for the benefit of both mathematicians and machines.

Title: Lagrangian Mechanics in Isabelle/HOL
Speaker: Dawson Silkenat
Abstract: 

Mechanics is an incredibly important branch of physics which describes motion of and interaction between particles in a system. It is widely applied in engineering fields and has a large historic role in our understanding of how the universe works. In my project I seek to provide a framework for formally proving properties of a system using the Lagrangian formulation of mechanics and a proof assistant.

Title: Practical Ethics and the Need for Interpretability in Biomedical AI
Speaker: Lauren DeLong
Abstract: 

I plan to submit a short essay on the need for​ interpretability in biomedical AI to the Oxford Uehiro Prize in Practical Ethics essay competition. Practical Ethics is the dialog and debate between three major facets of ethics: egoism, which is the belief that one acts in self-interest, consequentialism, in which one acts to maximize benefit for society in the future, and deontology, in which right or wrong is determined by rules beyond self-interest or societal benefit. Specifically, I use these three facets to discuss ethical dilemmas in using black-box vs. interpretable models for healthcare and medicine. I imagine this will be a 10-15 minute presentation, and I would greatly appreciate any feedback from the group regarding counterarguments, rebuttals, or important ideas which I failed to cover.

Title: Increasing User Engagement on the Archive of Formal Proofs
Speaker: Carlin Mackenzie
Abstract: 

The first part of this project focused on creating a strong foundation for future development on the Archive of Formal Proofs. We now add features which encourage community growth. For example, the addition of comments allows people to discuss entries and user profiles allow people to both express themselves and see statistics about their entries. Our next steps are to evaluate our additional features with users of the AFP.