Talks

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: 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: Explaining machine answers to human questions
Speaker: Jorge Gaete-Villegas
Abstract:
The field of artificial intelligence has accomplished much in recent years and every day its applications are 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: Uncertain events and Business Process Management
Speaker: Jiawei Zheng
Abstract:
Deviations are ubiquitous in our world, such as machine malfunction in the context of manufacturing and falling over in daily life. How to detect these deviations and provide effective interventions such as robot support when people fall to avoid further adverse effects is the main objective of my research.

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

Title: Preparing for the AIML 3 minute thesis competition
Speaker: Imogen Morris
Abstract: 

We are planning to hold a 3 minute thesis competition within the AIML lab (just like the one the University has each year, https://www.ed.ac.uk/institute-academic-development/postgraduate/doctoral/3mt/about-3mt). In brief: you have 3 minutes and 1 slide to present your thesis at an accessible level. On Friday I will give a brief description of the competition. We will look at some example 3 minute thesis presentationsand discuss what worked well and what did not. We will then have a mini-workshop to help each other come up with ideas for our presentations.

Title: Impact of multimorbidity profiles om mortality rates and sepsis: A network approach
Speaker: Jorge Gaete Villegas
Abstract: 

In this talk I will present the use of the Stochastic Block Model (SBM) as an alternative to clustering techniques to study the impact of multimorbidity on in-hospital sepsis and mortality. The SBM is an approach to community detection that can be used instead of classic clustering techniques such as k-means or Latent Class Analysis (LCA) to identify groups of patients. Since the SBM is a nonparametrical method and makes no assumptions about the features distribution, its application overcomes some of the known limitations of other clustering algorithms. As an added benefit, the SBM provides clusters at different resolutions in a hierarchical structure with potential uses to increase explainability of the results.

Title: Adverse Drug Reaction Prediction via Network Representation Learning and Multimodal Embedding
Speaker: Lauren DeLong
Abstract: 

Novel drugs often fail in late-stage clinical trials due to unforeseen adverse side effects which deem them unsafe for distribution. Many computational approaches have aimed to address this issue, but few have attempted to use Network Representation Learning (NRL) algorithms. Some previous approaches take advantage of the concept that similar chemical composition between drugs, should, in turn, indicate similar biochemical function and therefore similar side effects. However, this principle is shown to be violated frequently in clinical practice, such as in the case of Procaine and Procainamide, a local anesthetic and an antiarrhythmic, respectively. In contrast, newer approaches show improved performance with an increased variety of biomedical information. The complex landscape of interactions between drugs, targets, protein-protein interactions and adverse drug reactions (ADRs) can be modeled as a large heterogeneous graph in which nodes represent proteins, drugs, or ADRs, and edges which exist between these varieties of nodes indicate some sort of interaction, such as that a certain drug is associated with a side effect. Network topological measures can provide insight into which drugs are more likely to result in adverse events than others. However, in the context of drug development it is essential to de-risk targets and compounds as early as possible. Hence, it is important to predict adverse events for compounds and unwanted phenotypes for targets. These two problems can be formulated as link prediction tasks in the heterogeneous graph. Technically, this can be addressed via NRL, where an encoder is used to find low dimensional node embeddings and a corresponding decoder is used to assign likelihoods to each of the possible edges in the network. In this work, the Relational Graph Attention Network is extended to operate on multimodal biological input and compared alongside previously established side effect prediction methods to evaluate the efficacy of deep NRL for side effect prediction.

Title: Verified Optimisation in Lean
Speaker: Ramon Mir Fernandez
Abstract: 
Convex optimisation is a subfield of mathematics that studies convex functions and their maxima/minima over a given domain. It has applications in control synthesis, signal processing and operations research to mention a few. One issue is that reducing these problems to convex optimisation problems is not straightforward and error-prone. Moreover, the approximate nature of the algorithms used by the solvers can make the result unreliable. For these reasons, it would be highly desirable to use a formal tool alongside these solvers to rigorously check every step and certify the final result. We will delve into how the tools can be linked and discuss some work in progress. The formal tool chosen for this project is Lean, a theorem prover and programming language developed at Microsoft Research. We will explain some of its main features and talk about how it differs from other systems such as Coq or Isabelle. Finally, we will explore neural network verification as a potential case study.

Title: Mechanising Process Composition
Speaker: Filip Smola
Abstract: 
In this talk I will give an overview of progress made on my PhD project and the future plans. The project is centred on processes specified by input and output resource, and their composition. I will give a brief overview of processes and resources, as well as their mechanisation. I will then present four process models we have built that demonstrate some of the features our mechanisation can already express, such as located resources and sensing actions. Then I will go over how we relate the process compositions to proofs in linear logic, giving them a notion of correctness. Finally I will sum up the plans for the future of this project.

Title: A Formalisation of Markov Decision Processes
Speaker: Mark Chevallier
Abstract: 

In this talk I will discuss my formalisation of Markov Decision Processes. I will talk about the formalised model, formal proofs of value convergence and of the existence of an optimal policy by vector representation of functions on the states. My approach was based on Martin Puterman's proof, and in the process of formalisation I found a small flaw in it, which was addressed and fixed.

Title: Mapping and Reapplying Mathematical Knowledge
Speaker: James Vaughan
Abstract: 

There has been little research into the structure present in the litany of formal mathematics generated with interactive theorem provers. Network theory gives us tools to model the dynamics of complex systems, of which formal mathematics undoubtedly qualifies as an instance. I will discuss what we have done in the past year to apply these tools to improve the capabilities of interactive theorem provers. I will also present the plans for the remainder of my PhD.

Title: Tree Search using Human Expert’s Knowledge
Speaker: Mustafa Faisal Abdelwahed
Abstract: 

For a while, tree search algorithms have been used in solving challenging problems like planning problems and combinatorial optimization search. Researchers tend to encode their search parameters or knowledge into objective functions, which receives a state then generates a number to represent how satisfying this state is concerning built-in constraints or a targeted solution configuration while pruning branches with no possible potential. However, they ignored a vital point: transformation/encoding causes information loss, leading to degrading the solution quality and may result in more computational costs. Hence, in the upcoming presentation, we shall explore how we can augment the human experience directly with tree search without encoding them into objective functions.

Title: Using causal inference to evaluate the efficacy of medicinal treatments from observational data
Speaker: Callum Abbott
Abstract: 

Whether we're talking about COVID vaccines, antibiotics, or painkillers; the efficacy of medicinal treatments has been traditionally tested using the gold-standard Randomized Control Trial (RCT). However, conducting RCTs can often be unfeasible due to ethical, logistical or financial concerns. For instance, what if we needed to know the efficacy of a surgical procedure in treating a fatal neurological condition? We cannot afford to send the control group to their inevitable doom. Hence, in this study, we look to apply causal inference techniques to purely observational data to investigate the effectiveness of subdural drainage in preventing the recurrence of chronic subdural hematoma.