Provably safe systems: the only path to controllable AGI

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

For many tasks, ML is now better than humans at Step 1 (discovering algorithms and knowledge).

“Traditionally, all four steps have been performed by humans, but for many tasks, ML is now better than humans at Step 1.”

May combine two claims.

Corporations and research labs are racing to build AGI despite warnings it may lead to human extinction.

“corporations and research labs are racing to build AGI despite prominent AI researchers and business leaders warning that it may lead to human extinction [11].”

• cites [11]Not matched

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

May combine two claims.

Alignment is valuable but inadequate for human safety, especially given open-source AI that can be used maliciously.

“While this is valuable, we believe it is inadequate for human safety, especially given the profusion of open-source AI that can be used maliciously.”

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

Provably safe systems could counteract each of the catastrophic AI risks described by CAIS.

“Provably safe systems could counteract each of the risks they describe.”

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

The design and creation of provably safe AGI and infrastructure is extremely valuable and can become increasingly routine to implement, thanks to AI-powered advances in automated theorem proving and mechanistic interpretability.

“The design and creation of provably safe AGI and infrastructure is both extremely valuable and can become increasingly routine to implement, thanks to AI-powered advances in automated theorem proving and mechanistic interpretability.”

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

Regardless of intelligence, a system cannot prove a mathematical falsehood or do what is provably impossible.

“Regardless of how intelligent a system becomes, it cannot prove a mathematical falsehood or do what is provably impossible.”

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

These capabilities will only improve in coming years, and AGIs will eventually surpass the very best humans in each of these areas.

“These capabilities will only improve in coming years, and we should expect AGIs to eventually surpass the very best humans in each of these areas.”

May combine two claims.

The behavior of physical, digital, and social systems can be precisely modeled as formal systems and precise guardrails can be defined that constrain what actions can occur.

“The behavior of physical, digital, and social systems can be precisely modeled as formal systems and precise “guardrails” can be defined that constrain what actions can occur.”

May combine two claims.

Current LLMs can write code, prove theorems, design molecules, reverse engineer, plan attacks, deceive, and manipulate people, read and reason about every human text, recording, and video.

“Current Large Language Models (LLMs) [51] can write code [22], prove theorems [70], design molecules [29], reverse engineer [67], plan attacks [86], deceive [82] and manipulate people [75], read and reason about every human text, recording, and video, etc.”

• cites [51]Not matched

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

• cites [22]Not matched

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

• cites [70]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), S4 (based).

Building AGIs to provably satisfy human-specified requirements is the only path which guarantees safe controlled AGI.

“We further argue that it is the only path which guarantees safe controlled AGI.”

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

Mathematical proofs are cheap to check with inexpensive, extremely reliable hardware.

“And mathematical proofs are cheap to check with inexpensive, extremely reliable hardware.”

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

This path will soon be technically feasible using advanced AI for formal verification and mechanistic interpretability.

“We argue that this will soon be technically feasible using advanced AI for formal verification and mechanistic interpretability.”

May combine two claims.

If a mathematical proof of safety doesn't exist, then it is very likely that malicious AGIs will find the vulnerabilities and exploit them.

“If a mathematical proof of safety doesn't exist, then it is very likely that malicious AGIs will find the vulnerabilities and exploit them [37].”

• cites [37]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).

Networks of devices can be better able to detect and prevent intrusion and to be robust in the face of attacks.

“Networks of devices can be better able to detect and prevent intrusion and to be robust in the face of attacks.”

May combine two claims.

Passing evaluations that screen for known risks are a necessary but not sufficient condition for safety.

“passing evaluations that screen for known risks are a necessary but not sufficient condition for safety.”

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

The level of intelligence needed to convert all of one's own black-box knowledge into code has to be at least at AGI-level.

“Since we humans are the only species that can do this fairly well, it may unfortunately be the case that the level of intelligence needed to be able to convert all of one's own black-box knowledge into code has to be at least at AGI-level.”

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

The only absolutely trustable information comes from mathematical proof.

“The only absolutely trustable information comes from mathematical proof.”

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

Proof-carrying AGI running on PCH appears to be the only hope for a guaranteed solution to the control problem: no matter how superintelligent an AI is, it can't do what's provably impossible.

“Proof-carrying AGI running on PCH appears to be the only hope for a guaranteed solution to the control problem: no matter how superintelligent an AI is, it can't do what's provably impossible.”

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

Absence of evidence of risk is not evidence of its absence.

“Absence of evidence of risk isn't evidence of its absence.”

May combine two claims.

Since even our largest computers have only a finite number of states, if some safety property doesn't have a proof, then there must be a way to violate it.

“Since even our largest computers have only a finite number of states, this implies that if some safety property doesn't have a proof, then there must be a way to violate it.”

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

A major effort toward requiring AI to synthesize proof-carrying code can produce immediate improvements in AI safety and provide great societal value more generally, while taking steps toward solving the proof-carrying AGI challenge.

“These examples show that a major effort toward requiring AI to synthesize proof-carrying code can produce immediate improvements in AI safety (and provide great societal value more generally), while at the same time taking valuable steps toward solving the proof-carrying AGI challenge.”

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

Neural networks aren't necessary for efficiently executing PCC, because there are plenty of efficient massively parallel computational architectures that can run proof-carrying code on today's and tomorrow's GPU server infrastructure.

“Neural networks aren't necessary for efficiently executing PCC, because there are plenty of efficient massively parallel computational architectures that can run proof-carrying code on today's and tomorrow's GPU server infrastructure.”

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

Even the most powerful AGI can't fake safety by proving an incorrect theorem, and theorems can be cheaply and reliably checked.

“Even the most powerful AGI can't fake safety by proving an incorrect theorem, and theorems can be cheaply and reliably checked.”

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

Provable contracts can control the operation of devices such as drones, robots, GPUs and manufacturing centers.

“Provable contracts can control the operation of devices such as drones, robots, GPUs and manufacturing centers.”

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

Control of the GPU/factory/supply chain sector can be used to limit the rate of advancement of frontier AGI.

“Control of this sector can be used to limit the rate of advancement of frontier AGI.”

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

Guaranteed security against adversarial AGI requires Provably Compliant Hardware (PCH), with precise proofs and mathematical models in the style of theoretical cryptography.

“Guaranteed security against adversarial AGI requires the aforementioned Provably Compliant Hardware (PCH), with precise proofs and mathematical models in the style of those used today in theoretical cryptography.”

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

If current trends continue, we may soon routinely use AI to prove program properties vastly faster and better than is possible today.

“If current trends continue, then just as AI has already overtaken human ability in so many other domains, we may soon routinely use AI to prove program properties vastly faster and better than is possible today.”

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

In the last year, the field of Mechinterp has made more fundamental progress than all of traditional neuroscience combined, despite having orders of magnitude fewer researchers.

“In the last year, the field has made more fundamental progress than all of traditional neuroscience combined, despite having orders of magnitude fewer researchers.”

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

We may be on the cusp of a revolution in automated theorem proving, with LLMs and other AI tools showing signs of catching up with and overtaking humans in theorem-proving ability.

“However, we may be on the cusp of a revolution here, with large language models and other AI tools showing signs of catching up with and overtaking humans in theorem-proving ability.”

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

In an adversarial setting it is very easy to manipulate beliefs and to manufacture or manipulate evidence.

“But in an adversarial setting it is very easy to manipulate beliefs and to manufacture or manipulate evidence.”

May combine two claims.

Proofs of safety can be verified in advance or in real time as actions are occurring.

“Proofs of safety can be verified in advance or in real time as actions are occurring.”

May combine two claims.

When Meta allowed academic researchers access to a powerful language model, the weights were leaked within a week and distributed on bit torrent.

“When Meta allowed academic researchers access to a powerful language model, the weights were leaked within a week [92] and were then distributed on bit torrent.”

• cites [92]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), S4 (based). May combine two claims.

We still lack fully automated code-verifying AI powerful enough for the provably safe AI vision, but given the rate AI is advancing, we are hopeful that it will soon be available.

“In summary, we still lack fully automated code-verifying AI powerful enough for our provably safe AI vision, but given the rate AI is advancing, we are hopeful that it will soon be available.”

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

Provably safe infrastructure could stop the described bioterrorism attack at every stage.

“But provably safe infrastructure could stop this kind of attack at every stage: biochemical design AI would not synthesize designs unless they were provably safe for humans, data center GPUs would not execute AI programs unless they were certified safe, chip manufacturing plants would not sell GPUs without provable safety checks, DNA synthesis machines would not operate without a proof of safety,”

May combine two claims.

Current AI does not yet have all of the capabilities required for provably safe systems, but trends suggest that it soon will.

“Current AI does not yet have all of the capabilities we require, but trends suggest that it soon will.”

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

For provably safe infrastructure to solve the AGI safety problem, we need AI to build these systems rapidly and at scale.

“But for provably safe infrastructure to solve the AGI safety problem, we need AI to build these systems rapidly and at scale.”

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

