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∗1024∗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!!!
Note that effectively we are saying to trust the neural network
I expect that we’re going to have to rely on some neural networks regardless of how we approach AI. This paper guides us to be more strategic about what reliance to put on which neural networks.
Fortunately, for coarse “guardrails” the specs are pretty simple and can often be reused in many contexts. For example, all software we want to run should have proofs that: 1) there aren’t memory leaks, 2) there aren’t out-of-bounds memory accesses, 3) there aren’t race conditions, 4) there aren’t type violations, 5) there aren’t buffer overflows, 6) private information is not exposed by the program, 7) there aren’t infinite loops, etc. There should be a widely used “metaspec” for those criteria which most program synthesis AI will have to prove their generated code satisfies. Similarly, there are common constraints for many physical systems: eg. robots, cars, planes, boats, etc. shouldn’t crash into things or harm humans, etc. The more refined the rules are, the more subtle they become. To prevent existentially bad outcomes, I believe coarse constraints suffice. But certainly we eventually want much more refined models of the world and of the outcomes we seek. I’m a fan of “Digital Twins” of physical systems which allow rules and constraints to be run in simulation which can help in choosing specifications. We certainly want those simulations to be trusted. which can be achieved by proving the code actually simulates the systems it claims to. Eventually it would be great to have fully trusted AI as well! Mechanistic Interpretability should be great for that! I’m just reading Anthropic’s recent nice advances in that. If that continues to make progress then it makes our lives much easier but it doesn’t eliminate the need to ensure that misaligned AGI and malicious AGI don’t cause harm. The big win with the proof checking and the cryptographic hardware we propose is that we can ensure that even powerful systems will obey rules that humanity selects. If we don’t implement that kind of system (or something functionally equivalent), then there will be dangerous pathways which malicious AGI can exploit to cause great harm to humans.
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∗1024∗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!!!
I expect that we’re going to have to rely on some neural networks regardless of how we approach AI. This paper guides us to be more strategic about what reliance to put on which neural networks.
Fortunately, for coarse “guardrails” the specs are pretty simple and can often be reused in many contexts. For example, all software we want to run should have proofs that: 1) there aren’t memory leaks, 2) there aren’t out-of-bounds memory accesses, 3) there aren’t race conditions, 4) there aren’t type violations, 5) there aren’t buffer overflows, 6) private information is not exposed by the program, 7) there aren’t infinite loops, etc. There should be a widely used “metaspec” for those criteria which most program synthesis AI will have to prove their generated code satisfies. Similarly, there are common constraints for many physical systems: eg. robots, cars, planes, boats, etc. shouldn’t crash into things or harm humans, etc. The more refined the rules are, the more subtle they become. To prevent existentially bad outcomes, I believe coarse constraints suffice. But certainly we eventually want much more refined models of the world and of the outcomes we seek. I’m a fan of “Digital Twins” of physical systems which allow rules and constraints to be run in simulation which can help in choosing specifications. We certainly want those simulations to be trusted. which can be achieved by proving the code actually simulates the systems it claims to. Eventually it would be great to have fully trusted AI as well! Mechanistic Interpretability should be great for that! I’m just reading Anthropic’s recent nice advances in that. If that continues to make progress then it makes our lives much easier but it doesn’t eliminate the need to ensure that misaligned AGI and malicious AGI don’t cause harm. The big win with the proof checking and the cryptographic hardware we propose is that we can ensure that even powerful systems will obey rules that humanity selects. If we don’t implement that kind of system (or something functionally equivalent), then there will be dangerous pathways which malicious AGI can exploit to cause great harm to humans.