Skip to content

Talks

A New Web Interface for the Archive of Formal Proofs

    Date: 28th February 2020
    Time: 14:00 - 16:00

    Title: A New Web Interface for the Archive of Formal Proofs
    Speaker: Jaydn Goodwin
    Abstract:

    I will be presenting my developments on a new implementation of the Archive of Formal Proofs. I'll be highlighting the key features of the current interface that have been replicated as well as new features that have been added. I will also be discussing my design decisions, and methods I will use to evaluate the project.

    Explainable AI for the healthcare domain

      Date: 28th February 2020
      Time: 14:00 - 16:00

      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

      Euler the Mathemagician

        Date: 28th February 2020
        Time: 14:00 - 16:00

        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.

        Hyperduals and Hyperdual Extensions in Isabelle

          Date: 14th February 2020
          Time: 14:00 - 16:00

          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.

          Formal Verification of Reinforcement Learning

            Date: 31st January 2020
            Time: 14:00 - 16:00

            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.

            Context-Based Reasoning on Privacy in Internet of Things

              Date: 8th November 2019
              Time: 14:00 - 16:00

              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.

              Data-governance rules modelling and formal notations

                Date: 25th October 2019
                Time: 14:00 - 16:00

                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.

                Achieving some explainability in survival models for the healthcare domain

                  Date: 11th October 2019
                  Time: 14:00 - 16:00

                  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!

                  Formal Verification for Reinforcement Learning

                    Date: 27th September 2019
                    Time: 14:00 - 16:00

                    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.

                    Mechanising Euler’s Infinite Analysis in the Proof Assistant Isabelle

                      Date: 27th September 2019
                      Time: 14:00 - 16:00

                      Title: Mechanising Euler's Infinite Analysis in the Proof Assistant Isabelle
                      Speaker: Imogen Morris
                      Abstract:

                      I will describe my work this year on formalising Euler's proof of the Basel problem . The proof which I have partially formalised is from Euler's textbook `Introduction to the Analysis of the Infinite', in which he aims to show that the manipulation of infinitely small and infinitely large quantities can be accomplished using `ordinary algebra'. Euler's arguments using infinity and his theory of infinitesimals are not considered rigorous by present-day mathematicians. However, there is a modern theory of infinities and infinitesimals called nonstandard analysis, which captures many of the properties that 18th century mathematicians ascribed to infinite and infinitesimal numbers. I use this theory and the proof assistant Isabelle, as the framework to mechanise Euler's proof. My project aims to demonstrate that Euler's reasoning can be made consistent and that Euler appreciated the subtleties of infinitesimals. In my talk, I will also outline my plans for further research which include other arguments from Euler's textbook e.g. the infinite product for sine in terms of its roots and generalisations of the Basel problem.