The seemingly magical power of neural networks comes not from their ability to execute, but from their ability to learn.

“First, note that the seemingly magical power of neural networks comes not from their ability to execute, but from their ability to learn.”

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

If a GPU is PCH, then it should be unable to run anything but PCC meeting the GPU's specifications.

“If a GPU is PCH, then it should be unable to run anything but PCC meeting the GPU's specifications.”

May combine two claims.

RLHF is valuable for increasing alignment with human values but is inadequate in an adversarial context.

“While this is valuable for increasing alignment with human values, it is inadequate in an adversarial context.”

• cites [92]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), S4 (based).

It is much harder to discover a proof than to verify it.

“It's much harder to discover a proof than to verify it.”

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

AI regulations would incentivize massive industry investments in AI safety, placing responsibility on those selling and deploying the technology.

“such AI regulations would incentivize (sorely needed!) massive industry investments in AI safety, placing the responsibility where it belongs: on those selling and deploying the technology.”

May combine two claims.

Neural networks will help with knowledge and algorithm discovery, program synthesis and proof discovery, but PCCs will generally not be neural networks.

“We consider it likely that neural networks will help with knowledge and algorithm discovery, program synthesis and proof discovery, but that PCCs will generally not be neural networks”

• AssumptionRests on an assumption: The inner workings of language models are too messy to lend themselves to easy formal verification.

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

The knowledge and algorithms used by proof-carrying code can be AI-discovered, extracted either through self-explaining AI or with mechanistic interpretability tools.

“The knowledge and algorithms used by the code can be AI-discovered, extracted either through self-explaining AI or with mechanistic interpretability tools.”

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

Mechanistic Interpretability has seen rapid recent progress.

“This AI subfield has seen rapid recent progress under the label “Mechanistic Interpretability” [77] (often shortened to “Mechinterp” or “MI”).”

• cites [77]Not matched

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

May combine two claims.

Formal verification is fundamentally a search problem: searching an exponentially large space of proof strings, but once a valid proof is found, it is trivial to verify.

“This means that formal verification is fundamentally a search problem: you're searching an exponentially large space of proof strings, but once you find a valid proof, it's trivial to realize that you've found one.”

May combine two claims.

LLMs aren't irreducible blobs, but share recurrent high-level circuits and motifs and can sometimes be decomposed into modules.

“LLMs aren't irreducible blobs, but share recurrent high-level circuits and motifs and can sometimes be decomposed into modules (computational “quanta”).”

• cites [20]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), S4 (based).

For physical security to withstand a superintelligent adversary, it needs to be provably secure.

“For physical security to withstand a superintelligent adversary, it needs to be provably secure.”

May combine two claims.

Because of improvements in hardware and machine learning since Necula, it is now feasible to expand the scope of PCC far beyond original applications such as type safety, since ML can discover proofs too complex for humans to create.

“Because of the dramatic improvements in hardware and machine learning [70] since George Necula first proposed PCC in his seminal 1998 thesis [1], it is now feasible to expand the scope of PCC far beyond its original applications such as type safety, since ML can discover proofs too complex for humans to create [3].”

• cites [70]Not matched

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

• cites [1]Not matched

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

• cites [3]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), S4 (based).

Once powerful AI's are tasked with Mechinterp, we may see yet another ML-powered revolution.

“Once powerful AI's are tasked with Mechinterp, we may see yet another ML-powered revolution.”

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

No matter how superintelligent an AI is, it cannot do what is provably impossible.

“no matter how superintelligent an AI is, it can't do what is provably impossible.”

May combine two claims.

Currently, the two really hard steps in PCC are generating code that meets specification and generating a proof that the code meets specification.

“Currently, the two really hard steps are 3 and 4.”

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

Such failure modes can be avoided with provable contracts implemented in secure hardware, with precisely specified conditions enabling each possible action.

“Such failure modes can be avoided with provable contracts implemented in secure hardware, with precisely specified conditions enabling each possible action.”

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

Networks of provable contracts have the potential to completely eliminate social dilemmas and to encourage win-win thinking and actions.

“Those have the potential to completely eliminate social dilemmas and to encourage win-win thinking and actions.”

• AssumptionRests on an assumption: It is possible to construct networks of provable contracts that expose each participant to the externalities caused by their actions.

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

A PCC-compliant operating system could implement a cache system where it remembers which proofs it has checked, thus needing to verify each code only the very first time it is used.

“a PCC-compliant operating system could implement a cache system where it remembers which proofs it has checked, thus needing to verify each code only the very first time it's used.”