Provably Safe AI

Thanks for this write-up, Peter! 

Here's an interview I released yesterday with Omohundro on this paper: 
 

As a few commenters have already pointed out, this "strategy" completely fails in step 2 ("Specify safety properties that we want all AIs to obey"). Even for a "simple" property you cite, "refusal to help terrorists spread harmful viruses", we are many orders of magnitude of descriptive complexity away from knowing how to state them as a formal logical predicate on the I/O behavior of the AI program. We have no clue how to define "virus" as a mathematical property of the AI sensors in a way that does not go wrong in all kinds of corner cases, even less clue for "terrorist", and even less clue than that for "help". The gap between what we know how to specify today and the complexity of your "simple" property is way bigger than the gap between the "simple" property and most complex safety properties people tend to consider...

To illustrate, consider an even simpler partial specification - the AI is observing the world, and you want to formally define the probability that it's notion of whether it's seeing a dog is aligned with your definition of a dog. Formally, define a mathematical function of $3\ast 1024\ast 1020$ arguments that, with the arguments representing the RGB values for a 1024x1024 image, would capture the true probability that the image contains what you consider to be a dog - so that a neutral network that is proven to compute that particular function can be trusted to be aligned with your definition of a dog, while a neutral network that does something else is misaligned. Well, today we have close to zero clue how to do this. The closest we can do is to train a neutral network to recognize dog pictures, and than whatever function that network happens to compute (which, if written down as a mathematical function, would be an incomprehensible mess that, even if we optimize to reduce the size of, will probably tbe at least thousands of pages long) is the best formal specification we know how to come up with. (For things simpler than dogs we can probably do better by first defining a specification for 3d shapes, then projecting it onto 2d images, but I do not think this approach will be much help for dogs). Note that effectively we are saying to trust the neural network - whatever it learned to do is our best guess on how to formalize what it needed to do! We do not yet know how to do better!!!

Thanks Peter for the post and thank you everyone for the comments. Let me try to clarify a bit. We're looking for an absolute foundation of trust on top of which we can build a world safe for AGI. We believe that we need to adopt a "Security Mindset" in which AGI's either on their own or controlled by malicious humans need to be considered a full on adversaries. The only two absolute guarantees that we have are mathematical proof and the laws of physics. Even the most powerful AGI can't prove a falsehood or violate the laws of physics. Based on these we show how to build a network of "provable contracts" that provide absolute guardrails around dangerous actions. As a commenter points out, figuring out which actions we need to protect against and what the rules should be is absolutely essential and not at all trivial! In fact, I believe that should be one of the primary activities of humanity for the next decade! 

From the paper:

AI is allowed to write the code and proof, but not the proof-checker.

Some examples from the paper of things to be proved are "this plane will not fly into buildings" (p.3), "this drone flies safely" (p.2), and "this social media account is human" (p.2). Somehow a formal specification is made of such things, and the proof-checker verifies that the proof indeed proves that the code satisfies the formal specification.

The only suggestion that the paper makes of how to make a formal specification is by citing its reference 94, "Autoformalization with Large Language Models". I have not read it, but the title implies that its answer is to have an AI do it. Where do you get an AI that is safe enough to be trusted with that?

Putting the two papers together, the scheme is:

1. Give one AI a specification like "no-one can fly this plane into a building".

2. Have the AI come up with a formal specification of what that means.

3. A second AI generates avionics software to satisfy that specification and a purported proof that it does so.

4. Run the specification, the code, and the proof through a dumb proof-checker.

5. The code has been proved safe! Run it.

The second AI does not have to be safe, because the code it generates will not be run unless it passes step 4. But what about the first AI? The entire safety issue is still there. How can we assure ourselves that the formal specification that it generates actually describes what we really wanted? Especially if "no-one can fly this plane into a building" turns into a vast pile of mathematics as impenetrable as any neural network's weight matrices.

How do you stop someone doing the same with a different spec, "this plane will fly into any building I tell it to"?

It's not a silver bullet, but not useless either. In software verification, there are many safety properties that are valuable to have, but they never guarantee safety in ways that are not captured in their formulation. Similarly, the task of formulating safety of AI systems in formal properties is hopeless in its ambitious form but could be extremely useful piecemeal, when AI systems are structured as modular software instead of as monolithic models.

