Skip to content

Talks

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.

              Formalising the correct termination, fairness, and tractability of Meek’s method of STV in Isabelle/HOL

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

                Title: Formalising the correct termination, fairness, and tractability of Meek's method of STV in Isabelle/HOL
                Speaker: Jake Palmer
                Abstract:

                I will present my work on formalising various properties of Meek's method of STV. So far I have represented and proved the quantities, assumptions, and theorems in the paper "Algorithm 123: Single transferable vote by Meek's method", wherein they provide a proof that when some number of candidates are elected at some stage of the process, they remain elected and their votes converge on the quota (i.e. what a candidate needs to be elected) and this converged-to state is unique. I will briefly present some ideas on a more complete proof of correct termination which takes into account filling seats, and some ideas on how to go beyond that to making the notions of fairness and "wasted votes" in Meek rigorous and formally proving they are satisfied by the method. Finally, I will finish off the work by proving the tractability of the method in terms of its time complexity, and extract the verified algorithm.

                L’Hopital’s Theorems and Euler’s Notions of Orders of Infinity in Isabelle/HOL

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

                  Title: L'Hopital's Theorems and Euler's Notions of Orders of Infinity in Isabelle/HOL
                  Speaker: Kyriakos Katsamaktsis
                  Abstract:
                  In his paper on "Orders of Infinity" Euler writes, without rigorous proofs, about "infinitely large" and "infinitely small" quantities and how they relate to one another. For example, he writes that if x is infinite, then its logarithm is also infinite, and the ratio of the logarithm of x divided by x is infinitely small. Such statements can be put on a rigorous footing using nonstandard analysis, which treats infinity as a number (or more than one) without using limits. We will describe the formalisation of parts of Euler's paper in Isabelle using nonstandard analysis. We will shed light on a few vague statements and show how fairly standard modern mathematics plus some nonstandard analysis can resolve them.

                  Hybrid Process Mining

                    Date: 5th July 2019
                    Time: 14:00 - 16:00

                    Title: Hybrid Process Mining: Combining Imperative & Declarative Paradigms
                    Speaker: Christoffer Olling Back (PhD Fellow, Department of Computer Science, University of Copenhagen)
                    Abstract:

                    Modern organisations generate enormous amounts of data related to their business processes via IT systems such as Enterprise Resource Planning (ERP) systems. Mining process related data presents the opportunity for a truly data-driven approach to streamlining operations and building an intelligent enterprise. Depending on the use case, process mining may be employed with the aim of detecting deviations from a well-defined process, identifying areas for process enhancement (detecting bottlenecks, unnecessary rework), and in the case of pure process discovery – where the underlying process is not known – the task essentially becomes comparable to unsupervised learning.

                    In this talk, I will begin with a brief introduction to process mining generally, positioning the field in relation to data mining and machine learning. Afterwards, I will discuss different process modelling paradigms in more detail, and their strengths and weaknesses. In particular, the distinction between declarative (constraint-based) and imperative (flow-based) languages, and how they can be combined to form hybrid process models which combine the strengths of both. Time permitting, I will discuss my ongoing work on developing process mining algorithms which generate hybrid models by identifying pockets of regularity using an information theoretic approach, as well as challenges in empirically evaluating process mining algorithms.

                    Predicting graft and patient survival following liver transplantation

                      Date: 28th June 2019
                      Time: 14:00 - 16:00

                      Title: Predicting graft and patient survival following liver transplantation
                      Speaker: Simon Thorogood
                      Abstract:
                      I'll aim to cover a bit of the medical background (Why do people need liver transplants? What are the challenges when allocating livers?). I'll also talk about the NHSBT dataset I am using and some of the traditional statistical approaches to survival prediction (specifically, the field of Survival Analysis). Finally I'll discuss some of the machine learning approaches that I will be applying to the problem.