Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems

TL;DR

This paper defines guaranteed safe (GS) AI as a safety paradigm that seeks high-assurance quantitative guarantees for AI behaviour via a triad of components: a world model, a safety specification, and a verifier. It surveys the limitations of empirical safety assessments and outlines a spectrum of approaches for building GS AI, from manual or probabilistic world models to formal verification and runtime assurance. Concrete GS AI solutions are illustrated across domains such as code translation, autonomous driving, robotics, healthcare, and climate applications, demonstrating how safety specifications and verifiers interact with world models. The authors argue that GS AI can provide auditable, scalable safety guarantees and should complement existing safety methods within a diversified research portfolio.

Abstract

Ensuring that AI systems reliably and robustly avoid harmful or dangerous behaviours is a crucial challenge, especially for AI systems with a high degree of autonomy and general intelligence, or systems used in safety-critical contexts. In this paper, we will introduce and define a family of approaches to AI safety, which we will refer to as guaranteed safe (GS) AI. The core feature of these approaches is that they aim to produce AI systems which are equipped with high-assurance quantitative safety guarantees. This is achieved by the interplay of three core components: a world model (which provides a mathematical description of how the AI system affects the outside world), a safety specification (which is a mathematical description of what effects are acceptable), and a verifier (which provides an auditable proof certificate that the AI satisfies the safety specification relative to the world model). We outline a number of approaches for creating each of these three core components, describe the main technical challenges, and suggest a number of potential solutions to them. We also argue for the necessity of this approach to AI safety, and for the inadequacy of the main alternative approaches.

Figures (4)

• Figure 1: The GS AI approach builds on three components, namely a world model that describes the environment of the AI system, a safety specification that describes desirable safety properties and is expressed in terms of the world model, and a verifier that provides a quantitative guarantee of the extent to which an AI system satisfies the safety specification. In contrast, current AI Safety practices rely primarily on quality assurance (e.g. evaluations) to decide if an AI system is safe, which is insufficient for safety critical applications.
• Figure 2: Different approaches for building world models can be projected onto a spectrum according to how much safety they would grant if successfully implemented. Approaches listed in green fall into the GS AI family. Approaches in yellow may qualify (depending on underspecified aspects of the approach) or come close to qualifying as GS AI. In our view, approaches in red fail to provide high-assurance quantitative safety guarantees, and thus do not qualify as GS AI.
• Figure 3: Different approaches for creating safety specifications can be projected onto a spectrum according to how much safety they would grant if successfully implemented. Approaches listed in green fall into the GS AI family. Approaches in yellow may qualify (depending on underspecified aspects of the approach) or come close to qualifying as GS AI. In our view, approaches in red fail to provide high-assurance quantitative safety guarantees, and thus do not qualify as GS AI.
• Figure 4: Different approaches to verification can be projected onto a spectrum according to how much safety they would grant if successfully implemented. Approaches listed in green fall into the GS AI family. Approaches in yellow may qualify (depending on underspecified aspects of the approach) or come close to qualifying as GS AI. In our view, approaches in red fail to provide high-assurance quantitative safety guarantees, and thus do not qualify as GS AI.

Theorems & Definitions (10)

• Definition 3.1
• Example 4.1: Code Translation
• Example 4.2: Autonomous Vehicle (AV) Safety
• Example 4.3: Household Robots
• Example 4.4: Medical Diagnosis Agent
• Example 4.5: Compute Centre Management
• Example 4.6: Formally Verified Re-Implementation of Bug-Free Software and Hardware Systems for Cyber Defence.
• Example 4.7: Safe Nucleic Acid Sequence Screening & Synthesis
• Example 4.8: Stabilisation of the Climate System
• Definition 2.1