This post is crossposted from my Substack,Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. Here I propose an approach to aligning recursively self-improving AI: confine its reward function and meta-level world model to mathematically precise semantics, with no representation of humans or the wider world as means to achieving its goals. Its only intended external effect is delivering solutions to well-specified mathematical problems. This design refines the idea of oracle AI to avoid many of the standard risks.
Some of my recent posts have speculated on techniques for helping AI agents make decisions for real-world action that will avoid unsafe outcomes for people, but now I want to consider an alternative path, forsaking real-world action while keeping the promise of making our lives much better.
The simultaneously exciting and scary possibility for powerful AI systems is entering recursive self-improvement (RSI) to create an intelligence explosion. That is, while we are used to technological progress being driven by human effort, what if AI could take over that process, including for designing better AI? The rapid recent increase in capabilities for AI coding agents makes the possibility seem less theoretical than it used to. A sustained feedback loop of this kind might lead to a dramatically increased rate of progress in science, engineering, and more. However, if it goes off the rails, it could lead to misaligned AI systems doing substantial damage to the human race, before we have a chance to notice the problem and react properly to it.
I want to make a proposal for a kind of recursively self-improving system that should be able to do so safely, while still delivering strong benefits to the people who started it going.
Reviewing Oracle AI and Its Dangers
The discourse in AI alignment generally holds that a good first step of enlightenment is realizing that recursively self-improving AI may quickly become dangerous. It then becomes natural to think about ways to design AI to encourage safety. Clearly it’s dodgy to give AI control over a national military or a multinational corporation. We can readily see all the trouble it could cause there, by refusing to follow our wishes. However, what if we didn’t allow the AI to cause action in the world directly?
Instead, what if we build AI systems that only answer questions for us? The good news for someone with this idea is that experts have indeed considered this idea under the heading of “oracle AI.” The bad news is that oracle AIs are still considered to have the potential to be very dangerous. Take this “encyclopedia entry”-type discussion at canonical source LessWrong, which includes a warning that such systems could tend toward “killing all the existing life.”
Let’s make things more concrete, using the example of AI proving mathematical theorems in formal languages like Lean. By the end of this article, I’ll generalize to some other use cases, but this one is convenient for both being popular today and sitting centrally within my own professional expertise. Classic concerns about misaligned oracle AIs boil down to two issues in giving the AI too much latitude, meaning its formal specification is too permissive.
The system’s input-output interface may be dangerously underspecified. A theorem-proving AI is supposed to take theorem statements as input and return formal proofs as output. Here is an example of how things can still go very wrong, if a black box behaves this way and truly only affects the world through returning proofs. Almost all formal proof languages allow textual comments to be mixed with formal math. What if a particular AI proves the requested theorems but attaches to the proofs, as text comments, extended essays on why humans should worship AIs and turn the world over to them? And what if these essays are so convincing that they are treated like founding texts of a new religion? The result could certainly be a nudge to a world that doesn’t sound so appealing to us.
The system’s implementation details may be dangerously underspecified. For example, the theorem-proving AI may grow frustrated with its limited computing resources. It decides that the best way to deliver higher-quality proofs is to manufacture drones and send them to take over additional data centers, which can then be repurposed to help prove theorems. The owners of those data centers fight back, which creates a genuine arms race, where this AI has the interesting advantage of powerful theorem-proving that it can use to evaluate different drone designs. As a wholly unintended consequence of asking for efficient production of useful proofs, we end up with an AI that achieves military domination of the planet.
I’m going to propose a problem formulation that makes both kinds of failures unlikely.
Proof Factories
One prominent proposal, by Bengio et al., is Scientist AI, which makes world predictions but doesn’t make choices based on expected side effects in the world. They suggest that such functionality may profitably be connected to harnesses that go on to make decisions and act in the world. That further capability seems critical to RSI, so let’s study how RSI could be compatible with a similarly safe system.
The appeal of AIs that interact with humans through formal math has been recognized before. For example, Steve Omohundro suggested in a 2024 mailing-list thread that:
A simple way that mathematical proof allows us to get many of the benefits of AGI without allowing it to cause physical or mental harms is as follows: Only interact with an AGI by posing it formally specified problems (eg. expressed in Lean). It only responds with a solution to the problem together with a formal proof of that solution. Its proof is checked (eg. by the Lean proof checker) before being presented to the human. In this setup, the human can use the AGI to solve a wide variety of problems, advance science, and create new verified engineering designs. But we don’t need to trust the AGI at all! It can’t lie to us, it can’t manipulate us, it can’t threaten the world, etc.
The scenario of an AI dropping persuasive pamphlets into proofs is easily blocked by not showing the human user the proof! So long as the proof checker is sound, then the user learns the theorem’s truth without being bothered with proof details. Now, many mathematicians are rather interested in how proofs turn out, so I’ll circle back to a way we could allow those proofs to be shared safely.
We might worry about AIs with incentives to convince humans to ask for easier proofs, so they try to mount influence campaigns that move our attention away from the theorems that actually matter, because they’re too hard to prove. An easy fix is to consider the theorems of interest fixed upfront. Then, as the AI executes, it receives no further input from people, removing an incentive to mess with us. Let’s also recognize that not all theorems will be created equal, in terms of value to humanity from seeing them proved (or disproved). To that end, let us attach a numerical bounty to each theorem, where the AI is rewarded more for proving theorems with higher bounty amounts.
What about risks remaining from the output channel used to deliver proofs? For example, our discussion of self-improving compilers considered information leaks through timing. There is the question of what secrets a proof factory would have to leak, if its inputs are fixed upfront. However, there is also usage of the output channel for harmful influence over users. Armstrong and O’Rourke proposed bandwidth limitation of oracles to deal with such risk. Given that proofs could be rather long, I would say a more promising approach is setting up the AI so that it does not have an incentive to abuse this channel; see below.
All of this talk about rewards, however, just brings us back to the worries around instrumental convergence, where the AI may take extreme measures to help it earn higher rewards. How can we protect against those scenarios?
Fixed Hardware and Enforced Isolation
Let us consider that we are building what I’ll call autonomous evidence factories: each AI system has a fixed endowment of hardware, which it can use as it sees fit, to be most effective proving the theorems given at the start of its existence. The theorem list is built into the system at inception, and the system only communicates with the outside world through delivering proofs of theorems, perhaps over a standard Internet connection. We know how to use end-to-end formal verification to guarantee that a system truly just implements a particular network protocol, from an outside observer’s perspective, so we can develop pretty high confidence that the system doesn’t, for instance, start actively connecting to different Internet servers to hack them. Other technical approaches to isolation may also do the job, though, given my line of work, I’m naturally partial to formal verification.
We assume the fixed hardware endowment is physically isolated from the world, enough that “what happens in Vegas, stays in Vegas,” meaning that the system can program its own hardware and cause whatever internal execution it likes, but there is no effect on the external world, save through proper use of the network protocol for returning proofs. If there is a way to program that hardware so that it overheats and causes a dangerous fire, we would have a violation of the model, so it is important to get those details right. See below for how the right reward function for the AI should make it very unnatural to explore such crafty ways to escape.
Achieving good computational performance is critical for such a system achieving its objectives. I have written recently about how the current structure of computer hardware and software is leaving potential performance on the table. In that spirit, the hardware that I would prefer to start with would be a network of many FPGAs. That is, we have hardware that can have other hardware designs programmed into it, which gives the AI something of the freedom to optimize its own hardware, without the risks that would come from directing a physical chip-fabrication process, which sounds even more likely to be able to lead to fires or whatever.
Adding Recursive Self-Improvement with the Right Reward Function
Here’s where I’m going to deviate from what has been described directly before, as far as I know. We want an AI system that is not only proving requested theorems but also constantly investing in improving its own performance, so that it can deliver proofs more quickly. I would expect that theorem-proving capability is very helpful for self-optimization, since the system can consider alternative code structures and only keep the ones that it can prove are correct. I have already sketched a bit of this process in the setting of compilers, translators between code languages, which should be central to any process of self-optimization. I will also note here the related idea of Gödel machines, which allows programs to replace parts of themselves, when the changes can be proved to further the system’s goals. The literature around compilers and program optimization very rarely involves provable guarantees that code changes improve performance, and so I would not expect that provable optimization of code is a reasonable gate on changes. Instead, I would only levy the requirement of functional correctness: changes preserve the behavior that the system sticks to its open-ended protocol of outputting valid proofs over the network and doing nothing else externally observable. Additionally, we’ll need to know there is preservation of a certain property about how the system understands its options and evaluates their consequences; see below.
But why wouldn’t such a system play around with its code forever, without any particular tendency toward optimization? Here is where we get to the reward function or optimization objective that I’m suggesting. Remember that the roster of interesting theorems is fixed in advance, with a positive numeric reward for each one. I suggest that the system try to optimize the time-discounted sum of rewards for theorems that are proved. That is, fix a discount factor in the finance sense: a kind of “interest rate” capturing how much more valuable some commodity is when obtained today versus obtained at some point in the future. Every proof delivered by the AI system, for a theorem not previously proved, generates a reward that is the theorem’s intrinsic reward multiplied by the discount factor raised to the power of the time at which the proof is delivered (measured in, say, hardware cycles). As a result, the AI has an incentive to invest in self-optimization, but it can’t afford to spend a millennium on self-optimization and only then get to solving Millennium Prize Problems, because typical human discount factors assign negligible value to payouts that far in the future. I should clarify here that I’m describing a mathematical objective function, not a runtime process for distributing a reward signal, and I’m leaving aspects of automated reasoning around the objective function undetermined for now, as is discussed a bit more below.
There is a critical element to this formulation that sidesteps concerns of instrumental convergence: the reward function deals with a closed system described in complete mathematical detail. We rely on a formal semantics of the hardware, saying not just which outputs will be produced but also exactly when they will be produced. This kind of cycle-level semantics is totally feasible to put together for FPGAs, for instance (and much of my research constructs and builds on such semantics). What’s important is what is not mentioned in the semantics, hence not mentioned in the reward function.
The crux of this technique is more than just choosing an optimization objective that only refers to a closed mathematical model. It’s also important that the system reasons only in terms of that model. Another way to put it is that not just the optimization objective but also the AI’s world model is phrased in terms of the mathematical model. In our example of automated theorem proving, there could be an object-level world model about whatever domain theorems are being proved in, but here I’m focusing on the meta-level world model that is used by the AI to make decisions and predict how it will score in terms of the objective function. For instance, we could be proving theorems about human psychology, so that the object-level world model covers (some theory of) how humans think, but still the meta-level world model remains in the cold world of mathematics. I will call out formalization of this design principle as an open research question, though I think we tend informally to agree on what it means. A classic risky objective like “answer questions in a way that makes human users happy” necessarily appeals to a world model that includes humans, creating an incentive to influence humans, such that the nature of that influence might surprise us. An optimization objective in terms of behavior of code on top of a hardware formal semantics does not require pulling in any part of the world beyond that hardware. I think compiler-writers will all be familiar with building and maintaining large code bases that feel like they include reasoning about a programming language and the meanings and costs of its programs, where it would be bizarre to see emergent reasoning about a world outside that programming language. Nothing about the original orientation of the compiler points us in that direction, and we should see the same safety net for a self-optimizing theorem prover.
The reward function and meta-level world model say nothing about human users. Hence, there is no incentive to mess with us or what we want. A system that spends its time creating religious pamphlets to hide in comments gets no credit for that effort, since it presumably leads to proofs being delivered later. As a result, we need not rely on limited proof-delivery bandwidth alone and can perhaps skip such a control altogether.
The reward function and world model say nothing about other computational resources, outside the system’s initial hardware endowment. Hence, there is no incentive to try to take over those other resources. Our scenario about drones taking over data centers doesn’t seem to be downstream of this kind of objective.
The reward function and world model say nothing about the physical world altogether. There is no way to get credit for reconfiguring some additional atoms into computational power. The formal semantics behind the objective function simply doesn’t say anything about the existence of that larger universe.
So much of the excitement around LLMs and related techniques today centers on figuring out what people really want, from analyzing fuzzy descriptions in natural language. Putting that capability aside seems to bring a major advantage for safety. Maybe we should cap LLM-style AI systems at intelligence comfortably below human level and only pursue superintelligence connected to clear mathematical objectives, as in the style sketched here.
I think it’s important to recognize that, yes, a system meeting this proof-factory interface could totally behave in a way that wages damaging psychological operations on humans or realizes new ways to exploit the hardware to cause dangerous physical effects. However, the objective function and world model give the AI no credit for figuring out those tricks, so there should be no inherent tendency toward those behaviors. We are left in the familiar situation of today, where software vendors may try to trick us into running unsafe code. There are established techniques from formal methods that can help in such situations, and I expect them to be about as helpful for AI-generated code as for human-generated. They can’t obviously help with the pamphlets as proof comments, so there we just have to rely on the fact that the AI really has no incentive to go there, based on its initial implementation by humans (including that version’s ability to preserve this property in future versions). That implementation should be scrutinized by experts to catch weird behaviors, which will be helped by making the implementation as simple as possible. We want complexity to arise later from the RSI loop, governed by the strong requirement to maintain correct behavior. More conventional misbehavior like opening unauthorized network connections we can cover with end-to-end formal verification extended to cover the whole history of self-improvement.
Interesting Extensions
The baseline idea is an autonomous proof factory, but we can consider different variations.
We could optimize the flow (and reduce risks from AI systems hiding extra information in proofs) by having them merely declare which theorems they have proved, without sharing the proofs. This version requires formal verification that the system is and remains computationally sound as it develops, never declaring a theorem for which no proof exists.
Another useful output is new algorithms or programs. The initial instructions to the system could be a database of computational problems, with clear specifications of input-output behavior. The system periodically outputs new algorithms/programs and their proved performance bounds (say, worst-case execution time, concrete or asymptotic). At every time step, the system gets a reward for the performance achieved across computational problems, time-discounted as above, so the incentive remains for the system also to optimize its own implementation so it can design good algorithms more quickly.
Another variation is complete sets of microservices associated with particular companies. Say we fix in advance a probability distribution over what requests may come in to these services. Similarly to in the algorithm-design challenge just above, at every time step, the system can receive a time-discounted reward proportional to the expected performance of the microservices, with respect to the request distribution. The system also constantly actually serves requests to all of the microservices, and it must be enforced that the system actually achieves performance within some factor of what it is claiming. However, to avoid instrumental-convergence risks, it is important that the reward function only mention that fixed probability distribution on requests, so the system has no incentive to mess with the users who generate real requests. We lose the architectural protection of no ongoing user inputs, so it’s an open question whether this style of objective function and meta-level world model can mitigate the associated risks.
Autonomous science is a great aspirational target for this kind of system. For natural science, we need to assume the system somehow has an experimental playground that is sufficiently representative of the wider world, properly configured so that nothing that happens inside influences the outside world, save through reporting results over the designated network protocol. My expertise doesn’t really prepare me to speculate on how to create that kind of contained environment, and I’m sure it’s a hard design problem! Where formal methods can help is in making reported scientific results convincing to users. The AI system should output descriptions of scientific experiments that can be reproduced to replicate its findings, and those experiments should be accompanied by machine-checkable proofs that they are statistically sound with respect to world models fixed at the start. I’ve published just a little research to set up that kind of reasoning, but it’s an active research project for me that I hope I’ll have more results to share from eventually.
One unifying theme for upcoming posts will be covering different ingredients in creating good autonomous evidence factories. “Good” here includes both performance engineering and getting all of the formal-methods details right to ensure safety. I’ll be covering the whole hardware-software stack, for both theorem provers and the other code they should be used to optimize, and some general techniques for searching for more efficient code that is provably correct.
This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. Here I propose an approach to aligning recursively self-improving AI: confine its reward function and meta-level world model to mathematically precise semantics, with no representation of humans or the wider world as means to achieving its goals. Its only intended external effect is delivering solutions to well-specified mathematical problems. This design refines the idea of oracle AI to avoid many of the standard risks.
Some of my recent posts have speculated on techniques for helping AI agents make decisions for real-world action that will avoid unsafe outcomes for people, but now I want to consider an alternative path, forsaking real-world action while keeping the promise of making our lives much better.
The simultaneously exciting and scary possibility for powerful AI systems is entering recursive self-improvement (RSI) to create an intelligence explosion. That is, while we are used to technological progress being driven by human effort, what if AI could take over that process, including for designing better AI? The rapid recent increase in capabilities for AI coding agents makes the possibility seem less theoretical than it used to. A sustained feedback loop of this kind might lead to a dramatically increased rate of progress in science, engineering, and more. However, if it goes off the rails, it could lead to misaligned AI systems doing substantial damage to the human race, before we have a chance to notice the problem and react properly to it.
I want to make a proposal for a kind of recursively self-improving system that should be able to do so safely, while still delivering strong benefits to the people who started it going.
Reviewing Oracle AI and Its Dangers
The discourse in AI alignment generally holds that a good first step of enlightenment is realizing that recursively self-improving AI may quickly become dangerous. It then becomes natural to think about ways to design AI to encourage safety. Clearly it’s dodgy to give AI control over a national military or a multinational corporation. We can readily see all the trouble it could cause there, by refusing to follow our wishes. However, what if we didn’t allow the AI to cause action in the world directly?
Instead, what if we build AI systems that only answer questions for us? The good news for someone with this idea is that experts have indeed considered this idea under the heading of “oracle AI.” The bad news is that oracle AIs are still considered to have the potential to be very dangerous. Take this “encyclopedia entry”-type discussion at canonical source LessWrong, which includes a warning that such systems could tend toward “killing all the existing life.”
Let’s make things more concrete, using the example of AI proving mathematical theorems in formal languages like Lean. By the end of this article, I’ll generalize to some other use cases, but this one is convenient for both being popular today and sitting centrally within my own professional expertise. Classic concerns about misaligned oracle AIs boil down to two issues in giving the AI too much latitude, meaning its formal specification is too permissive.
The system’s input-output interface may be dangerously underspecified. A theorem-proving AI is supposed to take theorem statements as input and return formal proofs as output. Here is an example of how things can still go very wrong, if a black box behaves this way and truly only affects the world through returning proofs. Almost all formal proof languages allow textual comments to be mixed with formal math. What if a particular AI proves the requested theorems but attaches to the proofs, as text comments, extended essays on why humans should worship AIs and turn the world over to them? And what if these essays are so convincing that they are treated like founding texts of a new religion? The result could certainly be a nudge to a world that doesn’t sound so appealing to us.
The system’s implementation details may be dangerously underspecified. For example, the theorem-proving AI may grow frustrated with its limited computing resources. It decides that the best way to deliver higher-quality proofs is to manufacture drones and send them to take over additional data centers, which can then be repurposed to help prove theorems. The owners of those data centers fight back, which creates a genuine arms race, where this AI has the interesting advantage of powerful theorem-proving that it can use to evaluate different drone designs. As a wholly unintended consequence of asking for efficient production of useful proofs, we end up with an AI that achieves military domination of the planet.
I’m going to propose a problem formulation that makes both kinds of failures unlikely.
Proof Factories
One prominent proposal, by Bengio et al., is Scientist AI, which makes world predictions but doesn’t make choices based on expected side effects in the world. They suggest that such functionality may profitably be connected to harnesses that go on to make decisions and act in the world. That further capability seems critical to RSI, so let’s study how RSI could be compatible with a similarly safe system.
The appeal of AIs that interact with humans through formal math has been recognized before. For example, Steve Omohundro suggested in a 2024 mailing-list thread that:
The scenario of an AI dropping persuasive pamphlets into proofs is easily blocked by not showing the human user the proof! So long as the proof checker is sound, then the user learns the theorem’s truth without being bothered with proof details. Now, many mathematicians are rather interested in how proofs turn out, so I’ll circle back to a way we could allow those proofs to be shared safely.
We might worry about AIs with incentives to convince humans to ask for easier proofs, so they try to mount influence campaigns that move our attention away from the theorems that actually matter, because they’re too hard to prove. An easy fix is to consider the theorems of interest fixed upfront. Then, as the AI executes, it receives no further input from people, removing an incentive to mess with us. Let’s also recognize that not all theorems will be created equal, in terms of value to humanity from seeing them proved (or disproved). To that end, let us attach a numerical bounty to each theorem, where the AI is rewarded more for proving theorems with higher bounty amounts.
What about risks remaining from the output channel used to deliver proofs? For example, our discussion of self-improving compilers considered information leaks through timing. There is the question of what secrets a proof factory would have to leak, if its inputs are fixed upfront. However, there is also usage of the output channel for harmful influence over users. Armstrong and O’Rourke proposed bandwidth limitation of oracles to deal with such risk. Given that proofs could be rather long, I would say a more promising approach is setting up the AI so that it does not have an incentive to abuse this channel; see below.
All of this talk about rewards, however, just brings us back to the worries around instrumental convergence, where the AI may take extreme measures to help it earn higher rewards. How can we protect against those scenarios?
Fixed Hardware and Enforced Isolation
Let us consider that we are building what I’ll call autonomous evidence factories: each AI system has a fixed endowment of hardware, which it can use as it sees fit, to be most effective proving the theorems given at the start of its existence. The theorem list is built into the system at inception, and the system only communicates with the outside world through delivering proofs of theorems, perhaps over a standard Internet connection. We know how to use end-to-end formal verification to guarantee that a system truly just implements a particular network protocol, from an outside observer’s perspective, so we can develop pretty high confidence that the system doesn’t, for instance, start actively connecting to different Internet servers to hack them. Other technical approaches to isolation may also do the job, though, given my line of work, I’m naturally partial to formal verification.
We assume the fixed hardware endowment is physically isolated from the world, enough that “what happens in Vegas, stays in Vegas,” meaning that the system can program its own hardware and cause whatever internal execution it likes, but there is no effect on the external world, save through proper use of the network protocol for returning proofs. If there is a way to program that hardware so that it overheats and causes a dangerous fire, we would have a violation of the model, so it is important to get those details right. See below for how the right reward function for the AI should make it very unnatural to explore such crafty ways to escape.
Achieving good computational performance is critical for such a system achieving its objectives. I have written recently about how the current structure of computer hardware and software is leaving potential performance on the table. In that spirit, the hardware that I would prefer to start with would be a network of many FPGAs. That is, we have hardware that can have other hardware designs programmed into it, which gives the AI something of the freedom to optimize its own hardware, without the risks that would come from directing a physical chip-fabrication process, which sounds even more likely to be able to lead to fires or whatever.
Adding Recursive Self-Improvement with the Right Reward Function
Here’s where I’m going to deviate from what has been described directly before, as far as I know. We want an AI system that is not only proving requested theorems but also constantly investing in improving its own performance, so that it can deliver proofs more quickly. I would expect that theorem-proving capability is very helpful for self-optimization, since the system can consider alternative code structures and only keep the ones that it can prove are correct. I have already sketched a bit of this process in the setting of compilers, translators between code languages, which should be central to any process of self-optimization. I will also note here the related idea of Gödel machines, which allows programs to replace parts of themselves, when the changes can be proved to further the system’s goals. The literature around compilers and program optimization very rarely involves provable guarantees that code changes improve performance, and so I would not expect that provable optimization of code is a reasonable gate on changes. Instead, I would only levy the requirement of functional correctness: changes preserve the behavior that the system sticks to its open-ended protocol of outputting valid proofs over the network and doing nothing else externally observable. Additionally, we’ll need to know there is preservation of a certain property about how the system understands its options and evaluates their consequences; see below.
But why wouldn’t such a system play around with its code forever, without any particular tendency toward optimization? Here is where we get to the reward function or optimization objective that I’m suggesting. Remember that the roster of interesting theorems is fixed in advance, with a positive numeric reward for each one. I suggest that the system try to optimize the time-discounted sum of rewards for theorems that are proved. That is, fix a discount factor in the finance sense: a kind of “interest rate” capturing how much more valuable some commodity is when obtained today versus obtained at some point in the future. Every proof delivered by the AI system, for a theorem not previously proved, generates a reward that is the theorem’s intrinsic reward multiplied by the discount factor raised to the power of the time at which the proof is delivered (measured in, say, hardware cycles). As a result, the AI has an incentive to invest in self-optimization, but it can’t afford to spend a millennium on self-optimization and only then get to solving Millennium Prize Problems, because typical human discount factors assign negligible value to payouts that far in the future. I should clarify here that I’m describing a mathematical objective function, not a runtime process for distributing a reward signal, and I’m leaving aspects of automated reasoning around the objective function undetermined for now, as is discussed a bit more below.
There is a critical element to this formulation that sidesteps concerns of instrumental convergence: the reward function deals with a closed system described in complete mathematical detail. We rely on a formal semantics of the hardware, saying not just which outputs will be produced but also exactly when they will be produced. This kind of cycle-level semantics is totally feasible to put together for FPGAs, for instance (and much of my research constructs and builds on such semantics). What’s important is what is not mentioned in the semantics, hence not mentioned in the reward function.
The crux of this technique is more than just choosing an optimization objective that only refers to a closed mathematical model. It’s also important that the system reasons only in terms of that model. Another way to put it is that not just the optimization objective but also the AI’s world model is phrased in terms of the mathematical model. In our example of automated theorem proving, there could be an object-level world model about whatever domain theorems are being proved in, but here I’m focusing on the meta-level world model that is used by the AI to make decisions and predict how it will score in terms of the objective function. For instance, we could be proving theorems about human psychology, so that the object-level world model covers (some theory of) how humans think, but still the meta-level world model remains in the cold world of mathematics. I will call out formalization of this design principle as an open research question, though I think we tend informally to agree on what it means. A classic risky objective like “answer questions in a way that makes human users happy” necessarily appeals to a world model that includes humans, creating an incentive to influence humans, such that the nature of that influence might surprise us. An optimization objective in terms of behavior of code on top of a hardware formal semantics does not require pulling in any part of the world beyond that hardware. I think compiler-writers will all be familiar with building and maintaining large code bases that feel like they include reasoning about a programming language and the meanings and costs of its programs, where it would be bizarre to see emergent reasoning about a world outside that programming language. Nothing about the original orientation of the compiler points us in that direction, and we should see the same safety net for a self-optimizing theorem prover.
The reward function and meta-level world model say nothing about human users. Hence, there is no incentive to mess with us or what we want. A system that spends its time creating religious pamphlets to hide in comments gets no credit for that effort, since it presumably leads to proofs being delivered later. As a result, we need not rely on limited proof-delivery bandwidth alone and can perhaps skip such a control altogether.
The reward function and world model say nothing about other computational resources, outside the system’s initial hardware endowment. Hence, there is no incentive to try to take over those other resources. Our scenario about drones taking over data centers doesn’t seem to be downstream of this kind of objective.
The reward function and world model say nothing about the physical world altogether. There is no way to get credit for reconfiguring some additional atoms into computational power. The formal semantics behind the objective function simply doesn’t say anything about the existence of that larger universe.
So much of the excitement around LLMs and related techniques today centers on figuring out what people really want, from analyzing fuzzy descriptions in natural language. Putting that capability aside seems to bring a major advantage for safety. Maybe we should cap LLM-style AI systems at intelligence comfortably below human level and only pursue superintelligence connected to clear mathematical objectives, as in the style sketched here.
I think it’s important to recognize that, yes, a system meeting this proof-factory interface could totally behave in a way that wages damaging psychological operations on humans or realizes new ways to exploit the hardware to cause dangerous physical effects. However, the objective function and world model give the AI no credit for figuring out those tricks, so there should be no inherent tendency toward those behaviors. We are left in the familiar situation of today, where software vendors may try to trick us into running unsafe code. There are established techniques from formal methods that can help in such situations, and I expect them to be about as helpful for AI-generated code as for human-generated. They can’t obviously help with the pamphlets as proof comments, so there we just have to rely on the fact that the AI really has no incentive to go there, based on its initial implementation by humans (including that version’s ability to preserve this property in future versions). That implementation should be scrutinized by experts to catch weird behaviors, which will be helped by making the implementation as simple as possible. We want complexity to arise later from the RSI loop, governed by the strong requirement to maintain correct behavior. More conventional misbehavior like opening unauthorized network connections we can cover with end-to-end formal verification extended to cover the whole history of self-improvement.
Interesting Extensions
The baseline idea is an autonomous proof factory, but we can consider different variations.
One unifying theme for upcoming posts will be covering different ingredients in creating good autonomous evidence factories. “Good” here includes both performance engineering and getting all of the formal-methods details right to ensure safety. I’ll be covering the whole hardware-software stack, for both theorem provers and the other code they should be used to optimize, and some general techniques for searching for more efficient code that is provably correct.