Talks

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.

Title: Hyperduals and Hyperdual Extensions in Isabelle
Speaker: Filip Smola
Abstract:

In my talk, I will discuss new developments in my mechanization of hyperdual numbers in Isabelle, in particular the hyperdual extensions of real functions. I will introduce how limits and derivatives are defined for hyperduals, along with the mechanized proofs of those properties. I will then describe the idea of a hyperdual extension of a real function on the example of sin and cos. I will also describe my current best guess at a general locale for these extensions, along with a number of example instantiations.

Title:  Formal Verification of Reinforcement Learning
Speaker: Mark Chevallier
Abstract:

In this talk, I will introduce reinforcement learning and show my work formally verifying it using Isabelle/HOL. I will show how I have adapted existing models for Markov Decision Processes and modelled rewards, policies, value functions and other reinforcement learning concepts.  I will demonstrate results achieved already showing proofs of the existence of an optimal Q value function under certain conditions and how I intend to use this to show that Q Learning estimates converge to this optimal function over time.

Title: Context-Based Reasoning on Privacy in Internet of Things
Speaker: Nadin Kokciyan
Abstract:

More and more, devices around us are being connected to each other in the realm of Internet of Things (IoT).  Their communication and especially collaboration promises useful services to be provided to end users.  However, the same communication channels pose important privacy concerns to be raised.  It is not clear which information will be shared with whom, for which intents, under which conditions. Existing approaches to privacy advocate policies to be in place to regulate privacy. However, the scale and heterogeneity of the IoT entities make it infeasible to maintain policies among each and every entity in the system.  Conversely, it is best if each entity can reason on the privacy using norms and context autonomously. The proposed approach uses argumentation to enable IoT entities to reason about their context and decide to reveal information based on it.

Title: Data-governance rules modelling and formal notations
Speaker: Rui Zhao
Abstract:
People often focus on data privacy control but forget about the more general rules of data governance. They are pervasive, unavoidable and increasingly complicated with data processing; yet nowadays people seems to be satisfied for manually handling that. My work tries to provide a method to model the governance rules (especially obligations) in a computer-interpretable and actionable way, for the federated data-intensive research context where data will be passed on and processed by different bodies. In this talk, I'll also present an initial mapping to logical notations, and seek advice for logic systems and frameworks to use.

Title: Achieving some explainability in survival models for the healthcare domain.
Speaker:  Jorge Gaete
Abstract:
In this talk I will be presenting my current work on explainable AI in the healthcare domain. I will start from a high level introduction to the topic then move into the work I am currently doing on an existing model and its application to create explainable survival analysis models. This is a presentation on an ongoing research/exploratory work so any feedback will be really appreciated, hope to see you all!

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.