Verified Neural Network Training for Safe Human-Robot Interaction
Robotic movement in the home and other human-centred environments requires safe, constrained behaviour. Neural networks are powerful tools that can be used for low-level perception in such settings but whether they subsequently implement the intended behaviour is usually difficult to assert, let alone guarantee.
We wish for the assurance that a neural network can be taught constraints such as “never go past this threshold” or “avoid this region until it is clear” and actually obey them as intended when deployed e.g. in a robotic assistant.
To this end, we propose a neurosymbolic AI approach that tightly integrates rigorous logical reasoning and learning to formally constrain the training of neural networks. We will build a theorem-proving framework that allows for formal representation and proofs, and then faithful code-generation, of user-specified, spatio-temporal constraints that can then be used for learning in scenarios involving human-robot interaction.
Our ultimate aim is to provide a machine-certified, neurosymbolic approach that ensures safe robotics in complex human-centred environments.
Are you interested in doing a PhD or in collaborating with us on this topic (or other neurosymbolic AI ones)? Get in touch!
Artificial Intelligence and Multimorbidity: Clustering in Individuals, Space and Clinical Context (AIM-CISC)
AIM-CISC is a three-year research programme looking into multiple long-term health conditions (MLTCs) in the UK using a range of AI techniques. As the population grows and people are living longer, the impact of MLTCs on both the population and the health and care system intensifies.
This project aims to produce a detailed picture of MLTCs in the United Kingdom – how they present in individuals and through families, the influence that place and community has on MLTCs, and how people with MLTCs are treated by the health services. The results of this research can be used to inform future strategies in dealing with this issue.
Are you interested in doing a PhD or in collaborating with us on this topic (or more generally in AI for healthcare/medicine)? Get in touch!
Funder: National Institute for Health and Care Research (NIHR).
Total Funding: £3.9m.
Formal modelling of process workflows (and more)
Work on the development and application of the WorkflowFM framework is ongoing. This encompasses areas such as healthcare and manufacturing (e.g. as part of the Digiflow project).
Past and ongoing projects include (amongst others) the modelling of integrated care pathways (ICPs) for HIV (in association with NHS Lothian and NHS Greater Glasgow & Clyde), developing rigorous models for the treatment of burns (in collaboration with the Glasgow Royal Infirmary) and modelling the processes underlying patient transfers in hospitals (in collaboration with St Mary’s Hospital, London). More information is available on WorkflowFM.org.
Our domain- agnostic approach and technology is based on a correct-by-construction approach. It enables the development of high-level process models and workflows that can be faithfully deployed as software through automatic code-generation. The workflows can be integrated with data, e.g. coming from IoT devices, and monitored through our custom-built dashboard.
DIGIFLOW
Digitizing Industrial Workflow, Monitoring and Optimization
The WorkflowFM team (Smola, Vaughan, Papapanagiotou and Fleuriot) is working on the transfer of its formal-methods based technology to a real-world context involving the modelling and deployment of industrial workflows tracking shopfloor assets and workforce.
Funder: EIT Digital
Partners: FBK CREATE-NET, Reply, ThinkINside.
Total Funding: 500K EUR (2018) + 550K EUR (2019)
AI4T: AI FOR TRANSPLANTATION
Predictive AI modelling for liver transplantation
Project on predicting graft and patient survival following liver transplantation is currently underway. We’re working with a large dataset obtained from the National Health Service Blood & Transplant (NHSBT).
This work has so far resulted in a Poster of Distinction Prize at the Association of Surgeons in Training International Surgical Conference 2019 and in a best dissertation prize for an MSc in Data Science (2019) for Simon Thorogood’s work on “Predicting transplant and patient survival following liver transplantation using machine learning”.
Collaborators: Oxford University NHS Trusts.
AI-BASED SURVIVAL ANALYSIS
Modelling brain tumour survival using machine learning
This project investigates survival of patients with brain cancer using a specially curated dataset that includes genetic tests, tumour characteristics, demographic, clinical and treatment information .
This work has so far resulted in a MSc thesis titled “Investigating Brain Cancer Survival with Machine Learning” for Callum Biggs O’May. In this thesis, one of the oustanding MSc projects of 2019, machine learning techniques are used to interrogate the clinical consensus on how the above-mentioned factors influence one another and which are important for survival.
Collaborator: Paul Brennan, Senior Clinical Lecturer and Honorary Consultant Neurosurgeon at the University of Edinburgh and NHS Lothian.
RECONSTRUCTING EULER
Mechanizing Euler’s infinitesimal and infinite reasonning in Isabelle/HOL
Several projects on the formal reconstruction of Euler’s proofs involving infinitesimal and infinite reasoning using Nonstandard Analysis are currently underway in the theorem prover Isabelle.
Sources include Euler‘s famous Introductio in analysin infinitorum (Introduction to the Analysis of the Infinite), first published in 1748, and his Institutiones calculi differentialis (Foundations of Differential Calculus), first published in 1752.
Aside from a PhD research project by Imogen Morris, this work has led to two undergraduate final year projects, including a winner of the dissertation prize in Mathematics by Kyriakos Katsamaktsis for his work on Euler’s notions of orders of Infinity in Isabelle/HOL, and one outstanding MSc project (2019) by Jessika Rockel for her work on “Exploring Euler’s Foundations of Differential Calculus in Isabelle/HOLusing Nonstandard Analysis”.
AI FOR THEOREM PROVING
Intelligent theorem proving
We are working on predictive modelling and new visualisation techniques to support work with proof assistants. These include intelligent exploration of proof libraries, proof analytics and predictive help during proof. This work incorporates and extends the technology from the ProofPeer project on collaborative theorem proving.