Examples adjacent to where such methods might become relevant are Conjecture's CoEm and Drexler's CAIS [LW · GW]. AIs built for a particular purpose that avoid escalation of their capabilities, or respect boundaries [LW · GW] in their impact.

This also gets agent foundations a handhold in practical AI systems, ability to robustly implement particular laws of behavior. So not a solution to ambitious alignment, but rather tools for building systems that might eventually get us there, for keeping such systems tractable and bounded in particular ways.

Thank you for writing this review.

The strategy assumes we'll develop a good set of safety properties that we're demanding proof of.

I think this is very important. From skimming the paper it seems that unfortunately the authors do not discuss it much. I imagine that actually formally specifying safety properties is actually a rather difficult step.

To go with the example of not helping terrorists spread harmful virus: How would you even go about formulating this mathematically? This seems highly non-trivial to me. Do you need to mathematically formulate what exactly are harmful viruses?

The same holds for Asimov's three laws of robotics, turning these into actual math or code seems to be quite challenging.

There's likely some room for automated systems to figure out what safety humans want, and turn it into rigorous specifications.

Probably obvious to many, but I'd like to point out that these automated systems themselves need to be sufficiently aligned to humans, while also accomplishing tasks that are difficult for humans to do and probably involve a lot of moral considerations.

I'm skeptical because in addition to logical reasoning, intuitive reasoning seems pretty important. And I'm not sure if there's a simpler representation of intuitive reasoning that a bunch of weights from a bunch of concepts to another concept.

Peter, thanks again for starting this discussion! Just a few caveats in your summary. We don't depend on trustable AIs! One of the absolutely amazing and critical characteristics of mathematical proof is that anybody, trusted or not, can create proofs and we can check them without any need to trust the creator. For example, MetaMath https://us.metamath.org/ defines an especially simple system for which somebody has written a 350 line Python proof checker which can check all 40,000 MetaMath theorems in a few seconds. We need to make sure that that small Python program is correct but beyond that don't need to trust any AIs! It certainly would be nice to have trustable AIs but I think it is a mistake to depend on them. We are already seeing a wide range of open source AIs created by different groups with different intentions. And there are many groups working to remove the safety features of commercial Large Language Models and text-to-image models. 

The core of our proposal is to put provable guardrails around dangerous technologies that AGI might seek to control. As many commenters have pointed out we need to figure out what those are! Some current examples include DNA synthesis machines, nukes, military hardware of all kinds, drones capable of dispersing dangerous payloads, etc.  And we need to create rules for which actions with these systems are safe! But we already do that today for human use. The CDC has detailed rules for biohazard labs. The initial implementation of our proposal will most likely be digitally checkable versions of those existing human rules. But certainly we need to extend them to the new environment as AIs become more powerful. Any action remotely capable of human extinction should become a primary focus. I believe establishing the rules for high risk actions should be an immediate priority for humanity. And extending those rules to other systems to enable human flourishing should be a close second.

We can use untrusted AIs in much of this work! We simply require them to generate formal proofs of any designs or software that they create. These can then be easily and rigorously checked and they can be used without concern for the properties of the AI which generated them.

Perhaps it is best to develop AI systems that we can prove theorems about in the first place. AI systems that we can prove theorems about are more likely to be interpretable anyways. Fortunately, there are quite a few theorems about maxima and minima of functions including uniqueness theorems including the following.

Theorem: (maximum principle) If $C\subseteq R^n$ is a compact set, and $f:C\to [-\infty ,\infty )$ is an upper semicontinuous function that is subharmonic on the interior $C^{\circ }$, then ${max}_{x\in C}f\left(x\right)={max}_{x\in \partial C}f\left(x\right)$.

If $U$ is a bounded domain, and $f:U\to R$ is a $C^1$-function, then define the Dirichlet energy of $f$ as 

$E\left(f\right)=\frac{1}{2}\cdot {\int }_U\parallel \left(\nabla f\right)\left(x\right){\parallel }^{2}dx$. 

