Talks

Title: IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL
Speakers: Alex Hyman
Abstract:

We present IsaGrad, a formalisation of scalar reverse automatic differentiation (RAD) over mutable reference-based computational graphs using the Imperative HOL library of Isabelle, and verify its functional correctness by an interactive separation-logic proof. We use IsaGrad as the differentiation engine for two machine learning case studies: training a multi-layer perceptron and a recurrent neural network. Leveraging Isabelle’s code generation, we extract imperative-style Haskell programs where the training process is backed by our verified algorithm. To our knowledge, our implementation is the first of its kind to prove the functional correctness of an imperative, heap-based RAD algorithm. Beyond showcasing Imperative HOL’s expressiveness, this work demonstrates how formal verification increases confidence in computational graphs used for gradient-based optimisation, including neural network training.

Title: GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
Speakers: Mark Chevallier
Abstract:

We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, an optimiser learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent. During the presentation, we will discuss why STL is important for learning functions of continuous time and its limitations. We will also discuss the verification and code generation methods we use to ensure the correctness of the implementation.

Title: Progress towards Algebraic Quantum Field Theory in Isabelle/HOL
Speakers: Richard Schmoetten
Abstract:

Algebraic Quantum Field Theory (AQFT) is a topic in mathematical physics that aims to put the theories underlying modern particle physics on a solid axiomatic footing. This demand for rigour finds its natural continuation in the programme of formalisation of mathematics, gaining computer-checked certainty of correctness. The aim of my work is to conduct an investigation into a formalised theory of AQFT in Isabelle/HOL. Yet much of the mathematical context required for a meaningful definition of AQFT is missing from Isabelle’s libraries. During this talk, I report on progress we have made towards remedying this lack, and present formalisations in the theories of manifolds, Lie groups, and involutive algebras. I will then outline a plan to quickly obtain a minimal formalisation of AQFT, so that the study of theorems with physical interpretation can begin.

Title: Predicting brain health outcomes from objectively-assessed sleep duration in UK Biobank
Speakers: Matthew Whelan
Abstract:

Consistently short or long sleep duration, commonly defined as less than 7 hours or more than 9 hours of sleep, respectively, is implicated in worse outcomes for brain health. This includes increased risk of developing neurodegenerative diseases such as dementia, worse performance in cognitive tests, and smaller brain volume. However, most studies on sleep duration use subjectively reported sleep measures, which are known to match poorly with objective measures. This presentation will present findings for an initial associational analysis using data from UK Biobank. It assesses the feasibility of predicting brain health outcomes from sleep duration derived using accelerometery data.

Title: Investigating associations between physical multimorbidity and subsequent depression via a systematic cluster analysis
Speakers: Lauren DeLong
Abstract:

Multimorbidity, the co-occurrence of two or more conditions within an individual, is a growing challenge for health and care delivery as well as for research Many multimorbidity studies focus upon the co-occurrence of physical health conditions, but mental health disorders are less represented. However, recent studies have revealed links of a bidirectional nature between depression and physical conditions. To investigate associations between physical multimorbidity and subsequent depression, we first performed a clustering analysis upon baseline morbidity data for UK Biobank participants. In contrast to previous similar studies, we compared the usefulness of four independent clustering methods. The identified clusters indicated which physical conditions tend to co-occur most frequently in the whole population and stratified by sex. Finally, we used survival analysis to compare time to subsequent depression diagnosis between participants with particular groups of physical conditions at baseline and those without physical conditions at baseline. In comparison to agglomerative hierarchical clustering, latent class analysis, and k­-medoids, we found that k-modes models showed the best clustering performance amongst several metrics. Notably, the differentially represented conditions within several clusters reflected known bodily systems, such as the respiratory or digestive systems. While we found that certain clusters had stronger associations with depression, we also noted a positive correlation between such associations and the average number of conditions per participant. Therefore, both the type and number of conditions likely influence the subsequent diagnosis of depression. Our findings suggest further investigation into other factors, like social ones, which may link the effects of physical multimorbidity and depression.

Title: Bayesian Multi-view Clustering for Grouping of Patients in Critical Care
Speakers: Luwei (Demi) Wang
Abstract:

The COVID-19 pandemic underscored the need to tailor medical interventions to patient characteristics by identifying at-risk subgroups. While extensive research has explored associations between pre-existing conditions and COVID-19 complications, less attention has been given to the relationship between pre-existing conditions and symptom presentation. Latent Class Analysis (LCA) is commonly employed to investigate this association. However, traditional clustering methods like LCA falter by relying solely on a single data source, amalgamating disparate data streams and potentially compromising outcome accuracy. This approach overlooks individual clinical profiles' distinctiveness. Integrating multiple data sources, such as medical history and acute symptom presentation, offers a more tailored approach. Our study aims to utilize various clustering methods to explore connections between pre-existing condition clusters and symptom clusters while preserving their uniqueness. Multi-view clustering (MVC) techniques, unlike single-view methods, leverage consensus and complementary information to enhance clustering accuracy across multiple data representations. We evaluate different MVC methods—Binary Multi-view Clustering (BMVC), Consensus Graph Learning (CGL), and Bayesian Consensus Clustering (BCC)—against our proposed Bayesian approach. Simulation studies showcase our approach's ability to uncover target clustering structures and its advantage in discovering complementary clusters. Utilizing the ISARIC dataset further elucidates distinct characteristics of these methodologies. In conclusion, the performance of MVC methods varies depending on assumptions and model implementations. Our approach offers fast processing and data-driven insights, uniquely uncovering complementary clusters compared to existing methods.

Title: Predicting long-term incidence of new-onset dementia using primary and secondary care data from Electronic Health Records
Speakers: Konstantin Georgiev
Abstract:

Dementia is a devastating and frequently life-limiting condition, which affects over 90,000 older people in Scotland. While there are no cures available, recent scientific breakthroughs suggest the potential to further slow dementia progression, but these medications are likely to be needed very early in the condition. A recent surge in studies incorporating routine data to predict incidence of dementia has aided in this risk assessment, but a lot of these are selectively biased to include people with pre-existing cognitive impairments and episodes of memory loss. In this longitudinal study, my objective is to provide an inclusive community-level risk assessment, exploring the effects of demographic and lifestyle factors linked with medical and comorbidity history on incidence of dementia. In this talk, I will share some of the key stages of developing and validating a supervised Machine Learning tool for identifying people at risk of new-onset dementia at 5 and 10 years over a large NHS Lothian population. Given the complexity of dementia, this approach is unlikely to provide perfect diagnostic performance at individual-level predictions, but even just identifying groups with substantially higher than average long-term risk can aid in controlling for these risk factors through preventative interventions and drug therapy.

Title: How to set up interventional and/or invasive clinical studies not involving investigational medicinal products in the NHS
Speakers: Fiona Smith
Abstract:

Ever wondered how the anonymised healthcare data sets required for machine learning research come to exist and what approvals are needed before you can start looking at the data and doing the analysis? This talk will give a brief overview of the steps involved in setting up a clinical study in the NHS that does not involve an investigational medicinal product (Non-CTIMPs). It is informed by my experience of setting up a Non-CTIMP that covers more than one NHS health board. Expect an overview of the role of The Academic and Clinical Central Office for Research and Development (ACCORD) in setting up NHS Lothian/University of Edinburgh research projects, the School of Informatics Ethics Approval process, and what is involved in writing project protocols, patient information sheets, patient consent forms, data management plans and securing data sharing agreements.

Title: Mechanising Tensors in Isabelle/HOL
Speakers: Filip Smola
Abstract:

In this talk I will describe our ongoing effort to mechanise tensors - a generalisation of scalars, vectors and matrices - in Isabelle/HOL. This project was started by Matt as part of his master's project and builds on the work of Alexander Bentkamp (at that time of Vrije Universiteit Amsterdam).

I will introduce what tensors are and where they are used. They have found many uses around machine learning in particular, because they are good for expressing structured data and operations on it. Then I will introduce Bentkamp's representation of tensors, highlight some of its drawbacks and show how our approach fixes those. Particularly interesting is the system we use to avoid having to redefine existing operations. Then I will close on some of our plans for to where take this project in the future.