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 permits rewriting its software, including the code that searches for changes. Its initial admission route requires a proof that switching to a proposed program has greater expected utility than continuing the current search, under axioms describing the machine, environment, and utility function (Schmidhuber, §3.2 (snapshot required)).

This is a proof-governed construction of reflective self-modification, not a definition of reflection. Its admission rule offers rigor relative to a formalization while excluding switches for which the required proof is not obtained. That restriction alone says neither how large the reachable state space is nor how well the machine operates within a practical budget.

The change loop

The construction can be read as a proposal-selection improvement loop:

Function Gödel-machine realization
Self-representation Axioms describing the machine, its software, environment assumptions, and utility
Search Proof techniques that can construct proposed replacements and proofs
Evaluation A proof of the target theorem comparing switching with continued search
Authority and retention The switching operation invokes the proved replacement, which can rewrite the subsequent software

These functions are not independent components. Passing the switching check and invoking the replacement are coupled. Environmental observations can enter the proof process through the source's time-labelled state2theorem operation; the machine is not limited to deductions about its initial state alone.

Self-modification can also change the proof searcher, axioms, or utility representation where the predecessor formalization licenses that change. The construction does not require every later policy choice to have been listed in the seed, nor does it require an unchanged proof-search implementation forever (Schmidhuber, §3.2 and §6.1 (snapshot required)).

Three different limits

Admission. A useful switch cannot take effect through the proof-gated route unless the required proof is obtained. The paper says the machine "must ignore those self-improvements whose effectiveness it cannot prove" (Schmidhuber, §2.4 (snapshot required), verbatim). Some claims may be unprovable under the axioms; others may be provable but not found within the available resources. These are different limits.

Adequacy of the formalization. The Global Optimality Theorem compares a switch with continuing the search, including the later switches that search might find. Its guarantee is conditional on the encoded assumptions and utility. A valid proof under an inadequate model or objective need not warrant the outcome a user actually wanted. Formalization moves some judgment into the choice of premises and objective; it does not remove that judgment.

Practical continuation. The existence of an admissible beneficial switch says little about the cost of finding it or about sustained software-production performance. A restrictive proof gate may allow many useful changes under one formalization and few under another. No general size estimate follows from proof-gated admission alone. Likewise, being allowed to emit arbitrary code does not make a useful empirical successor likely.

Comparison with empirical self-modification

An empirical loop can propose a change, test it, observe later consequences, and recover without first proving improvement. Its characteristic risk is accepting harmful changes. The proof route instead risks leaving a useful change unavailable because its proof is absent or too expensive. Which costs more depends on the objective, evidence, search process, and consequences of error.

Consider the narrow case of a prompt-editing loop whose harness loads each edit without an independent acceptance check. Its revision path is permissive and its retention reliable, but neither property makes the edit good. Once a harmful instruction is retained, it can affect later runs. This illustrates why false-positive acceptance becomes operative.

That is a property of the chosen gate, not of natural-language representation. A prompt-editing system can add tests, limited authority, independent criticism, versioning, and rollback. Conversely, executable code can be admitted through a weak gate. Available checks bound what the observed success warrants in either case. Proof is one way to govern self-referential changes; it is not the only way to obtain bounded empirical warrant.

Acceptance and search pressure differ

The Darwin Gödel Machine uses viability to decide archive admission and benchmark performance to weight later parent selection. It does not require each archived candidate to prove or even demonstrate immediate improvement. The Huxley-Gödel Machine uses evidence about descendants to inform that selection. These are different uses of evidence from a proof authorizing a switch.

Incremental Self-Improvement provides another contrast: a payoff-per-time criterion governs retained modifications and restoration when they cease to qualify. These cases show why admission, reproduction, and continued retention should not be collapsed into one notion of evaluator strength.

The useful comparison has at least two dimensions: the rigor of inference from stated premises, and how well those premises and observations cover the objective. A strong answer on one dimension does not supply the other.

Grounds for change: comparison with a theory builder

A theory builder develops and revises tentative theories of external subjects and of its own machinery, and a machinery change need not first be proved beneficial under the current self-theory. The distinction from the Gödel machine concerns the grounds required for a change, not whether the system observes the world or can rewrite its evaluators. Natural language, fixed model weights, and the mere presence of self-modification do not define the difference.

Question Gödel machine's proof-governed route Theory builder
What justifies a machinery change? A proof of the switching claim under the formalization Evidence supporting the change relative to a stated objective, with assurance bounded by the checks performed
How does evidence enter? Observations enter through formalized operations and can support proofs Cases and operating consequences can challenge the theory used to diagnose, propose, or evaluate a change
What if an empirical assumption is inadequate? Proof does not establish the adequacy of the premises; formal revisions remain subject to the licensing route The builder revises the implicated assumption and tests the resulting theory and machinery without proving the revision from that assumption
What remains uncertain? Whether the formalization is adequate and useful proofs can be found within resources Whether interpretation, diagnosis, evaluation, and later correction are reliable enough for the intended use

Empirical acceptance permits acting where the required proof has not been obtained, and it permits accepting harmful changes. A theory builder is therefore not simply a more permissive admission route; its research question is whether explicit theories, including a self-theory that the return from external work revises, make its machinery acquisition and evaluation reliable enough for its work. Keep acquisition capability separate from the warrant for using an extension: evaluator replacement needs evidence of adequacy, not permission from the incumbent. Whether the Gödel machine itself is a theory builder is assessed per deployment and stays open; an internally represented utility does not by itself decide where outcome assessment occurs, and this comparison establishes no categorical exclusion.

Scope

  • A reflective system needs a causally connected self-representation, not a proof of improvement. Proof-gated admission is an additional design choice.
  • Deductive closure concerns derivable propositions. Transition closure concerns states reachable through permitted operations and inputs. Neither alone establishes practical reliability.
  • The Gödel-machine paper presents a formal construction, not an implemented software house with measured continuation reliability. It supports the architectural comparison, not a performance ranking.
  • Formal causal reasoning would require suitable assumptions and objectives inside the formalization. The host architecture alone does not supply them.

Relevant Notes: