Safeguarded AI
Backed by £59m, Safeguarded AI sits within the Mathematics for Safe AI opportunity space and aims to demonstrate a world where we can use fleets of AI agents to model and verify critical cyber and cyber-physical systems, radically boosting societal resilience.
Select to explore more:
TA1 Tooling
We can build an extendable, interoperable language and platform to maintain formal world models and specifications, and check proof certificates.
Meet the TA1.1 Creators (Theory)
Our TA1.1 Creators will look to unlock novel frontiers for representing different sources of uncertainty, with the ultimate goal of using this semantics to formally model and soundly over approximate a wide range of application domains and safety specifications, against which Safeguarded Al systems will later be verified. The intended output will be a single artefact that is a dissertation-length definition of these languages. With these mathematical representations and formal semantics in place, the programme's other TAs will produce world-models, safety specifications, and proof certificates.
Our TA1.1 Creators have been tasked with defining “syntax” (algebraic construction operators, and version-controllable serialisable data structures), and formal semantics, for language(s) that can be used by teams of humans – and, later, AI systems – to define “world models”, probabilistic specifications, neural network controllers, and proof certificates. These proof certificates present efficiently checkable arguments verifying that a controller composed with a world model satisfies its specification.
In convening this group, we’ve brought together a wide range of relevant expertise in mathematical modelling (across dynamical systems, imprecise probability, category theory, type theory proof theory and more), as well as expertise in domains that will ensure these approaches are commensurable and computationally practical.
Safety: Core representation underlying safeguarded AI
Team Lead: Ohad Kammar, University of Edinburgh
Axiomatic Theories of String Diagrams for Categories of Probabilistic Processes
Fabio Zanasi, University College London
SAINT: Safe AI ageNTs – Formal certification of AI agents in the world
Alessandro Abate, University of Oxford Team
ULTIMATE: Universal Stochastic Modelling, Verification and Synthesis Framework
Radu Calinescu, University of York
Quantitative Predicate Logic as a Foundation for Verified ML
Ekaterina Komendantskaya + Robert Atkey, University of Southampton/Heriot-Watt University; University of Strathclyde
Learning-Theoretic AI Safety
Vanessa Kosoy, Association of Long Term Existence and Resilience (ALTER)
Probabilistic Protocol Specification for Distributed Autonomous Processes
Nobuko Yoshida, University of Oxford
Philosophical Applied Category Theory
David Corfield, Independent Researcher
Double Categorical Systems Theory for Safeguarded AI
David Jaz Myers, Topos Research UK
Monoidal Coalgebraic Metrics
Filippo Bonchi, University of Pisa
Doubly Categorical Systems Logic: A theory of specification languages
Matteo Capucci, Independent Researcher
True Categorical Programming for Composable Systems Total
Jade Master + Zans Mihejevs, Glasgow Lab for AI Verification (GLAIVE)
Unified Automated Reasoning for Randomised Distributed Systems
Alexandra Silva, University College London + Cornell University
Employing Categorical Probability Towards Safe AI
Sam Staton, University of Oxford
Syntax and Semantics for Multimodal Petri Nets
Amar Hadzihasanovic, Tallinn University of Technology
Event Structures as World Models
Alex Kavvos, University of Bristol
Supermartingale Certificates for Temporal Logic
Mirco Giacobbe, University of Birmingham
Hyper-optimised Tensor Contraction for Neural Networks Verification
Stefano Gogioso, Hashberg Ltd
A Computational Mechanics Approach to World Models via Multi-Scale Compositional Abstractions
Fernando Rosas, University of Sussex
String Diagrammatic Probabilistic Logic: Specification and modelling languages
Pawel Sobocinski, Tallinn University of Technology
Profunctors: A unified semantics for safeguarded AI
Nicola Gambino, University of Manchester
Modal Types for Quantitative Analysis of Higher-Order Probabilistic Programs
Vineet Rajani + Dominic Orchard, University of Kent
The projects we have funded were selected from teams and individuals who applied to our previous funding calls for this programme. You can read more about these archived calls below.
The Creator experience
What you can expect as an ARIA R&D creator.
Applicant guidance
Discover the process of applying for ARIA funding and find key resources.