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

Type: kb/types/note.md · Tags: foundations, computational-model, self-improving-systems

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 Darwin Gödel Machine explicitly relaxes proof to empirical search pressure: viability decides archive admission, while benchmark score weights later reproduction rather than acceptance. The Huxley-Gödel Machine then 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: