Case packet

Neutral case identifier: case-c34b3568d535fc

The possible directed relationship from Artifact A to Artifact B is under review.

Artifact A

Gödel machines are a proof-governed case of reflective self-modification

Schmidhuber's Gödel machine makes all of its code rewritable, including the routine that searches for code changes. Every rewrite must pass a single gate: an embedded proof searcher must prove that switching now yields greater expected utility than continuing the current search, under axioms describing the machine's hardware, initial code, environment, and utility function ([Schmidhuber 2003, printed pp. 4, 9–10; PDF pp. 5, 10–11]).

It is a comparison case, not a foundation: it realizes the reflective change loop in a fully formal register, and its gate makes the defining tradeoff explicit — deductive rigor relative to a formalization, at the price of making beneficial but unprovable rewrites unreachable.

The change loop, formally realized

The architecture is a [proposal-selection improvement loop] — candidates generated, evaluated with a possibility of non-adoption, selectively made operative — and maps onto its search, evaluation, and retention decomposition:

Reflective change function Gödel-machine realization
Self-representation An axiomatized description of the machine, its utility function, hardware, and environment assumptions
Search Systematic enumeration of proof techniques that may construct candidate replacements
Evaluation A proof that the switching criterion — the target theorem — is satisfied
Authority The proof checker invokes the proved replacement program; no other path can invoke it
Retention The replacement becomes the machine's subsequent code

The decomposition thus applies to a fully formal construction, not only to systems with fallible evaluators. It does not follow that the functions vary independently: here authority and retention are coupled — passing the proof checker both invokes the replacement and installs it as the machine's subsequent code.

What the proof gate buys, and what it costs

The Global Optimality Theorem builds waiting into the comparison: continuing the current search implicitly includes every later rewrite the search might find, so a proved switch is better — according to the encoded axioms and utility function — than holding out for any of them. The "no local maxima" claim applies to the sequence of self-modifications, not to the external problem's reward landscape; and because the proof accounts for later self-modifications affected by the current one, the acceptance criterion collapses the regress of separate meta-levels (printed p. 12; PDF p. 13).

The cost is stated in the paper: a Gödel machine "must ignore those self-improvements whose effectiveness it cannot prove" (printed p. 5; PDF p. 6). And the guarantee is only as good as the formalization, whose consistency is assumed rather than proved: sound axioms and a faithful utility function make a valid proof a rigorous conditional guarantee, while a wrong formalization lets a valid proof license a harmful change. Axiomatization moves judgment upstream into model specification; it does not eliminate it.

Fallible empirical evaluators have the opposite risk profile: they may accept changes that do not help, but they can reach changes no available proof can license. Neither regime dominates without assumptions about model adequacy, proof surface, and the cost of each kind of error.

The opposite corner: LLM prompt self-editing

A system whose behavior-determining organization is natural-language a language model can read and rewrite — prompts, instructions, retained guidance — occupies the corner of the design space diagonally opposite, and the trade inverts on both axes at once. The Gödel machine holds the strongest possible gate over a nearly empty reachable set: it must ignore every improvement it cannot prove. A prompt-editing loop has an enormous search range — any semantic revision of its own instructions is a candidate — and, by default, no gate at all: bare autonomy comes free, and natural-language supplies no proof surface to bound it, [since warranted autonomy is bounded by oracle domain].

A retention asymmetry sharpens the weak-gate corner's risk. A Gödel-machine rewrite becomes operative only through the proof checker — evaluation and authority are coupled by construction. A prompt edit's operative retention is instead guaranteed by the executing harness: the instruction is loaded on every run, so consumer, channel, and force come free, and an unwarranted acceptance becomes operative immediately and compounds across runs, [since false-positive acceptance becomes operative]. Where a retained note can fail silently by never being consulted — [retrieval failure is reflection failure] — a prompt sits at the opposite limit: the wire is guaranteed, so the gate is the only protection there is.

The comparison locates what the axiomatization actually bought: warrant for self-referential change. When the artifact being edited contains the acceptance criteria themselves, the Gödel machine's axioms are the one clean answer on record; the natural-language form has no analogue yet. Pending one, warranted prompt self-editing runs through empirical gates — evaluations over prompt variants, with warrant scoped to the eval's domain — or keeps a human at the gate. The two corners fail in opposite directions: the proof-gated system starves for reachable improvements, the prompt-edited system drowns in unwarranted ones.

Acceptance evidence varies across systems

The acceptance gate is a useful axis of comparison — not a controlled experiment, and not a single ladder of strength. A Gödel machine requires proof under its formalization. [Incremental Self-Improvement] retains policy changes on reward history and rollback. The [Huxley-Gödel Machine] estimates a lineage's future value from benchmark evidence. Commonplace combines tests, validators, review, and human judgment.

The axis separates two dimensions a single [oracle-strength spectrum] can obscure: the rigor of the inference from stated premises, and the adequacy of those premises to the external objective. In a Gödel machine [the boundary of automation is the boundary of verification] by construction — but the boundary is provability under the formalization, not truth about the world.

