Guaranteed Safe AI Safety Case
Context
Dalrymple2024 - Towards Guaranteed Safe AI frames high-risk AI safety as a model-based assurance problem. The central claim is not that safety can be guaranteed without assumptions, but that assumptions should be explicit, auditable, and connected to quantitative bounds.
Formal Statement
A GS AI safety case can be represented as a tuple:
The intended assurance judgment is:
The strongest proof-style case has epsilon=0 relative to the world model. Probabilistic or asymptotic cases allow epsilon>0, but the verifier should provide a sound upper bound or a clearly specified convergence guarantee.
Derivation / Construction
- Specify the relevant system boundary, including the AI component, hardware, software, and deployment infrastructure.
- Build or learn a world model that conservatively covers effects relevant to the safety specification.
- State a bounded safety specification, such as reachability constraints, probabilistic temporal-logic formulas, causal counterfactual requirements, or other auditable risk criteria.
- Run a verifier that produces a proof certificate, sound probability bound, optimal-control certificate, or asymptotic guarantee.
- Monitor deployment for evidence that the world model is invalid, and route failures to backup systems or safe-state transitions when necessary.
Implications
- The guarantee is model-relative: a sound verifier cannot compensate for a missing hazard in the world model or a badly chosen specification.
- Empirical evaluation can contribute evidence but does not by itself give the GS-style assurance judgment.
- Existing safe-RL tools such as shields, safe sets, probabilistic model checking, and runtime monitors can serve as components in the larger safety case.
- The schema creates a natural audit target for regulators or external reviewers: inspect the specification, world-model assumptions, and verifier strength separately.