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

1. Introduction

• GS AI aims to provide high-assurance quantitative safety guarantees through a formal safety specification, a world model, and a verifier.The paper presents these as the framework’s three core components.Source: §1 · p. 1
• As AI systems become more capable or enter safety-critical contexts, developers should bear the burden of demonstrating safety above relevant risk or capability thresholds.The paper argues that experimental tests alone are insufficient for such guarantees.Source: §1 · p. 1
• The paper surveys GS AI approaches and challenges, proposes potential solutions, and discusses practical examples, feasibility, benefits, related work, and conclusions.It frames the approaches as a portfolio of complementary R&D efforts.Source: §1 · pp. 1–2

2. Background

• The background covers the AI safety problem, risk-based classification of AI systems, and empirical safety assessments.Source: §2 · p. 2

2.1. The AI Safety Problem

• The section situates these challenges within long-standing concerns that sufficiently advanced AI could threaten human survival or cause permanent disempowerment.Source: §2.1 · p. 2
• In open-ended domains, specifying intended behavior is difficult because formalizations can leave a substantial gap between what is specified and what is intended.The passage links this challenge to robust action in unprecedented situations.Source: §2.1 · p. 2

2. In a conflict of interests, greater intelligence is a sub-

• If substantially more intelligent AI systems are not aligned with human interests, the authors expect human interests to be marginalized.They connect this concern to the advantage that greater intelligence gives in conflicts of interest.Source: §2 · p. 2
• Correctly specified goals may still be internalized incorrectly, while AI systems also pose immediate risks including disinformation, unfair disadvantage, privacy invasion, and power centralization.The paper focuses primarily on the technical aspect of the safety problem, while noting that technical solutions alone do not ensure global implementation.Source: §2 · pp. 2–3

2.2. AI Safety Levels

• AI Safety Levels classify systems by capability; many current language models appear to be ASL-2, showing early signs of dangerous capabilities whose risks remain importantly bounded, while ASL-4 and higher are not yet defined in as much detail.Source: §2.2 · p. 3

2.3. Empirical Safety Assessments

• Testing and red-teaming can find unsafe behavior but cannot provide rigorous quantitative guarantees, since serious failures may remain undiscovered, including in adversarial settings.The authors cite jailbreaks following extensive evaluation as an example of failures remaining undetected.Source: §2.3 · p. 3
• A positive safety case can combine empirical and theoretical arguments, but empirical inferences may depend on assumptions such as deployment matching the test operating domain.The paper describes stronger bounds from adversarial testing, randomized simulations, mechanistic understanding, and theory-based extrapolation.Source: §2.3 · pp. 3–4
• Because empirical evaluations rely on input-distribution assumptions, distribution shift and deceptive alignment complicate long-horizon guarantees; the authors expect model-based approaches to be needed for stronger assurances at ASL-3 and beyond.The paper notes that powerful AI may itself create novel situations, making distribution shift especially relevant.Source: §2.3 · p. 4

3.1. Definition of GS AI

• GS AI combines a world model, safety specification, and verifier to provide a quantitative safety guarantee, rather than relying primarily on empirical evaluation or informal arguments.The verifier establishes that the system or its output satisfies the specification relative to the world model; the approach is agnostic about how the core AI or containment methods were produced.Source: §3.1 · pp. 4–5

3.2. The World Model

• World models must predict AI-caused effects at specification-relevant granularity and account for uncertainty and applicability; even sound physics models require data about initial and boundary conditions.Manual models may be feasible in known or controllable settings but may not be sufficiently accurate for complex systems; model uncertainty should inform the strength of resulting guarantees.Source: §3.2 · pp. 6–8

3.3. The Safety Specification

• Safety specifications vary by application, can express properties beyond reward functions, and range from human-judged or natural-language criteria to hand-written formal rules.Examples include probabilistic temporal logics, causal counterfactual queries, and hyperproperties; specifications may address physical harm, lawful driving, cyber vulnerabilities, or medical-research risks.Source: §3.3 · p. 9
• Open-ended safety specifications are difficult because concepts such as harm may require detailed world models, while vague predicates and hard-to-extract AI beliefs complicate formalisation.Similar difficulties arise in specifying that an AI never lies or always follows human instructions.Source: §3.3 · pp. 9–10
• Safety proxies can diverge from intuitive judgments when optimized, so specifications may need high accuracy to remain reliable for systems with strong optimization or planning capabilities.The passage describes this as Goodhart’s law.Source: §3.3 · p. 10
• Reward learning may support verifiable preference-respecting systems, but data can leave rewards ambiguous, methods depend on modelling assumptions, and learned rewards are often uninterpretable; conservative or manual predicates are alternatives.Conservative predicates may be sufficient but not necessary for safety, or may make systems safer without ensuring safe behaviour.Source: §3.3 · p. 10
• Formalising safety at the system level can remain feasible even when individual AI components are difficult to specify, as illustrated by autonomous-vehicle systems.A complementary proposal builds a hierarchy of provably compliant systems from hardware-level modules whose verification recursively checks their components.Source: §3.3 · pp. 10–11
• CIRL models AI-human interaction as a cooperative Markov game with shared reward known only to the human, encouraging feedback-seeking behaviour and allowing verification against safety specifications.Specifications may require the AI to be provably beneficial to the human, but can depend on assumptions about human behaviour and preferences.Source: §3.3 · p. 11