What this comparison does not license

  • Proof is added to reflection; it does not define it. A [reflective system] requires a causally connected self-representation, not formal verification or successful improvement. The Gödel machine occupies one proof-governed corner of the design space, not the endpoint of a maturity ladder.
  • The Gödel-machine paper is not causal-inference literature. It shows a proof-gated host architecture. Causal reach-assessment would require causal calculus, discovery assumptions, and intervention or counterfactual objectives inside the axioms and utility function; those are not supplied by Schmidhuber's construction.
  • The paper describes a construction, not a running system. It reports no implementation and no experiments, so it supports architectural conclusions, not empirical performance claims.

Relevant Notes:

Artifact B

False-positive generation is filtered; false-positive acceptance becomes operative

In a [proposal-selection improvement loop], search and evaluation fail in ways that are not symmetric, and the asymmetry is structural rather than incidental.

Search sits upstream of a filter. A bad candidate — useless, harmful, off-target — reaches evaluation and is rejected. It cost effort and nothing else; it never became operative.

Evaluation is the filter. A bad acceptance is not caught by anything downstream, because retention is not a filter — retention is the machinery that makes the change stick. The accepted artifact acquires a consumer, a channel, and a force, and starts shaping behavior.

Only the last filter's errors survive.

What the claim covers, and what it does not

The asymmetry is between the two kinds of false positive. Search produces something that should not have been produced, and the filter catches it. Evaluation passes something that should not have passed, and nothing catches it.

Search's other failures are not filtered, because there is nothing to filter. Search also fails by omission — never generating the candidate worth having, choosing the wrong target, stopping too early — and those errors are invisible and permanent. No evaluator recovers them: [evaluation cannot select a candidate that search never reaches]. They are not retained either, since nothing enters the system; they are simply forgone, and the system cannot tell that they were.

The precise claim is:

False-positive generation is filtered before retention; false-positive acceptance becomes operative.

That is what makes "make the evaluator stronger" no answer to a weak generator, and it is why the two functions cannot be traded against each other. It also means the consequence below ranks what to automate among the errors the loop can see. Omission errors are the reason automating search is not free either — a generator with narrow range costs improvements no one will ever miss.

The consequence: automate search first

The costs of automating the two functions are paid in different currencies.

Automating search costs evaluation throughput. Machine-generated candidates are judged by the same evaluator that judged the human's. The failure mode is a queue: candidates arriving faster than anything can judge or prune them, which is exactly the pathology in [entropy management must scale with generation throughput]. That is a capacity problem, and capacity problems are tractable — batch, prioritize, sample, or strengthen the evaluator.

Automating evaluation costs correctness. A weak oracle accepts changes that do not help, they are retained, and they compound: a bad note gets linked, cited, and reshaped into a skill. That is not a capacity problem and no amount of throughput fixes it. It is bounded by [the boundary of automation is the boundary of verification].

And taking the autonomy anyway does not break anything visibly — which is what makes it dangerous. A fallible evaluator still rejects some candidates, so it is a real evaluator and [the loop still closes]. The system stays self-improving and looks healthy, running unattended, while its mistakes accumulate in the artifacts it keeps. Nothing announces the degradation, because the machinery that would have announced it is the machinery that was weakened.

So search is the function whose failures the loop already catches, and it is the one to automate first. Evaluation is the one that has to be bought, with an oracle.

This explains a common disappointment in agent-memory systems. Most of them automate search — mine the traces, extract the tips, write them down — and leave evaluation to a human or to nothing at all. The result is a growing pile of unjudged candidates that changes little. The [agent-memory-system-review] type already points at the same place from the other end when it says the distillation step's "trigger, oracle, and curation policy is often the most discriminating part." This claim says why: the oracle is the only part whose errors are both permanent and operative — an omitted candidate is lost, but an accepted bad one goes to work.

The correction path does not escape the bound

The asymmetry is not absolute, and pretending otherwise would overstate it. A bad acceptance can be caught later — by a review sweep, a freshness pass, or a Popperian "do I still believe this?" reread. Retention is revocable.

But that correction path is itself evaluation, and it inherits the same bound. Three things follow:

  • It spends evaluation capacity, which was the scarce resource to begin with.
  • It runs against the same oracle that made the original mistake, so the blind spot that let the change in is the blind spot that lets it stay. A second pass with an unchanged oracle is not a second chance.
  • Meanwhile the artifact has been operative, and may have acquired dependents — the cost of removing it is no longer the cost of never having accepted it.

False-positive generation is caught by machinery already running in the loop, at no extra cost. False-positive acceptance is caught only by spending more of the thing that was scarce, and only if the oracle has meanwhile improved.

Scope

  • The claim is scoped to the proposal-selection subtype of [self-improvement] — the architecture that has an acceptance step at all. A direct evidence-driven update pathway (gradient, reward, viability) adopts every update, so its failure surface is the adequacy of the objective and the update rule, not a gate's false positives.
  • The claim assumes evaluation is the terminal filter. If a system adds monitoring or rollback downstream, that is not a counterexample — it is more evaluation, and it inherits the same bound.
  • It holds whether evaluation runs before a candidate becomes operative or after. Post-hoc evaluation changes when the bad change is caught, not whether an unfiltered acceptance is retained.
  • It ranks what to automate first under a fixed oracle. It does not say search is easy: [automating KB learning is an open problem], and the judgment-heavy parts of search remain hard for their own reasons.

Relevant Notes:

Under-review context phrase

why guaranteed retention concentrates the prompt-editing corner's risk entirely at the gate