Safeguarded AI Meeting

This week, 50 category theorists and software engineers working on “safeguarded AI” are meeting in Bristol. They’re being funded by £59 million from ARIA, the UK’s Advanced Research and Invention Agency.

The basic idea is to develop a mathematical box that can contain a powerful genie. More precisely:

“By combining scientific world models and mathematical proofs we will aim to construct a ‘gatekeeper’, an AI system tasked with understanding and reducing the risks of other AI agents. In doing so we’ll develop quantitative safety guarantees for AI in the way we have come to expect for nuclear power and passenger aviation.”

This program director is David Dalrymple, and you can get a much better description of the project from him in the first 4 minutes here:

It’s remarkable how many of the applied category theorists in the UK are involved in this:

• Category theorists in AI

If you’re wondering “why category theory?”, I think the idea is this: software based on general abstract math is more flexible, yet also easier to formally verify.

For example the Topos Institute, run by my former student Brendan Fong, now has a branch in the UK largely funded by ARIA. At the meeting, Topos is demonstrating how to build models in CatColab, their new category-based software.

I am not part of this project, though some of my math is getting used here. I prefer to avoid doing things connected to AI. I have no idea how successful this “safeguarded AI” project will be, so I’m watching with fascination and profoundly mixed emotions.