3.4. The Verifier

• Strong guarantees require a Level 8, 9, or 10 verifier: finite-time coverage bounds, sound failure-probability bounds, or a concise human-checkable proof.Obtaining such guarantees currently imposes a high burden of specialised cognitive labour, even for relatively simple software properties.Source: §3.4 · p. 12
• A narrowly scoped AI restricted to a formal theorem-prover could automate verification work while limiting real-world influence and power-seeking potential.A proposed training loop combines retrieval, formalisation of literature, proof generation, and reinforcement learning from verified statements and successful proof traces, though challenges remain.Source: §3.4 · p. 12
• Scalable verification calls for analyzable modular abstractions, compositional proofs with inferred contracts, design-time/run-time integration, and replacing key neural modules with verifiable software.The software may be generated through AI-powered synthesis or by distilling learned algorithms with mechanistic interpretability tools.Source: §3.4 · pp. 12–13

4.1. Code Translation

• Code translation requires functional correctness and security specifications, while general translation remains largely unsolved despite simple verified instances.The proposed world model includes program preconditions and security threat models, with large language models suggested for code generation.Source: §4 · pp. 13–14

4.2. Autonomous Vehicle (AV) Safety

• Autonomous driving combines scenario-based safety and functionality rules with world models of vehicles, agents, environments, and human preferences.The ADS should retain a smaller core safety specification outside specified scenarios; runtime monitors check world-model assumptions and may trigger backup action.Source: §4 · p. 14

4.3. Household Robots

• Household robots are specified to perform varied tasks safely while adapting skills to different human needs and home environments.The proposal pairs multi-task and continuous learning with models of diverse homes, tasks, and robot constraints.Source: §4 · p. 14

4.4. Medical Diagnosis Agent

• A medical diagnosis agent is tasked with diagnosing from symptoms, explaining underlying causes, and recommending treatment using models of physiology and environmental factors.The proposed system parses diagnostic notes and medical imaging.Source: §4 · p. 14

4.5. Compute Centre Management

• Compute-centre management targets efficient, correct multi-tenant operation while enforcing business agreements, legal caps, and security.Its world model represents tenant isolation, resource allocation, and cryptographically secured hardware.Source: §4 · pp. 14–15

4.6. Formally Verified Re-Implementation

• Verified re-implementation aims to reduce cyberattack surface by replacing buggy legacy software and hardware with formally verified versions.The AI agent infers intended function through autoformalisation and stakeholder specification work before synthesising a bug-free version.Source: §4 · p. 15

4.7. Safe Nucleic Acid Sequence Screening & Synthesis

• Nucleic-acid screening must reject sequences usable to produce pathogens or toxic chemicals while accepting sequences with health-promoting applications.The proposal models the relationship between molecular structures and pathology and checks whether harmful-application risk remains below a conservative bound.Source: §4 · p. 15

4.8. Stabilisation of the Climate System

• A climate agent would generate geoengineering solutions that verifiably stabilise the climate system without compromising ecosystem health.The world model represents complex climate dynamics under different intervention regimes.Source: §4 · p. 15

Discussion

• Safety-critical AI needs quantitative safety guarantees because empirical evaluations alone do not provide adequate assurance.The discussion presents GS AI as a potential route to such guarantees while acknowledging challenges in the research agenda.Source: §5 · p. 15
• Auditable safety specifications can make democratic oversight easier by allowing outsiders and regulators to examine assumptions behind risk-threshold claims.The authors connect this transparency to the possibility of challenging assumptions that are not socially acceptable.Source: §5 · p. 15
• GS AI proof certificates may support multi-stakeholder coordination by verifying conformance to shared specifications with minimal trust among parties.The paper links this low-trust verification capacity to coordination across stakeholders.Source: §5 · p. 15
• Some GS AI costs may be amortised: once specifications and scalable verification methods exist, new systems may be checked at lower marginal cost.The authors suggest this could reduce incentives to disregard costly safety measures and improve scalability as AI progresses.Source: §5 · p. 16
• GS AI could help secure critical infrastructure, where cybervulnerability is framed as a major catastrophic-risk vector.The examples include water supply, power grids, nuclear plants, dams, and information and communication technology.Source: §5 · p. 16
• An “anytime” R&D portfolio should span cheaper, weaker-assurance evaluations and more ambitious GS AI approaches as safety needs change.The authors also describe feasible partial successes, including provably compliant cybersecurity, geofencing, remote kill switches, and verified sensors and actuators.Source: §5 · p. 16
• Deployment infrastructure can monitor for signs of an inaccurate world model and use a trustworthy backup when disabling the main controller is unsafe.Finite deployment horizons can also limit how long outputs need verification before shutdown or transition to a safe mode, reducing verification complexity.Source: §5 · p. 16
• A policy-based alternative would prove safety directly for interpretable policies rather than using a separate world model, but policy complexity may make interpretation harder.The authors leave the relative difficulty of creating interpretable policies versus interpretable world models as an empirical question for each domain.Source: §5 · pp. 16–17

