Safeguarded AI: TA1.1 R&D Creators

Building on an existing body of work, cognate literature and the certification of AI agents via “neural synthesis”, Alessandro and his team will look to advance beyond the synthesis of model-based certificates that are either Boolean or have specific probabilistic forms; move beyond the adherence by a single model of the AI agent or its environment; and to advance beyond the restrictive assumption of single, fixed specifications. The project will bridge between the use of SAT solvers and statistical approaches such as PAC.

Radu + his team plan to develop a universal framework for the compositional definition, verification and synthesis of stochastic world models. When realised, this universal framework will support the modelling of probabilistic and nondeterministic uncertainty, discrete and continuous time, partial observability, and the use of both Bayesian and frequentist inference to exploit domain knowledge and data about the modelled context.

This project aims to develop a unifying logical framework, Quantitative Predicate Logic (QPL), to provide the connection between specifications of low-level machine learning components and cyber-physical system specifications (CPS spec). The current state of saturation and fragmentation of the literature that concerns specification, verification, and spec-driven training of ML models suggests that a novel umbrella “foundation for verified ML” that unifies mathematical concepts coming from Empirical Risk Minimisation (ERM), Formal Verification, and Quantitative Reasoning is urgently needed. Ekaterina + Robert plan to define and establish such a unifying framework.

The project aims to develop formal, theoretical foundations that ensure the safe and reliable functioning of AI systems, particularly those that may reach or surpass human-level intelligence. This includes but is not limited to developing mathematically rigorous theories concerning ambiguous online learning (i.e. online learning with partially-specified hypotheses) and infra-bayesian regret bounds.

Cyber-physical AI systems – which are often composed of concurrent autonomous components communicating via networks – are frequently unsafe, unreliable and non-robust. Nobuko and her team plan to develop a new theory of Probabilistic Session Types (ProST), which provides a formal interpretation using Probabilistic Petri Nets. ProST will provide correctness by construction, ensuring that each component follows a specified protocol during communication, enhancing the safety and reliability of these systems under uncertain conditions.

This project plans to overcome the limitations of traditional philosophical formalisms by integrating interdisciplinary knowledge through applied category theory. In collaboration with other TA1.1 Creators, David will explore graded modal logic, type theory, and causality, and look to develop the conceptual tools to support the broader Safeguarded AI programme.

This project aims to utilise Double Categorical Systems Theory (DCST) as a mathematical framework to facilitate collaboration between stakeholders, domain experts, and computer aides in co-designing an explainable and auditable model of an autonomous AI system’s deployment environment. David + team will expand this modelling framework to incorporate formal verification of the system’s safety and reliability, study the verification of model-surrogacy of hybrid discrete-continuous systems, and develop serialisable data formats for representing and operating on models, all with the goal of preparing the DCST framework for broader adoption across the Safeguarded AI Programme.

Filippo and team intend to establish a robust mathematical framework that extends beyond the metrics expressible in quantitative algebraic theories and coalgebras over metric spaces. By shifting from Cartesian to a monoidal setting, this group will examine these metrics using algebraic contexts (to enhance syntax foundations) and coalgebraic contexts provide robust quantitative semantics and effective techniques for establishing quantitative bounds on black-box behaviours), ultimately advancing the scope of quantitative reasoning in these domains.

This project aims to develop a logical framework to classify and interoperate various logical systems created to reason about complex systems and their behaviours, guided by Doubly Categorical Systems Theory (DCST). Matteo’s goal is to study the link between the compositional and morphological structure of systems and their behaviour, specifically in the way logic pertaining these two components works, accounting for both dynamic and temporal features. Such a path will combine categorical approaches to both logic and systems theory.

This project intends to develop a type theory for categorical programming that enables encoding of key mathematical structures not currently supported by existing languages. These structures include functors, universal properties, Kan extensions, lax (co)limits, and Grothendieck constructions. Jade + team are aiming to create a type theory that accurately translates categorical concepts into code without compromise, and then deploy this framework to develop critical theorems related to the mathematical foundations of Safeguarded AI.

This project will look to extend Outcome Logic, a framework that captures correctness and incorrectness properties in programmes with effects, to handle randomisation and concurrency. Orthogonally, it will also look at string diagrammatic reasoning on probabilistic programs. By providing probabilistic descriptions of system behaviours and supporting compositional reasoning, the team will look to allow for scalable reasoning for complex systems.

Sam + team will look to employ categorical probability toward key elements essential for world modelling in the Safeguarded AI Programme. They will investigate imprecise probability (which provides bounds on probabilities of unsafe behaviour), and stochastic dynamical systems for world modelling, and then look to create a robust foundation of semantic version control to support the above elements.

Amar + team will develop a combinatorial and diagrammatic syntax, along with categorical semantics, for multimodal Petri Nets. These Nets will model dynamical systems that undergo mode or phase transitions, altering their possible places, events, and interactions. Their goal is to create a category-theoretic framework for mathematical modelling and safe-by-design specification of dynamical systems and process theories which exhibit multiple modes of operation.

This project aims to advance the theory of Two-dimensional Kripke Semantics (2DKS), which enhances traditional Kripke semantics by incorporating ‘evidence’ in state changes, aligned with an “information order” on states. Alex will look to create expressive logics and frameworks for modelling state-based computational systems that will also function as proof-relevant certificates to reasoning over systems with modal logic. 

The project aims to create a new theory of ‘supermartingale proof certificates’ for temporal logic specifications and ω-regular languages, with formal probabilistic guarantees. The theory will enable the development of learnable and efficiently checkable certificates for probabilistic systems that will extend and generalise all existing supermartingale certificates to date.

The project aims to develop ‘hyper-optimised tensor network contraction’ algorithms specifically optimised to reason about hybrid theories. These new algorithms will combine quantum simulation and automated reasoning technologies to push the boundaries in the compositional analysis of complex systems that integrate stochastic dynamics, hybrid software/cyber-physical systems and neural networks.

This project aims to develop a theoretical framework to optimise the design and analysis of AI world models. By identifying key variables and appropriate levels of granularity, Fernando will look to enable accurate simulations with minimal computational load. By introducing notions of  ‘effective’ and ‘leaky abstractions,’ the framework will ensure optimal simulation of AI behaviours while balancing accuracy and efficiency. Beyond this, the project will look to set a new paradigm for world model analysis and design by improving existing world models, uncovering their compositional structure, and creating new ones.

This project aims to combine advances in probabilistic modelling (Markov categories) with string diagrammatic logic (cartesian bicategories) to develop expressive graphical specification languages for probabilistic applications. Pawel’s team brings together experts from both fields to enhance string diagrams for probabilistic contexts, integrate them with first-order logic, and address the complexity of specifications.

This project aims to investigate the mathematical notion of a profunctor, which provides a unified and efficient concept for studying formal theories. It will explore open problems related to the category-theoretic structure of profunctors and related notions, such as symmetric sequences and symmetric multicategories. Key questions focus on tensor product for bimodules between symmetric multicategories and the differential operation for analytic functors. This will build on Nicola + team’s previous work.

This project aims to develop a compositional framework for specifying and reasoning about quantitative safety properties in machine learning, where algorithms often use randomness to make decisions under uncertainty. By building a graded modal type theory for a higher-order probabilistic programming language, Vineet + team will look to enable engineers to enforce cost optimality bounds on machine learning models directly through type checking.