Theorem: (Dirichlet principle) If $C$ is a compact subset of $R^n$, then whenever $g:\partial C\to R$ is continuous and $f:C\to R$ is a continuous function which is harmonic on $C^{\circ }$ and where $f{|}_{\partial C}=g$, then $f$ is the $C^2$-function that minimizes the Dirichlet energy $E\left(f\right)$ subject to the condition that $f{|}_{\partial C}=g$.

Theorem: (J Van Name: A version of the Cauchy-Schwarz inequality) Suppose that $A_1,\dots ,A_r\in M_n\left(C\right)$ which have no invariant subspace and $A_1{A}_1^{\ast }+\cdots +A_r{A}_r^{\ast }=1_n$. Suppose furthermore that $L:M_n\left(C\right)\to R$ is the partial function where $L(X_1,\dots ,X_r)=\frac{\rho (A_1\otimes (X_1^{\ast }{)}^T+\cdots +A_r\otimes \left(X_r^{\ast }{)}^T\right)}{\rho (X_1\otimes (X_1^{\ast }{)}^T+\cdots +X_r\otimes (X_r^{\ast }{)}^T{)}^{1/2}}$. Then $L(X_1,\dots ,X_r)\le 1$ and $L(X_1,\dots ,X_r)=1$ if and only if there is some non-zero complex number $\lambda$ and invertible matrix $C$ with $X_j=\lambda C{A}_j{C}^{-1}$ for $1\le j\le r$. Here, $\rho \left(X\right)$ denotes the spectral radius of a matrix $X$.

Right now, there are some AI systems related to the above theorems. For example, if we are given a graph, then the smallest eigenvalues of the Laplacian of a graph form clusters in your graph, so spectral techniques can be used to analyze graphs, but I am working on developing spectral AI systems with more advanced capabilities. It will take some time for spectral AI systems to catch up with deep neural networks while retaining their mathematical properties (such as fitness functions with an almost unique local maximum), but it is plausible that the development of spectral AI systems is mostly a matter of engineering and hard work rather than a problem of possibility, but I am not sure whether spectral AI systems will be as energy efficient as neural networks once well developed.

I don't like to be negative, but I'm almost completely certain that provable safe A.I. is impossible, by which I mean that it must contain a contradiction.

The problem is impossible already for humans, safety vs freedom, the problem of defining "good" and "evil", giving somebody the ability to protect themselves while also making sure that they won't harm others, having a system which prevents itself from its own corruption (protects itself against itself). And wouldn't world domination look exactly the same as an AI enforcing peace and safety? These two would require the same amount of power and control, i.e. they're basically the same thing seen from two different perspectives.

As far as I know, the Three Laws of Robotics aren't perfect, nor has anyone yet been able to come up with a workable (by which I mean perfect/failproof) set of rules. There seems to be a contradiction here, as if you're making a system which is stronger than itself. Even if you can prove that a system has a certain property, shouldn't you first be able to define such a property?

It's my belief that we have never come up with a good solution in any instances of this problem. Philosophical, moral, legal, political, you name it. Even the "paradox of tolerance", an idea that I don't consider very well thought out, seems to point at a fundemental problem. There's no unique origin/root/beginning which we can rely on (base things on, compare things against), no universal system, there's only relativity/perspectivism.

This generalizes. What's the fundemental axioms of mathematics? No unique answer exists. What's the beginning of everything? What's the center of the universe? As usual, the question itself is wrong. This problem of alignment seems to attempt to answer a global problem from a local perspective, which is like solving a subjective problem objectively, or asking a formal system to prove itself, or expecting a human being to escape their own programming and biases. You could argue for a proof by construction, for if everything acts as one object then there can't be any disagreements between objects. But even in individual people, there's many internal conflicts going on, we're not even aligned with ourselves. And even if we managed to steer humanity into a fixed point, I think we'd get stuck there forever, with a provable inability to exit again (which I think would make it unsafe). If you only bound the AI, you can't prove that malicious actors can't modify it and make it unsafe, for that would also mean that good actors wouldn't be able to modify a malicious system and make it safe.

I realize that this looks like the comment of somebody who is mentally unwell, but I'm confident there's a solid argument in there somewhere.