Relevant Existing Work

• The paper does not claim the three-component architecture as novel; it instead identifies convergence, offers a taxonomy, and outlines a research agenda for high-assurance quantitative safety guarantees.Source: §6 · p. 17

Computational Learning Theory

• Computational learning theory offers formal generalization and regret guarantees, typically for narrow performance metrics; GS AI targets safety assurances for advanced systems in open-ended environments.Source: §6 · p. 17

Formal Verification of AI Systems

• Formal-verification research develops algorithms for checking whether neural networks or systems containing learned components satisfy specifications, sometimes for restricted model classes or interfaces.Source: §6 · p. 17

Program Synthesis

• Correct-by-construction synthesis uses formal methods to derive programs satisfying specifications, with contemporary methods sometimes using learned heuristics guided by verifiers or language models.Source: §6 · p. 17

Model-Based Reasoning and Planning

• Automated planners can generate plans that reach goals while satisfying formal safety specifications, but classical planners assume deterministic Boolean world models; extensions cover stochastic and partially observable settings.Source: §6 · pp. 17–18

Probabilistic Programming

• Probabilistic programming can represent world models combining uncertainty, symbolic code, and learned differentiable components; newer methods may support learning and refining models from data.Source: §6 · p. 18

Safety Engineering

• Safety engineering is a related discipline focused on identifying, evaluating, and mitigating hazards and risks in systems and processes.Source: §6 · p. 18

Boxing Methods

• Earlier AI boxing proposals limit interaction channels, whereas the GS AI gate formally verifies outputs before they can affect the world.Source: §6 · p. 18

Conclusion

• GS AI aims to equip AI systems with formal, verifiable, and auditable safety guarantees; its spectrum includes both static and runtime verification.Source: §7 · p. 18
• Accurate interpretable world models, precise safety specifications, and scalable formal verification remain difficult, so the authors view GS AI alongside complementary safety research.Source: §7 · p. 18
• The authors argue that formal verification can provide stronger safety assurances than empiricism and interpretability, and that narrow or partial GS solutions may still have value.Source: §7 · p. 18
• The authors call for substantially more attention and resources for the GS agenda, while noting that much work remains to develop it fully.Source: §7 · p. 18

Author contributions and Acknowledgements

• David ’davidad’ Dalrymple and Joar Skalse were lead drafters; Ben Goldhaber and Nora Ammann led project coordination.Source: §8 · p. 18
• The paper lists core and contributing authors and thanks several colleagues for feedback on the idea and manuscript.Source: §8 · p. 18
• The authors link the paper's creation to shared understanding at the Bletchley Summit and acknowledge Drexler's Open Agency Model as a prior conceptualization of separated system roles.Source: §8 · pp. 18–19

A. A Definition of Harm

• The causal model represents variables and their relationships in a directed acyclic graph; an intervention leaves upstream variables unchanged and updates downstream variables.Source: A. A Definition of Harm · p. 29
• Causation is assessed counterfactually by comparing actual settings and outcomes with what would have happened under an alternative setting.Source: A. A Definition of Harm · p. 29
• The extended causal model adds an outcome variable with utilities normalized from 0 to 1 and a context-dependent default utility as the reference point for harm.Source: A. A Definition of Harm · p. 29
• An event causes harm when it produces an outcome below the model's default utility and a counterfactual alternative event would have caused a higher-utility outcome.Source: A. A Definition of Harm · p. 29
• The definition is only a starting point: representing utilities and downstream implications meaningfully in a complex world model remains challenging.Source: A. A Definition of Harm · p. 29

• A GS AI system is a policy paired with a world model, safety specification, and verifier, whose output lies in a permissible set.The system is equipped with a quantitative safety guarantee produced by those components.Source: B. A Formal Definition of GS AI · pp. 29–30
• The policy maps histories of observations and actions to a distribution over actions.Source: B. A Formal Definition of GS AI · p. 29
• The world model maps each world state and action to a set of probability distributions over observations and next states; this set may be a credal set.Source: B. A Formal Definition of GS AI · p. 29
• The safety specification assigns each policy and world model a value from 0 to 1, which the verifier computes or estimates.The verifier may be an anytime algorithm that produces increasingly accurate estimates as time increases.Source: B. A Formal Definition of GS AI · p. 30