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

Probably not a substantial claim: may not pass S3 (load-bearing).

Correct-by-construction program synthesis is an approach to software development that aims to produce programs guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.

“This is an approach to software development that aims to produce programs that are guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.”

• cites Alur et al., 2013 sourceDisputed

  Split into 2 atoms — 0 confirmed, 1 partially supported, 1 disputed, 0 misattributed, 0 unverifiable. Expand the claim to see per-atom verdicts.

  Checked by a reasoning model — may be wrong.

  Experimental — accuracy not yet measured
• cites Abate et al., 2020 sourceNot checked yet

  Checked before — its earlier verdict is held back until a new check runs.

Probably not a substantial claim: may not pass S3 (load-bearing).

One possible approach to creating a world model with AI is to use large language models or similar systems to write probabilistic programs that correspond to the system being modelled.

“One possible approach to creating a world model with AI is to use large language models (or similar systems) to write probabilistic programs that correspond to the system(s) being modelled (e.g., Wong et al., 2023a;b;Elmaaroufi et al., 2024;Tang et al., 2024;Lew et al., 2020).”

• cites Wong et al., 2023aNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Elmaaroufi et al., 2024 sourceSupported
• cites Tang et al., 2024 sourcePartly supported

  The Introduction describes using an LLM to synthesize a Python program that models the environment’s transition function. But §5, “Limitations and Open Directions,” says WorldCoder currently assumes deterministic dynamics and presents probabilistic programs as a possible future extension, not what its LLM writes in this work. (LLM, conf=0.88)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

For AI systems, probabilistic programs have been shown to be a promising formalism for world modeling.

“For AI systems, probabilistic programs have been shown to be a promising formalism for world modeling (e.g., Milch et al., 2007;Matheos et al., 2020;Gothoskar et al., 2021;Fremont et al., 2022).”

• cites Milch et al., 2007 sourceNot checked yet

  Checked before — its earlier verdict is held back until a new check runs.

• cites Matheos et al., 2020Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Gothoskar et al., 2021 sourceSupported

May combine two claims.

The LLM-based method may also produce world models that are interpretable by default, if the language models are trained on code written by human programmers, or if the language used to generate pieces of the world model is forced or encouraged to be interpretable through probabilistic translation to and from natural language.

“This method may also produce world models that are interpretable by default (Grand et al., 2023), if the language models are trained on code written by human programmers, or if the language used to generate pieces of the world model is forced or encouraged to be interpretable through probabilistic translation to and from natural language (Jacob et al., 2023).”

• cites Grand et al., 2023 sourceNot checked yet

  Not checked in the free run.

• cites Jacob et al., 2023 sourceCould not verify

  Split into 2 atoms — 0 confirmed, 0 partially supported, 0 disputed, 0 misattributed, 2 unverifiable. Expand the claim to see per-atom verdicts.

  Experimental — accuracy not yet measured

May combine two claims.

Formal verification is often hard to produce, even for relatively simple computer programs, and traditional formal methods face unique challenges for AI systems.

“Of course, such formal verification is often hard to produce, even for relatively simple computer programs, and traditional formal methods face unique challenges for AI systems (Seshia et al., 2016).”

• cites Seshia et al., 2016 sourcePartly supported

  Section 3.2 (p. 4) says that producing a high-quality formal specification is challenging even in domains where formal verification has succeeded, and that AI systems exacerbate the challenge. The Conclusion (p. 12) identifies five challenges for applying formal methods to AI systems. Our copy does not establish the more specific claim that formal verification is often hard to produce even for relatively simple computer programs. (LLM, conf=0.86)

  Experimental — accuracy not yet measured

May combine two claims.

Further progress in automated reasoning and theorem proving due to integration with data-driven learning could make formal verification substantially easier, and might also scale with further progress in AI more generally.

“However, further progress in automated reasoning and theorem proving due to integration with data-driven learning (see e.g.Lample et al., 2022;Seshia, 2015;Wu et al., 2022;First et al., 2023;Trinh et al., 2024) could make this substantially easier, and might also scale with further progress in AI more generally.”

• cites Lample et al., 2022 sourceSupported
• cites Seshia, 2015 sourceNot checked yet

  Checked before — its earlier verdict is held back until a new check runs.

• cites Wu et al., 2022Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Using probabilistic programming, one can leverage sequential Monte Carlo methods to gradually infer a theory represented as a probabilistic program as new data is observed, or by incrementally refining an initially coarse 3D world model.

“Using probabilistic programming, one can leverage sequential Monte Carlo (SMC) methods to gradually infer a theory T (represented as probabilistic program) as new data is observed (Saad et al., 2023), or by incrementally refining an initially coarse 3D world model (Gothoskar et al., 2023;Stuhlmüller et al., 2015).”

• cites Saad et al., 2023 sourceSupported
• cites Gothoskar et al., 2023 sourceNot checked yet

  Checked before — its earlier verdict is held back until a new check runs.

• cites Stuhlmüller et al., 2015 sourcePartly supported

  The Introduction (p. 2) describes using SMC to refine a probabilistic model from coarse to fine. The stereo-matching experiment (p. 9) applies this to a disparity map that can provide a rough measure of depth, but it does not describe incrementally refining a 3D world model. (LLM, conf=0.86)

  Experimental — accuracy not yet measured

May combine two claims.

Most data sources are insufficient for identifying the underlying reward function uniquely, even in the limit of infinite data, and this irreducible ambiguity may be problematic.

“In particular, most data sources are insufficient for identifying the underlying reward function uniquely, even in the limit of infinite data, and this irreducible ambiguity may be problematic (Ng & Russell, 2000;Dvijotham & Todorov, 2010;Cao et al., 2021;Kim et al., 2021;Skalse et al., 2023;Schlaginhaufen & Kamgarpour, 2023).”

