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 reach, and the cost of each kind of error.

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: