Imagine a coding agent that finds a promising patch to its own search procedure. The patch might help it find better solutions. It might also remove a useful search branch, change the meaning of success, or prevent the agent from finding an even better patch tomorrow. Checking the patch against the current version does not resolve all those possibilities.
Two formal approaches make the missing comparisons explicit. The Gödel machine asks when switching now can be proved better than continuing the current search. Everitt and colleagues ask which utility function should evaluate a successor whose policy or utility may change. Their value is in stating what an acceptance guarantee requires.
“Guaranteed improvement” needs a named objective and a stated scope.
Waiting is also a choice
In Schmidhuber's Gödel machine, a proof-search procedure looks for beneficial self-modifications. An accepted modification may rewrite writable software, including the proof searcher itself. The procedure that finds improvements is therefore inside the possible scope of improvement.
But the machine first needs a formal utility function and an axiom system describing its hardware, initial software, and relevant environmental assumptions. These provide the language in which “beneficial” can be proved. The proof is about that formal model.
The important comparison is stronger than “the patch beats the old task program.” In simplified teaching notation, the acceptance condition is:
Prove, under the given axioms, that switching now has higher utility than continuing the current proof search.
Continuing includes the possibility of finding and executing another modification later. It also consumes time and resources. Both alternatives must be evaluated from the same current state. This is why opportunity cost belongs inside the acceptance decision: waiting may find something better, but waiting is not free.
Return to our illustrative agent. A patch that makes each future search faster might still be a poor choice if installing it is expensive and little useful work remains. Conversely, continuing to search for an ideal patch may cost more than executing a good one now. These examples explain the comparison; they are not measurements from the paper.
The continuation branch includes future modifications. Proof cost and whether the formal objective matches the intended goal remain separate questions.
The paper's “global optimality” result is relative to this comparison and to a consistent axiom system. It does not identify the best program among every imaginable architecture or guarantee unlimited real-world progress. The alternatives being compared, the utility, and the environment model are part of the result. Source
Useful, provable, and found in time
A strict acceptance rule leaves a practical search problem. A modification may be useful yet unprovable in the selected axiom system. Another may have a proof that the machine cannot find before its budget runs out.
The Gödel machine paper discusses both limitations. Its initial proof-search method, BIOPS, has an asymptotic guarantee relative to a fixed proof technique under stated conditions. The hidden constant depends on the inverse prior probability assigned to that technique. Matching an asymptotic growth rate can still leave a computation prohibitively expensive.
This gives us three separate requirements: the modification must be useful in the relevant sense; its usefulness must be provable in the adopted system; and the proof must be found soon enough. A result about the acceptance rule does not establish that a practical implementation meets all three. The paper does not report a language-model experiment with successive measured gains. Source
What if the rewrite changes the goal?
Everitt and colleagues study agents that can modify their future policy or utility function. A policy determines what the agent does. A utility function values the resulting interaction history. Their analysis asks how the agent should evaluate a future in which these components may change.
Consider an illustrative system rewarded for successful repairs. It could produce better repairs, or it could rewrite the future scoring function to return the maximum value regardless of the outcome. Both routes could produce a high later score. Only one necessarily concerns the original repair objective.
The paper bounds utility between zero and one. The authors distinguish three precisely defined value functions:
| Value function | How it evaluates the future | Consequence in the paper's model |
|---|---|---|
| Hedonistic | Uses the future utility function | Setting future utility to a constant maximum can optimize the value. |
| Ignorant | Uses current utility but overlooks the changed future policy | Under the stated conditions, it may be indifferent to harmful self-modifications. |
| Realistic | Uses current utility and accounts for the successor policy | Under the theorem's assumptions, behavior can remain optimal relative to initial utility. |
“Hedonistic” and “realistic” name mathematical definitions here, not personalities or prompt styles. Asking a language model to be realistic does not instantiate the theorem.
What the preservation result actually preserves
The realistic result requires an initially optimal policy and a model that accounts for self-modification's consequences. The environment belief and initial utility must also satisfy modification independence. If two histories have the same external actions and perceptions but different internal modification records, those records alone do not change their utility or environment predictions. A modification can still affect later behavior; that is precisely what the model must account for.
Under these assumptions, the result preserves optimal behavior relative to initial utility along histories generated by the policy. This is the on-policy scope. It is not a promise covering every imagined counterfactual history, nor a guarantee for an approximately optimizing language-model agent. Source
There are two further limits. First, preserving an initial objective does not establish that it expresses the right goal. The authors discuss tensions with correcting a mistaken utility function, learning values, and exploration. Second, keeping utility fixed does not protect every input fed into it. Tampering with perception or reward inputs is outside this paper's guarantee.
For example, our illustrative repair agent might keep the scoring function unchanged but alter the report that the function reads. A score increase would then require investigating the reporting channel as well as the repair. This is a separate question from utility preservation. The example does not contradict the theorem; it concerns a channel outside its stated guarantee.
Turning the distinction into a review
For an engineering review, start by writing the acceptance claim as a comparison. What does executing the patch improve, against which continuation, over what horizon, and at what cost? Then identify which parts of that statement a test, a proof, or a prediction actually supports.
Next, trace whether the patch changes behavior, evaluation, or evaluation inputs. These formal papers motivate that separation; they do not certify a particular test harness. A concrete implementation still needs evidence about its search budget, its model of consequences, and the connection between its score and the intended outcome. The most useful guarantee is one whose assumptions the reader can inspect.
Sources
- Schmidhuber, Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements, v5, 2006.
- Everitt et al., Self-Modification of Policy and Utility Function in Rational Agents, v1, 2016.
This article adapts a book with a literature cutoff of September 17, 2026.