• cites Ng & Russell, 2000Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Dvijotham & Todorov, 2010Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Cao et al., 2021 sourcePartly supported

  The Introduction (p. 2) says that even perfect knowledge of an optimal policy does not fully identify the reward, and Section 7.1 (p. 24) shows that this is not statistical error. The Introduction (p. 1) explains why identifying the specific reward matters for predictions in changed environments. The paper establishes this ambiguity for particular IRL observations, not the broader claim that most data sources are insufficient; it also describes conditions under which rewards can be identified. (LLM, conf=0.84)

  Experimental — accuracy not yet measured

May combine two claims.

The learnt reward model is itself typically not interpretable, which is a serious issue.

“Finally, the learnt reward model is itself typically not interpretable, which is a serious issue (see e.g.Michaud et al., 2020;Jenner & Gleave, 2022).”

• cites Michaud et al., 2020Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Jenner & Gleave, 2022 sourceSupported

May combine two claims.

While such a proxy may robustly correlate with our intuitive judgements of harm in normal situations, they may still reliably come apart if those proxies are used as an optimisation target.

“However, while such a proxy may robustly correlate with our intuitive judgements of harm in normal situations, they may still reliably come apart if those proxies are used as an optimisation target.”

• cites Goodhart (1975)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Manheim & Garrabrant (2019)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Hennessy & Goodhart (2023) sourcePartly supported

  The Introduction describes predictions fitted to clean training data that become biased when future agents manipulate the covariates used for prediction. That supports the general point that a useful proxy can diverge from what it predicts when incentives target it. The paper does not address proxies for intuitive judgements of harm specifically. (LLM, conf=0.85)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Safety specifications could be expressed in terms of probabilistic computation tree logic (PCTL), or in terms of conjunction of linear inequalities of reachability probabilities.

“Safety specifications could be expressed in terms of probabilistic computation tree logic (PCTL) (Hansson & Jonsson, 1994), or in terms of conjunction of linear inequalities of reachability probabilities, for example.”

• cites Hansson & Jonsson, 1994 sourceSupported

May combine two claims.

A safety specification is in general different from a reward function, though they include bounded reward functions as a special case.

“A safety specification is in general different from a reward function, though they include bounded reward functions as a special case.”

• cites Amodei et al., 2016 sourcePartly supported

  The Safe Exploration section (p. 15) describes safety in terms of constraints, including an approach with separate safety and performance functions. This supports distinguishing safety requirements from a reward function, but the paper does not say that safety specifications include bounded reward functions as a special case. (LLM, conf=0.81)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

Seshia et al. (2022) presents 15 principles for providing provable guarantees of safety for AI systems.

“Seshia et al. (2022), who presents 15 principles for providing provable guarantees of safety for AI systems.”

• cites Seshia et al. (2022) sourceSupported

Classified as probably not a substantial claim.

The informal to formal translation data for this phase can be generated using cycle-consistency training together with the small but increasing amounts of human-verified formalization of informal statements.

“The informal to formal translation data for this phase can be generated using cycle-consistency training (Lample et al., 2017) together with the small but increasing amounts of humanverified formalization of informal statements.”

• cites Lample et al., 2017 sourceSupported

• AssumptionRests on an assumption: Early examples of models that extract statements and definitions from text and formalise them already exist, but they must be improved before they are of sufficient quality to be used in the initial phase of a bootstrap loop.

Probably not a substantial claim: may not pass S3 (load-bearing).

We may attempt to create safety predicates which make an AI system more safe, even if they do not ensure safe behaviour.

“Alternatively, we may attempt to create safety predicates which make an AI system more safe, even if they do not ensure safe behaviour (as e.g.Soares et al., 2015;Orseau & Armstrong, 2016;Hadfield-Menell et al., 2017, etc).”

• cites Soares et al., 2015Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Orseau & Armstrong, 2016Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Hadfield-Menell et al., 2017 sourceSupported

Classified as probably not a substantial claim.

One important piece is devising suitable abstractions of AI components such as neural networks.

“First of all, one important piece is devising suitable abstractions of AI components such as neural networks.”

• cites Seshia et al. (2022) sourceSupported

May combine two claims.

The algorithms to be coded up and verified can be autogenerated either by direct AI-powered program synthesis or by using automated mechanistic interpretability tools to distill machine-learned algorithms into verifiable code.

“The algorithms to be coded up and verified can be autogenerated either by direct AI-powered program synthesis or by using automated mechanistic interpretability tools to distill machine-learned algorithms into verifiable code (Michaud et al., 2024).”

• cites Michaud et al., 2024 sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Probabilistic programming languages (e.g. Scenic) offer one mechanism for world modelling for autonomous vehicle safety and have had some success in practice.

“Probabilistic programming languages (e.g.Scenic, Fremont et al., 2022) offer one mechanism for world modelling for this application and have had some success in practice.”

• cites Fremont et al., 2022 sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Defining functional correctness is easy in some cases but more complicated in general since the source and target program structure can be very different and specifications can be partial.

“Defining functional correctness is easy in some cases (e.g., (Bhatia et al., 2024)) but more complicated in general since the source and target program structure can be very different and specifications can be partial.”

• cites Bhatia et al., 2024 sourceSupported

May combine two claims.

Recent advances in probabilistic programming have led to more general and scalable methods for Bayesian inference, probabilistic program synthesis, and automatic differentiation of expected values, which may serve as key enablers for learning and refining world models from data.

“Recent advances in probabilistic programming have also led to more general and scalable methods for Bayesian inference (Baydin et al., 2019b;Lew et al., 2023b), probabilistic program synthesis (Saad et al., 2023), and automatic differentiation of expected values (Lew et al., 2023a), which may serve as key enablers for learning and refining world models from data.”

• cites Baydin et al., 2019bNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Lew et al., 2023bNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Saad et al., 2023 sourcePartly supported

  Split into 2 atoms — 1 confirmed, 1 partially supported, 0 disputed, 0 misattributed, 0 unverifiable. Expand the claim to see per-atom verdicts.

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

This literature has proposed a range of algorithms which can be used to ensure that a given neural network satisfies a given specification, or that a system containing neural components satisfies a safety specification.

“This literature has proposed a range of algorithms which can be used to ensure that a given neural network (potentially belonging to some restricted class) satisfies a given specification (typically specified over its interfaces), or that a system containing neural components satisfies a safety specification.”

• cites Seshia et al. (2022) sourceSupported
• cites Albarghouthi (2021) sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

Many contemporary program synthesis methods involve learning algorithms, e.g., using neural network heuristics, guided by oracles such as formal verifiers or LLMs to accelerate the learning process.

“Many contemporary program synthesis methods involve learning algorithms, e.g., using neural network heuristics, guided by oracles such as formal verifiers or LLMs to accerelate the learning process (Ellis et al., 2023;Grand et al., 2023).”

• cites Ellis et al., 2023 sourcePartly supported

  The Introduction and §2 (Wake/sleep program learning; page unavailable) describe neural networks that guide program search and speed up problem-solving. The cited paper does not support the added claim that formal verifiers or LLMs serve as oracles guiding that learning process. (LLM, conf=0.86)

  Experimental — accuracy not yet measured
• cites Grand et al., 2023 sourcePartly supported

  Section 2 identifies neural-network guidance as a way to make program-synthesis search more tractable, and Section 3 describes LILO using an LLM for approximate search. The paper does not describe formal verifiers as guiding oracles; it describes checking candidate programs by execution. It also treats the LLM as a search model rather than an oracle. (LLM, conf=0.86)

  Experimental — accuracy not yet measured

May combine two claims.

ChatGPT was evaluated in great detail over several months, and users found ways to circumnavigate its safety precautions within a single day of it going public.

“For example, ChatGPT was evaluated in great detail over a period of several months (OpenAI et al., 2024), and yet users found ways to circumnavigate its safety precautions within just a single day of it going public (Burgess, 2023).”

• cites OpenAI et al., 2024Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Burgess, 2023Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

About 25% of bridges built in the 1870s collapsed within the decade, before a deeper theoretical understanding of civil engineering reduced bridges' failure rates to less than 0.4% per decade.

“About 25% of bridges built in the 1870s collapsed within the decade (McCullough, 2001), before a deeper theoretical understanding of civil engineering reduced bridges' failure rates to less than 0.4% per decade (Cook, 2014).”

• cites McCullough, 2001Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Cook, 2014Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

If successful, the LLM-based approach could produce a world model on Level 2, 3 or possibly 4, depending on the extent to which the resulting model is audited.

“If successful, this approach could produce a world model on Level 2, 3 or possibly 4, in the classification above (depending on the extent to which the resulting model is audited).”

Probably not a substantial claim: may not pass S3 (load-bearing).

The LLM-based world-modeling method has the potential to be scalable, since most of the work is offloaded to AI systems.

“This method has the potential to be scalable, since most of the work is offloaded to AI systems.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

World models serve to elucidate the AI system designers' assumptions, and those assumptions may hold only part of the time.

“World models also serve to elucidate the AI system designers' assumptions, and we must be mindful that those assumptions may hold only part of the time.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Fault trees are a common safety engineering technique that allows for quantitative analysis, interpretable as deduction in probabilistic logic.

“Fault trees (Nieuwhof, 1975) are a common safety engineering technique that allows for quantitative analysis, which can be interpreted as deduction in probabilistic logic.”

• cites Nieuwhof, 1975 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S4 (based). May combine two claims.

We must be able to trust the correctness of the world model, which means that it ideally should be interpretable and understandable.

“Of course, we must also be able to trust the correctness of this world model, which means that it ideally should be interpretable and understandable.”

Probably not a substantial claim: may not pass S4 (based).

If the verifier and the world model together can establish that the AI, or the AI's output, satisfies the safety specification, a quantitative safety guarantee is obtained, even if the AI system remains uninterpretable.

“If the verifier and the world model together can establish that the AI (or the AI's output) satisfies the safety specification, a quantitative safety guarantee is obtained (even if the AI system remains uninterpretable, etc).”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

One of the main challenges with the LLM-based approach would likely be to ensure that the world model has a high predictive accuracy.

“One of the main challenges with this approach would likely be to ensure that the world model has a high predictive accuracy.”

Classified as probably not a substantial claim. May combine two claims.

The GS AI approach remains agnostic about both how the core AI system was produced, and about what containment or boxing methods are used.

“Note that the GS AI approach remains agnostic about both how the”

• cites Armstrong et al., 2012 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

A rigorous theory for how deep networks generalise might enable principled extrapolation from empirical testing on a limited validation domain to a broader test domain.

“For example, a rigorous theory for how deep networks generalise (as built towards by, e.g., Kearns & Vazirani, 1994;Watanabe, 2009;2018;Mingard et al., 2021;2020) might enable principled extrapolation from empirical testing on a limited validation domain to a broader test domain.”

• cites Kearns & Vazirani, 1994 sourceNot checked — no full text of the source
• cites Watanabe, 2009Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Mingard et al., 2021Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based). May combine two claims.

In principle, the manual approach is likely to provide the best understanding of the assumptions underlying the world model, as well as the delineation of its domain of applicability.

“In principle, this manual approach is likely to provide the best understanding of the assumptions underlying the world model, as well as the delineation of its domain of applicability.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

For AI systems that directly interface with very complex systems such as human users, the world economy, or sensitive ecosystems, it may not be possible to create sufficiently accurate world models in a fully manual way.

“However, for AI systems that directly interface with very complex systems (such as e.g.human users, the world economy, or sensitive ecosystems), it may not be possible to create sufficiently accurate world models in a fully manual way.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing). May combine two claims.

The world model need not be a complete model of the world; the level of detail and abstraction that is adequate depends on the safety specification and the AI system's context of use.

“Note that the world model need not be a”

Probably not a substantial claim: may not pass S2 (checkable). May combine two claims.

Without a world model we can only verify specifications defined over input-output relations, but it is often desirable to instead verify specifications over input-outcome relations.

“More generally, without a world model we can only verify specifications defined over input-output relations, but it is often desirable to instead verify specifications over input-outcome relations.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

A key challenge for world models is finding a satisfactory solution to handling both Bayesian and Knightian uncertainty.

“A key challenge -which we will discuss more below -is finding a satisfactory solution to handling both Bayesian and Knightian uncertainty.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The manual approach would produce a world model on Level 4 or 5.

“This approach would produce a world model on Level 4 or 5.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

In such cases, the world model must instead be machine learned or automatically generated by some other means.

“In such cases, the world model must instead be machine learned (or automatically generated by some other means).”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Even stronger bounds may be obtained through a more mechanistic understanding of the system.

“Even stronger bounds may be obtained through a more mechanistic understanding of the system.”

Probably not a substantial claim: may not pass S2 (checkable).

The domain of applicability and epistemic uncertainty regarding different pieces of the world model must be represented and taken into account.

“Hence, the domain of applicability and epistemic uncertainty regarding different pieces of the world model must be represented and taken into account.”

Probably not a substantial claim: may not pass S2 (checkable).

For these reasons, the world model, or relevant aspects of it, should be auditable or monitorable at run time.

“For these reasons, the world model, or relevant aspects of it, should be auditable or monitorable at run time.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Stronger empirical bounds, with weaker assumptions, may be obtained through methods such as adversarial testing and/or testing in simulations with domain randomisation.

“Stronger empirical bounds (i.e. with weaker assumptions) may be obtained through methods such as adversarial testing, and/or testing in simulations with domain randomisation.”

May combine two claims.

Manual world models have been created in settings where the operating environment is known or controllable, such as controllers in airplanes and self-driving cars, and are commonly used in scientific research including epidemic simulators and particle physics simulators.

“This has been done in settings where the operating environment is known or controllable, for e.g.controllers in airplanes (Garion et al., 2022;Fremont et al., 2020a) and self-driving cars (Ivanov et al., 2020;Fremont et al., 2020b).Such models are also commonly used in scientific research, including epidemic simulators (Broeck et al., 2011) and particle physics simulators (Baydin et al., 2019b).”

• cites Garion et al., 2022Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Fremont et al., 2020aNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Ivanov et al., 2020 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S1 (asserted), S2 (checkable), S3 (load-bearing), S4 (based).

'Harm' is a vague predicate, in the sense that there are edge-cases where it is controversial whether a given person is harmed or not.

“Moreover,”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

Similar issues occur if we want to ensure that an AI system never lies, or that it always follows instructions from humans.

“Similar issues occur if we want to ensure that an AI system never lies, or that it always follows instructions from humans, etc.”

May combine two claims.

Task-specific AI services often afford contextual operationalisations of safety, while more general-purpose AI assistants may require specifications that invoke broad definitions of harm.

“Task-specific AI services often afford contextual operationalisations of safety, while more general-purpose AI assistants may require specifications that invoke broad definitions of harm (Beckers et al., 2022b;London & Heidari, 2023).”

• cites Beckers et al., 2022bNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites London & Heidari, 2023Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based). May combine two claims.

Humans are very complex, and it seems dubious to presuppose that it is possible to create a model of human behaviour.

“Moreover, humans are very complex, and it seems dubious to presuppose that it is possible to create a model of human behaviour”

Probably not a substantial claim: may not pass S3 (load-bearing).

If successful, the physics-verified approach would produce a world model on Level 4.

“If successful, this would produce a world model on Level 4.”

May combine two claims.

A world model can include model uncertainty, and this uncertainty can be taken into account when the safety specifications are verified.

“First of all, a world model can (and should) of course include model uncertainty, and this uncertainty can be taken into account when the safety specifications are verified.”

May combine two claims.

We can be confident that a system truly satisfies a specification if that specification is verified for that system relative to our best theories of physics, and that specification also includes the requirement that the system is not moved beyond the domains where our theories are known to be accurate.

“We can therefore be confident that a system truly satisfies a specification if that specification is verified for that system relative to our best theories of physics, and that specification also includes the requirement that the system is not moved beyond the domains where our theories are known to be accurate.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

A very ambitious approach would be to use world models that are formally verified as being sound abstractions of the basic laws of physics.

“A very ambitious approach would be to use world models that are formally verified as being sound abstractions of the basic laws of physics.”

Probably not a substantial claim: may not pass S2 (checkable). May combine two claims.

Any strategy for creating safe AI systems must rely on some beliefs or assumptions about the real world, and these assumptions could be wrong; a world model simply makes these assumptions explicit.

“Any strategy for creating safe AI systems must rely on some beliefs or assumptions about the real world, and these assumptions could be wrong; a world model simply makes these assumptions explicit.”

Classified as probably not a substantial claim.

Goodhart's law is an informal principle sometimes stated as 'when a measure becomes a target, it ceases to be a good measure'.

“This phenomenon is known as Goodhart's law, which is an informal principle sometimes stated as”

• cites Goodhart (1975)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

The levels in the classification above can be mixed within a single GS AI system.

“Also note that the levels in the classification above can be mixed within a single GS AI system.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

There are many possible strategies for creating safety specifications.

“There are many possible strategies for creating safety specifications.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

If we assume that a human's preferences can be captured by a reward function, and if we can learn a representation of this reward function from some data source, then we may be able to prove that a given AI system will respect the preferences which are embodied by that reward function.

“If we assume that a human's preferences can be captured by a reward function, and if we can learn a representation of this reward function from some data source, then we may be able to prove that a given AI system will respect the preferences which are embodied by that reward function.”

May combine two claims.

Authoring safety specifications is routine in automated controller design, and can frequently be achieved for both traditional software systems and domain-specific AI.

“Authoring safety specifications is routine in automated controller design (Tabuada, 2009), and can frequently be achieved for both traditional software systems and domainspecific AI.”

• cites Tabuada, 2009 sourceNot checked — no full text of the source

May combine two claims.

While physics is not a completed field, there is good reason to believe that our current best theories are completely accurate in certain domains; for example, quantum gravity effects appear irrelevant to contemporary AI systems.

“Note that while physics is not a completed field, there is good reason to believe that our current best theories are completely accurate in certain domains: for example, quantum gravity effects appear irrelevant to contemporary AI systems (see e.g.Carroll, 2021).”

• cites Carroll, 2021Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

In many cases, it will likely be necessary for the world model to model the behaviour of humans.

“Note that in many cases, it will likely be necessary for the world model to model the behaviour of humans.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

One strategy is to attempt to learn safety specifications from data. This is explored by the field of reward learning, where the specification is assumed to have the form of a reward function.

“One strategy is to attempt to learn safety specifications from data.This is explored by the field of reward learning, where the specification is assumed to have the form of a reward function.”

May combine two claims.

Both the neural network and sequential Monte Carlo approaches can potentially be combined, and benefit from more computation: by increasing the size or training time of the neural network used to approximate the posterior, convergence to the true posterior is expected.

“Both of these approaches can potentially be combined 6 , and also benefit from more computation: by increasing the size or training time of the neural network used to approximate P (T | D), convergence to the true posterior is expected.”

Classified as probably not a substantial claim. May combine two claims.

If successful, the data-driven Bayesian approach would produce a world model on Level 2, or 4 if the model passes additional checks.

“If successful, this approach would produce a world model on Level 2 (or 4, if the model passes additional checks).”

May combine two claims.

If it is impossible to create world models that are sufficiently accurate to ensure that an AI system adheres to some specification, then it is presumably in general impossible to ensure that this specification is satisfied by that system.

“Stated differently, if it is impossible to create world models that are sufficiently accurate to ensure that an AI system adheres to some specification, then it is presumably in general impossible to ensure that this specification is satisfied by that system.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

We can further decrease the risks associated with insufficient training or sampling by encouraging the inferred theories to be human-inspectable.

“We can further decrease the risks associated with insufficient training or sampling by encouraging the inferred theories to be human-inspectable (e.g. by conditioning on the constraint that theories can be converted to natural language and back with minimal error).”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

There may in some cases be a fundamental trade-off between interpretability and predictive accuracy.

“There may thus in some cases be a fundamental trade-off between interpretability and predictive accuracy.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

These strategies can roughly be placed on a spectrum, depending on how much safety it would grant if successfully implemented.

“These strategies can roughly be placed on a spectrum, depending on how much safety it would grant if successfully implemented.”

Classified as probably not a substantial claim. May combine two claims.

In CIRL, both players have the same reward function, but only the human knows what the reward function is.

“Both players have the same reward function, but only the human knows what the reward function is.”

• cites Hadfield-Menell et al. (2024)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing). May combine two claims.

We may require that the AI has no incentive to influence any part of the external world, or to find out any information about the external world.

“For example, we may require that the AI has no incentive to influence any part of the external world, or to find out any information about the external world (e.g.Armstrong et al., 2012;Armstrong & O'Rorke, 2018;Armstrong & O'Rourke, 2018;Everitt et al., 2021;van Merwijk et al., 2022).”

• cites Armstrong et al., 2012 sourceNot checked — no full text of the source
• cites Armstrong & O'Rorke, 2018Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Armstrong & O'Rourke, 2018Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

AI systems could be used to suggest new specifications, to critique proposed specifications, or to generate examples of cases where two candidate specifications differ.

“AI systems could be used to suggest new specifications, to critique proposed specifications, or to generate examples of cases where two candidate specifications differ.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Another approach is to attempt to create 'conservative' safety predicates which aim to be sufficient (but not necessary) for safety.

“Another approach is to attempt to create”

Probably not a substantial claim: may not pass S4 (based).

A proof-generation agent can be trained on the relatively large corpus of existing formal theorems.

“Similarly, a proof-generation agent can be trained on the relatively large corpus of existing formal theorems.”

Probably not a substantial claim: may not pass S4 (based).

This restricts the AI's potential for power-seeking behaviour.

“This restricts the AI's potential for power-seeking behaviour.”

May combine two claims.

It is much harder to discover an algorithm with a compliance proof than to verify it, which can be done with just a few hundred lines of human-written code.

“Just as it is much harder to find a needle in a haystack than to verify that it is a needle, it is much harder to discover an algorithm with a compliance proof than to verify it -which can be done with just a few hundred lines of human-written code (Megill, 2023).”

• cites Megill, 2023Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Further development in AI capabilities will tend to make it easier to create good safety specifications.

“further development in AI capabilities will tend to make it easier to create good safety specifications.”

Classified as probably not a substantial claim. May combine two claims.

In CIRL, the two players must cooperate to obtain a high reward, and the AI system must listen to feedback from the human.

“This means that the two players must cooperate to obtain a high reward, and that the AI system must listen to feedback from the human.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Many of the challenges to reward learning also apply to CIRL.

“Also note that many of the challenges to reward learning also apply to CIRL.”

May combine two claims.

The PCS-approach rests on a foundation of relatively simple provably compliant systems, from sensors, actuators and memory devices, to microprocessors with physics-based proofs that they meet their specification, including a protocol guaranteed to reveal failure or tampering.

“the PCS-approach rests on a foundation of relatively simple provably compliant systems, from sensors, actuators and memory devices, to microprocessors with physics-based proofs that they meet their specification -including a protocol guaranteed to reveal failure or tampering.”

• cites Tegmark & Omohundro (2023)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Such specifications may require the world model to also make modelling assumptions about the behaviour of the human (and in particular about how the behaviour of the human relates to its preferences).

“Note that such specifications may require the world model to also make modelling assumptions about the behaviour of the human (and in particular about how the behaviour of the human relates to its preferences).”

Probably not a substantial claim: may not pass S4 (based).

The scope of training for such an agent would be very limited, i.e., it would only be exposed to natural language mathematics and computer science.

“Note that the scope of training for such an agent would be very limited, i.e., it would only be exposed to natural language mathematics and computer science.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

It may be possible to train AI systems without ASL-4 capabilities to automate much of this labour at a near-expert level of sophistication without raising significant safety concerns.

“it may be possible to train AI systems without ASL-4 capabilities to automate much of this labour at a near-expert level of sophistication without raising significant safety concerns.”

• AssumptionRests on an assumption: Even for relatively simple properties of software, obtaining strong guarantees currently imposes a very high burden, as it requires highly specialised cognitive labour.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

While certainly challenging, it may still be feasible to simply specify the safety predicates manually.

“Moreover, while certainly challenging, it may still be feasible to simply specify the safety predicates manually.This is (partially) attempted in works such as e.g.Beckers et al. (2022a;b).”

• cites Beckers et al. (2022a;b)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Additional capability can be achieved via a reinforcement learning loop that trains the translation model and the neural prover in lockstep.

“Additional capability can be achieved via a reinforcement learning loop that trains the translation model and the neural prover in lockstep.”

• AssumptionThe authors state this as an assumption: Both the translation model and the neural prover can be assumed to be retrieval-augmented large language models.

Classified as probably not a substantial claim.

A complementary approach is to create a hierarchy of safety specifications for provably compliant systems (PCSs) all the way down to the physical level.

“A complementary approach is to create a hierarchy of safety specifications for provably compliant systems (PCSs) all the way down to the physical level”

• cites Tegmark & Omohundro (2023)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Progress in AI could thus also accelerate the creation of good safety specifications.

“Progress in AI could thus also accelerate the creation of good safety specifications.”

Probably not a substantial claim: may not pass S4 (based).

Different approaches to verification can be projected onto a spectrum according to how much safety they would grant if successfully implemented.

“Different approaches to verification can be projected onto a spectrum according to how much safety they would grant if successfully implemented.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

There are multiple existing proof-of-concept solutions for various components of this reinforcement learning system, which suggests that a full solution may be realizable in the coming years.

“there are multiple existing proof-of-concept solutions for various components of this reinforcement learning system (Szegedy, 2020), which suggests that a full solution may be realizable in the coming years.”

• cites Szegedy, 2020 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

The difficulties in formalising specifications are not unique to the GS research agenda.

“These difficulties are thus not unique to the GS research agenda.”

• AssumptionRests on an assumption: Most approaches to AI safety require formal safety specifications (or at least formalisations of what an AI system should be optimised for).

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The prover can be trained on the successful proof traces.

“In addition, the prover can be trained on the successful proof traces.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Whenever a statement is proven to be correct and it is useful for proving other statements like its informal counterpart, it can be considered to be a correct transcription and used for training the translation model.

“Whenever a statement is proven to be correct (that is, verified by the formal prover), and it is useful for proving other statements like its informal counterpart, it can be considered to be a correct transcription and used for training the translation model.”

Probably not a substantial claim: may not pass S3 (load-bearing).

CIRL formulates the interaction between an AI and a human as a two-player Markov game.

“CIRL formulates the interaction between an AI and a human as a two-player Markov game”

• cites Hadfield-Menell et al. (2024)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

A comprehensive suite of rigorous empirical evaluations may be expensive and time-consuming, and this cost would have to be paid again for each new AI system created.

“For example, a comprehensive suite of rigorous empirical evaluations may be expensive and time-consuming to carry out, and this cost would (presumably) have to be paid again for each new AI system that is created.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

This alternative strategy may also be more difficult, especially because the policy may be more complex than the world model.

“However, it may also be more difficult, especially because the policy may be more complex than the world model.”

Probably not a substantial claim: may not pass S2 (checkable).

In cases where a system is safety critical, it may not be possible or desirable to simply shut it down.

“It is worth noting that in cases where a system is safety critical, it may not be possible or desirable to simply shut it down.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

GS AI may not be the only route to achieving verifiable quantitative safety guarantees.

“Moreover, while we have argued for the need for verifiable quantitative safety guarantees, it is important to note that GS AI may not be the only route to achieving such guarantees.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing). May combine two claims.

Quick partial successes in GS AI are both plausible and useful.

“Furthermore, quick partial successes in GS AI are both plausible and useful.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

It may be much easier to create an interpretable world model than to create a performant interpretable policy.

“In a similar way, it may be much easier to create an interpretable world model than to create a performant interpretable policy.”

May combine two claims.

The deployment systems can allow us to shorten the time horizon of outputs that need to be verified, thereby reducing the complexity of verification and increasing its tractability.

“The deployment systems can therefore also allow us to shorten the time horizon of outputs that need to be verified, thereby reducing the complexity of verification and increasing its tractability.”

Probably not a substantial claim: may not pass S3 (load-bearing).

A complementary approach is to replace neural networks by traditional formally verifiable software in deployed systems or key modules thereof.

“A complementary approach is to replace neural networks by traditional formally verifiable software in deployed systems or key modules thereof (Tegmark & Omohundro, 2023).”

• cites Tegmark & Omohundro, 2023Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable).

Safety-critical AI systems need to be equipped with quantitative safety guarantees.

“We have argued that safety-critical AI systems need to be equipped with quantitative safety guarantees, and that empirical evaluations alone are insufficient for producing such guarantees with an adequate level of assurance.”

Probably not a substantial claim: may not pass S3 (load-bearing).

If signs that the world model is inaccurate are detected, the AI system could be disabled to ensure that there is no unaccounted for risk of unsafe behaviour.

“If such signs are detected then the AI system could be disabled, to ensure that there is no unaccounted for risk of unsafe behaviour.”

Probably not a substantial claim: may not pass S4 (based).

A drastic reduction of the attack surface area and thus improved cybersecurity can be achieved by replacing legacy code with software that has been formally verified to be bug-free and trustworthy.

“A drastic reduction of this surface area and thus improved cybersecurity can be achieved by replacing legacy code with software that has been formally verified to be bug-free and trustworthy.”

• AssumptionRests on an assumption: The currently existing software and hardware infrastructure contains many bugs, thereby creating a large attack surface area for cyberattacks.

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

It is much easier to specify the axioms of Euclidean geometry than to specify a computer program that is good at proving theorems about Euclidean geometry.

“For example, the rules of chess are less complex than a policy which is good at chess, and it is much easier to specify the axioms of Euclidean geometry than it is to specify a computer program that is good at proving theorems about Euclidean geometry.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

These bounds typically show that a given learning algorithm under some given circumstances is guaranteed to attain a given level of performance with at least some given probability, and may also show how these probabilities scale in terms of the amount of training data.

“These bounds typically show that a given learning algorithm under some given circumstances is guaranteed to attain a given level of performance with at least some given probability, and may also show how these probabilities scale in terms of the amount of training data, etc (see e.g.Kearns & Vazirani, 1994).”

• cites Kearns & Vazirani, 1994 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Much remains to be done to solve the general code translation problem.

“While some simple instances of this general problem have been solved (e.g., translating side effect-free functional programs from a source language to a domainspecific target language (Bhatia et al., 2024)), much remains to be done to solve the general code translation problem.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

An alternative approach to achieving verifiable quantitative safety guarantees is to extract interpretable policies from black-box algorithms via automated mechanistic interpretability and directly proving safety guarantees about these policies.

“An alternative approach might be to extract interpretable policies from black-box algorithms via automated mechanistic interpretability and directly proving safety guarantees about these policies.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

This alternative approach differs from GS AI in that it does not make use of a world model separate from the policy; instead, it requires that the policy can itself be made interpretable.

“This approach differs from GS AI in that it does not make use of a world model that is separate from the policy; instead, it requires that the policy can itself be made interpretable.”

Probably not a substantial claim: may not pass S3 (load-bearing).

It is ultimately an empirical question whether it is easier to create interpretable world models or interpretable policies in a given domain of operation.

“However, it is ultimately an empirical question whether it is easier to create interpretable world models or interpretable policies in a given domain of operation.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

GS AI systems themselves may be useful for creating bug-free software and tamperproof hardware that could be used in backup systems.

“Also note that GS AI systems themselves may be useful for creating bug-free software and tamperproof hardware that could be used in backup systems.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Computational learning theory investigations have produced various formal guarantees for large classes of learning algorithms, primarily in the form of generalisation guarantees and regret bounds.

“These investigations have produced various formal guarantees for large classes of learning algorithms, primarily in the form of generalisation guarantees and regret bounds.”

• cites Kearns & Vazirani, 1994 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S4 (based).

Any potential safety measure faces the issue that if it is costly to implement, there is an incentive to disregard it.

“Any potential safety measure (in AI or elsewhere) faces the issue that if said safety measure is costly to implement, then there is an incentive to disregard it.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

Provably compliant cybersecurity, geofencing, remote kill switches, verified sensors and actuators may all be feasible even if the most ambitious proposals within the GS AI agenda are not, and would still provide benefits in their own right.

“For example, provably compliant cybersecurity, geofencing, remote kill switches, verified sensors and actuators, etc., may all be feasible even if the most ambitious proposals within the GS AI agenda are not, and would still provide benefits in their own right.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Arguably the first system with separate components for world-modelling, specification, and verification was the GPS, published by Newell & Simon, 1961.

“Note that we do not mean to claim novelty with respect to the three-component architecture -for example, arguably the first system with separate components for world-modelling, specification, and verification was the (GPS), published by (Newell & Simon, 1961).”

• cites Newell & Simon, 1961Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Classified as probably not a substantial claim.

There is a spectrum of approaches for safety assessments, ranging from easy ones that provide weaker safety assurances to more expensive procedures that provide stronger safety guarantees.

“We also want to emphasise that there is a spectrum of approaches for safety assessments, ranging from easy ones that provide weaker safety assurances (such as evaluations and red teaming) to more expensive procedures that provide stronger safety guarantees (such as the approaches within the GS AI spectrum).”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

An important benefit to GS AI is that it makes democratic oversight easier, because concrete safety specifications can be audited and discussed by outside observers and regulators.

“An important benefit to GS AI is that it makes democratic oversight easier, because concrete safety specifications can be audited and discussed by outside observers and regulators.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

This alternative strategy may be easier if it is intractably difficult to create a sufficiently good world model or adequate methods for doing formal verification relative to that world model.

“This strategy may be easier if it is intractably difficult to create a sufficiently good world model or adequate methods for doing formal verification relative to that world model.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The rules of chess are less complex than a policy which is good at chess.

“For example, the rules of chess are less complex than a policy which is good at chess, and it is much easier to specify the axioms of Euclidean geometry than it is to specify a computer program that is good at proving theorems about Euclidean geometry.”

Probably not a substantial claim: may not pass S2 (checkable).

These assumptions can then be challenged by the regulator (and society at large) if they are not deemed socially acceptable.

“These assumptions can then be challenged by the regulator (and society at large) if they are not deemed socially acceptable.”

• AssumptionRests on an assumption: In other safety-critical industries, probabilistic safety assessment means that the developer must specify all the assumptions or premises needed to deduce that their system meets the required societal risk thresholds.

Probably not a substantial claim: may not pass S2 (checkable).

GS AI is a potential avenue for feasibly obtaining such safety guarantees.

“We have also introduced GS AI as a potential avenue for feasibly obtaining such safety guarantees, discussed the main challenges with this research agenda, and some ways in which those challenges may be overcome.”

Probably not a substantial claim: may not pass S4 (based).

GS AI can produce proof certificates verifying that a given solution conforms to auditable-to-all-parties specifications, in a way that requires minimal trust among the parties.

“This is because GS AI is able to produce proof certificates verifying that a given solution conforms to auditable-to-all-parties specifications, in a way that requires minimal trust among said parties.”

Probably not a substantial claim: may not pass S2 (checkable).

GS AI approaches have the potential to play a critical role in securing critical infrastructure, thereby drastically bolstering civilisational resilience to both accidents and adversarial threats.

“GS AI approaches have the potential to play a critical role in securing such critical infrastructure, thereby drastically bolstering civilisational resilience to both accidents and adversarial threats.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

To specify or learn world models which are interpretable and expressive enough for GS AI, an appropriately rich formal representation is necessary.

“To specify or learn world models which are interpretable and expressive enough for GS AI, an appropriately rich formal representation is necessary.”

Classified as probably not a substantial claim. May combine two claims.

Computational learning theory is typically concerned with guarantees concerning narrow performance metrics, whereas GS AI is additionally concerned with specifications that would provide strong safety assurances for advanced systems operating in open-ended environments.

“However, CLT is typically concerned with guarantees concerning narrow performance metrics, whereas we are additionally concerned with specifications that would provide strong safety assurances for advanced systems operating in open-ended environments.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

The usage of powerful AI is likely to itself create situations that are novel and unprecedented.

“Note that the usage of powerful AI is likely to itself create situations that are novel and unprecedented, which makes this a point of particular importance.”

Probably not a substantial claim: may not pass S3 (load-bearing).

GS AI is more broadly related to the field of safety engineering, an area of engineering science that focuses on identifying, evaluating, and mitigating potential hazards and risks associated with various systems and processes.

“GS AI is more broadly related to the field of safety engineering, an area of engineering science that focuses on identifying, evaluating, and mitigating potential hazards and risks associated with various systems and processes.”

• cites Ericson (2015)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Leveson (2012) sourceNot checked — no full text of the source
• cites Dhillon (2003)Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S2 (checkable).

In order for it to be possible to completely satisfy the specification, it must at least be conceivable, i.e., the specification's level of satisfaction needs to be bounded at least in theory.

“In order for it to be possible, it must at least be conceivable, i.e., the specification's level of satisfaction needs to be bounded at least in theory.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based). May combine two claims.

The world model need not make predictions about arbitrary properties of the world, and even about properties on which they do make predictions, these predictions need not necessarily be precise.

“Also note that the world model need not make predictions about arbitrary properties of the world, and even about properties on which they do make predictions, these predictions need not necessarily be precise.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Computational learning theory is concerned with deriving formal guarantees for AI systems.

“Like the GS approach to AI safety, CLT is also concerned with deriving formal guarantees for AI systems.”

Probably not a substantial claim: may not pass S3 (load-bearing).

There is a large literature on formal verification of AI-enabled systems.

“There is also a large literature on formal verification of AI-enabled systems.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

A world model with a more abstract state-space may make it easier to express certain safety specifications, or make verification more tractable, but this may come at the cost of making the predictions less accurate.

“Note that a world model with a more abstract state-space may make it easier to express certain safety specifications, or make verification more tractable, but that this may come at the cost of making the predictions less accurate.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Many proposed safety specifications require recognizing when harm occurs.

“Many proposed safety specifications require recognizing when harm occurs.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

A limitation of classical automated planners is that they operate over deterministic world models which only admit Boolean variables.

“A limitation of classical automated planners is that they operate over deterministic world models which only admit Boolean variables.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

Implementing the causal definition of harm in a complex world model to meaningfully cover the utilities, the downstream implications of an event, etc. is a challenge.

“However, we do think this is just a starting point; implementing this in a complex world model to meaningfully cover the utilities, the downstream implications of an event, etc. are, to put it mildly, a challenge.”

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

It should be possible to completely satisfy the specification in order to relieve optimisation pressure.

“The reason for this requirement is that it should be possible to completely satisfy the specification in order to relieve optimisation pressure.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The formal verification of AI-enabled systems literature builds on more classic work on formal verification of control policies and classical expert systems, to develop methods for formal verification of neural networks and other machine learning systems.

“This builds on more classic work on formal verification of control policies (e.g., (Tabuada, 2009)) and classical expert systems (O'Keefe & O'Leary, 1993), to develop methods for formal verification of neural networks and other machine learning systems.”

• cites Tabuada, 2009 sourceNot checked — no full text of the source
• cites O'Keefe & O'Leary, 1993 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

Much work remains to fully develop the GS approach.

“Much work remains to fully develop the GS approach.”

Classified as probably not a substantial claim.

GS AI aims to ensure the safety of AI systems by equipping them with formal, verifiable and auditable safety guarantees.

“GS AI aims to ensure the safety of AI systems by equipping them with formal, verifiable and auditable safety guarantees.”

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

With a concerted research effort on the core technical problems, significant progress could be made.

“With a concerted research effort on the core technical problems, significant progress could be made.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The core idea behind correct-by-construction synthesis is to use formal methods to systematically construct programs that satisfy a given set of formal specifications or correctness properties.

“The core idea behind correct-by-construction synthesis is to use formal methods to systematically construct programs that satisfy a given set of formal specifications or correctness properties.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Automated theorem proving and automated planning both study methods for efficient automated reasoning over formal models.

“Related to program synthesis are the fields of automated theorem proving (Loveland, 2016) and automated planning (Ghallab et al., 2004).Both areas study methods for efficient automated reasoning over formal models, with the former focused on reasoning over mathematical theories and program logics, and with the latter, by analogy (Fikes & Nilsson, 1971), focused on reasoning over theories of”

• cites Loveland, 2016Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Ghallab et al., 2004Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Fikes & Nilsson, 1971 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S4 (based). May combine two claims.

Creating accurate and interpretable world models, formulating precise safety specifications, and performing formal verification at scale are all difficult problems.

“Creating accurate and interpretable world models, formulating precise safety specifications, and performing formal verification at scale are all difficult problems.”

Probably not a substantial claim: may not pass S4 (based). May combine two claims.

Empiricism and interpretability are useful tools, but they do not provide the strong safety assurances that formal verification can.

“While empiricism and interpretability are useful tools, they do not provide the strong safety assurances that formal verification can.”

Probably not a substantial claim: may not pass S2 (checkable).

The GS approach may be necessary given the serious limitations of other methods such as empirical testing and interpretability.

“Furthermore, the GS approach may be necessary given the serious limitations of other methods such as empirical testing and interpretability.”

Probably not a substantial claim: may not pass S2 (checkable). May combine two claims.

Although formal verification is challenging, the GS research program offers a promising path toward making it feasible at scale.

“Although formal verification is challenging, the GS research program offers a promising path toward making it feasible at scale.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Correct-by-construction synthesis is typically achieved by encoding the specifications as logical formulas or constraints, and then using automated solvers or synthesis algorithms to derive programs that provably satisfy those constraints.

“This is typically achieved by encoding the specifications as logical formulas or constraints, and then using automated solvers or synthesis algorithms to derive programs that provably satisfy those constraints.”