Guaranteed Safe AI
Definition
Guaranteed Safe AI is a family of AI-safety approaches that aim to attach high-assurance quantitative safety guarantees to an AI system and its deployment infrastructure. In Dalrymple2024 - Towards Guaranteed Safe AI, the core components are a world model, a safety specification, and a verifier.
Why It Matters
Empirical evaluations and red-teaming can miss long-horizon failures, distribution shifts, or systems that behave differently under test. Guaranteed safety reframes the burden of proof: for sufficiently risky AI systems, developers should provide auditable evidence that harmful behavior is ruled out or bounded under explicit assumptions.
Formalism / Key Objects
- World model: a mathematical model or distribution over models describing relevant AI-environment effects.
- Safety specification: a bounded criterion for acceptable behavior, potentially expressed with reachability probabilities, temporal logic, causal counterfactual queries, or other formal constraints.
- Verifier: a procedure that checks the system against the specification relative to the world model and returns a proof certificate, sound probability bound, asymptotic guarantee, or comparable assurance.
- Guaranteed Safe AI Safety Case records the compact assurance tuple and the model-relative probability-bound schema.
- Compact guarantee schema:
- Stronger GS-style guarantees require the verifier to be near the proof, optimal-control, or sound-bound end of the assurance spectrum rather than only the empirical-testing end.
Connections
- Formal Methods supplies specification, abstraction, model checking, proof, and synthesis tools for GS-style safety cases.
- Safe Reinforcement Learning provides runtime filters, safe sets, constraints, and verified policies that can serve as pieces of a GS AI architecture.
- Goal Alignment describes objective-matching failures that a safety specification or world model may need to represent explicitly.
- Probabilistic Model Checking and Runtime Verification are natural verification layers when the world model is stochastic or the guarantee must be monitored during deployment.
- Counterfactual Simulation becomes relevant if a safety specification includes causal counterfactual or fairness criteria.
Common Confusions
- Guaranteed safe does not mean assumption-free. The guarantee is only as strong as the world model, specification, and verifier.
- A high benchmark score is not a safety guarantee unless the benchmark result is embedded in a valid quantitative safety argument.
- A reward function is not always a safety specification; bounded temporal, probabilistic, causal, or hyperproperty constraints may express safety requirements that scalar reward does not.