Talks

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.

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.