Ingest: Gödel Machines — Provably Optimal Self-Improvements

Type: kb/sources/types/ingest-report.md

Source: goedel-machines-schmidhuber.md Captured: 2026-07-14 From: https://arxiv.org/abs/cs/0309048

Citations below are given as (printed p. N; PDF p. N+1), matching the snapshot's capture note.

Classification

Genre: scientific-paper — a theoretical CS paper (TR IDSIA-19-03 v5, December 2006; v1 September 2003; cs.LO/cs.AI) whose contributions are a construction plus two theorems, with no experiments and no implementation. The genre recorded on the snapshot is correct. Domains: self-modification, reflection, verification, oracle-strength Author: Jürgen Schmidhuber (IDSIA / TU München) — a principal in the universal-search and metalearning lineage (Universal Search extensions, OOPS, Incremental Self-Improvement). High authority on the formal content, and also an interested party in the priority framing, which shows in the structure: Section 6.4 is largely a comparison against Hutter's and his own prior work (printed pp. 18–21; PDF pp. 19–22).

Summary

A Gödel machine is a universal problem solver whose entire initial software p(1) — the environment-interacting subpolicy e(1) and the proof searcher that looks for changes to p — is modifiable, but only through one gate. An embedded proof searcher systematically tests proof techniques (programs that emit proofs) against an axiomatic system A encoded in p(1); A axiomatizes the hardware, the initial code, the environment's stochastic properties, and a formal utility function u. The searcher builds (switchprog, proof) pairs until it proves a target theorem stating that immediately rewriting p through the current switchprog yields higher utility than leaving p as is — that is, than continuing to search for alternatives. Only then does the instruction check() set switchbit and transfer control to switchprog, which may rewrite any part of the state, including p and the proof searcher itself (printed pp. 4, 9–10; PDF pp. 5, 10–11). The Global Optimality Theorem 4.1 states that, given a formalizable u and assuming the consistency of A, such a switch is globally optimal in one specific sense: executing the present switchprog beats waiting for the searcher to produce a later alternative — because "leave p as is" implicitly quantifies over every switchprog the unmodified searcher could ever find (printed pp. 11–12; PDF pp. 12–13). Theorem 5.1 separately shows the initial searcher (BIOPS, Universal Search applied online to proof space) is O()-optimal while remaining itself rewritable (printed p. 14; PDF p. 15). The paper is explicit that all of this is relative to A: Section 2.4 concedes the machine must simply ignore any improvement it cannot prove, and the closing paragraph asks the question the construction leaves open — which theorems a practical Gödel machine should be given as axioms so the searcher need not derive them from scratch (printed pp. 5, 24; PDF pp. 6, 25).

Connections Found

The source lands in an already-populated kb/notes/ cluster and does not open a new one. Its durable role is the proof-governed limit case of reflective self-modification: the system that pays the maximum price — full axiomatization of hardware, environment, and goal — to buy a guarantee that no other self-modifying system in the casebook can offer.

It is the strongest available corroboration of a proposal-selection improvement loop requires search, evaluation, and operative retention, because the Gödel machine instantiates all three functions separably and formally: proof-technique enumeration is search, the target-theorem proof is evaluation, and check() plus switchprog is retention with operative force. That the decomposition survives in a fully formal setting shows it is not an artifact of oracle-poor KB domains. It supplies the missing hard-oracle occupant for oracle strength spectrum, whose hard end currently tops out at unit tests and type checks. And it makes the boundary of automation is the boundary of verification true by construction rather than by observation: no rewrite executes without a proof, so the automation boundary is the provability boundary relative to A.

One adjacency needs care rather than an edge. The Exclusions section of reflective system separates reflection from "successful self-improvement" and from "formal verification". The Gödel machine has all three — but it adds a proof system on top of a causally connected self-representation to get them. The pairing should make that exclusion concrete, not quietly repeal it: reflection supplies the causal path by which a self-change can take effect, and nothing more. Finally, this paper is the named ancestor of Huxley-Gödel Machine — a different, modern coding-agent system that borrows the name and substitutes an empirical benchmark estimate for the utility proof. Reading the pair isolates exactly what is traded away when the proof oracle is unavailable; it does not make HGM a Gödel machine, nor this paper a limit that HGM converges to.

Extracted Mechanics

The five points a downstream comparison note needs, with citations.

1. The proof searcher

The initial searcher does not enumerate proofs; it enumerates proof techniques — programs written in a universal language L implemented within p(1) (Schmidhuber suggests a PROLOG or FORTH variant), which read parts of the state s and emit proofs. This is the announced advantage over the brute-force searchers of Hutter's work, which generate all proofs in order of size and so take time exponential in proof size; short proof techniques can produce certain long proofs (printed p. 6; PDF p. 7).

A proof technique may read any part of s — including the inputs x and the code of p(1) — may write to a scratch region sp, may set switchprog, and grows a proof in the string variable proof; proof and sp are reset at the start of each new proof-technique test (printed p. 6; PDF p. 7).

The instruction set is exactly six proof-modifying instructions ("there are no others"), and their design is what trivializes proof verification — it is impossible to insert an incorrect theorem into proof (printed pp. 6–11; PDF pp. 7–12):

  • get-axiom(n) — appends the n-th axiom of the axiom scheme to proof.
  • apply-rule(k, m, n) — applies the k-th inference rule (e.g. modus ponens) to the m-th and n-th theorems already in proof, appending the result; if inapplicable, the proof technique under test is interrupted, which is what keeps invalid proofs out.
  • delete-theorem(m) — deletes the m-th theorem to free storage (deleted theorems can no longer be addressed by apply-rule).
  • set-switchprog(m, n) — sets switchprog := sp[m:n].
  • check() — the switching gate; see point 2.
  • state2theorem(m, n) — turns the currently observed contents of s[m:n] into a time-labelled theorem (s[m:n](t1) = z) without proving it from s(1), which is how environmental inputs and already-executed computations enter the proof. Schmidhuber flags the self-observation hazard here: parts of s that change while being read (a fast instruction pointer) may be unreadable in principle, and he compares this to Heisenberg uncertainty (printed pp. 10–11; PDF pp. 11–12).

The search strategy over these techniques is BIOPS (Bias-Optimal Proof Search): Universal Search applied online to proof space. Starting from a bias P over proof techniques (e.g. P(w) = K^-l(w)), phase i = 1, 2, 3, … runs every self-delimiting proof technique w with P(w) ≥ 2^-i for at most 2^i P(w) steps, undoing each technique's effects on sp afterwards (Method 5.1, printed p. 14; PDF p. 15). Its guarantee is Theorem 5.1: if some unknown fast proof technique w needs at most f(k) steps to produce a proof of difficulty k, BIOPS needs at most O(f(k)) steps — the 1/P(w) factor is constant in k (printed p. 14; PDF p. 15). The online setting is the stated novelty: unlike offline Universal Search, the same proof technique started at different times may yield different proofs, because it reads a changing s (printed p. 13; PDF p. 14). Section 5.2 adds OOPS-style reuse — proof techniques that yielded target theorems are frozen (non-writable but readable and callable by later techniques), giving 8-bias-optimality (printed pp. 14–15; PDF pp. 15–16).

BIOPS is a choice, not a requirement: "the Global Optimality Theorem 4.1 expresses optimality with respect to whichever initial proof searcher we choose" (printed p. 15; PDF p. 16).

2. The switching / target-theorem criterion

check() is the only gate. It first tests whether the last theorem in proof has the form of a target theorem, which states that, under the axiomatized utility function u, switching from p to the current switchprog has higher utility than continuing to execute p (which would keep searching for alternative switchprogs). Formally (equation 2, printed p. 9; PDF p. 10):

(u[s(t1) ⊕ (switchbit(t1) = ‘1’), Env(t1)] > u[s(t1) ⊕ (switchbit(t1) = ‘0’), Env(t1)])

where s(t1) ⊕ (switchbit(t1) = ‘b’) denotes the state obtained by replacing the true value of switchbit at t1 with b. The set of possible target theorems is parameterized only by the time step t1, which exists to absorb the hardware delay between finding an abstract proof and matching it to the machine's real current state.

If a target theorem is found, check() uses a prewired subroutine to verify that there is enough time left to set switchbit before time reaches t1; if not, it exits. Otherwise it sets switchbit := 1 — "there is no other way of changing switchbit" — then repeatedly tests time until time > t1 so that the condition of the formula was actually fulfilled at t1, and then transfers control to switchprog — "there is no other way of calling switchprog" (printed p. 10; PDF p. 11). Retention is wired, not hoped for: the proof is the sole channel to execution.

Section 4.2 offers a relaxed target theorem (equation 3) with ≥ instead of >: the machine then rewrites itself as soon as it proves the change will not make things worse (printed p. 12; PDF p. 13).

A precision worth carrying: to prove a target theorem the searcher does not need to compute the true expected utilities of switching and not switching — it only needs to determine which is higher (printed p. 13; PDF p. 14).

3. Scope of permitted self-modification

switchprog "may subsequently rewrite all parts of s, excluding hardware-reserved parts such as time and x, but including p" (printed p. 10; PDF p. 11) — and p includes the proof searcher. Section 2.2 says it plainly: the machine "executes switchprog, which may completely rewrite p, including the proof searcher" (printed p. 4; PDF p. 5). Section 6.1 enumerates the reach (printed pp. 15–16; PDF pp. 16–17): retune the time-sharing ratio between proof search and the subpolicy e; modify e only; modify its very axioms to speed things up (replacing or augmenting them with theorems derivable from the originals); change its own utility function and target theorem — "but can do so only if their new values are provably better according to the old ones"; speed up subroutines of the proof searcher or reorder its proof generation; in a degenerate environment, delete most of its initial software including the proof searcher entirely; and even augment its own hardware by exploiting physical resources of the environment.

What remains fixed is therefore narrow: the hardware state-transition function F and the hardware-reserved parts of s (time, x), plus the axiomatic bootstrap A and the utility function u as starting points — and even those two are revisable, but only through the old A and the old u. The recursion does not run away, because of the meta-level collapse (Section 4.3): "any proof of a target theorem automatically proves that the corresponding self-modification is good for all further self-modifications affected by the present one, in recursive fashion. In that sense all possible 'meta-levels' of the self-referential system are collapsed into one" (printed p. 12; PDF p. 13; restated as FAQ 2 and 3, printed p. 22; PDF p. 23). Self-reference is bootstrapped without circularity by the initial-state axioms — p can encode a description of itself, since "some software may include a program that can print the software" (printed p. 9; PDF p. 10).

4. Formal utility assumptions

Everything the machine can prove rests on the axiomatic system A, encoded in p(1) and reachable only via get-axiom(n). Its six axiom classes (printed pp. 7–9; PDF pp. 8–10):

  • (a) Hardware axioms — formally specify how components of s (other than environmental inputs) change from one cycle to the next; the paper gives a sample 64-bit instruction-pointer axiom and asserts "any abstract hardware model can be fully axiomatized in a similar way."
  • (b) Reward axioms — computational costs of every hardware instruction, physical costs of output actions, values assigned to input events, and the total value of the machine's life as a scalar function of all rewards and costs between cycles 1 and T.
  • (c) Environment axioms — restrict how the environment produces inputs in reaction to outputs; e.g. that it is sampled from an unknown µ in a known set M of distributions (all computable ones, or limit-computable, or the Speed Prior, or Markovian, or fully predictable). "All such prior assumptions are perfectly formalizable in an appropriate A."
  • (d) Uncertainty and string-manipulation axioms — standard arithmetic, calculus, probability theory, statistics, sufficient to prove bounds on expected remaining lifetime, costs, and rewards.
  • (e) Initial state axioms — enough to reconstruct s(1), including p(1) itself.
  • (f) Utility axioms — the overall goal, in the form of the utility function u.

The default u is expected cumulative future reward, u(s, Env) = E_µ[ Σ_{τ=time}^{T} r(τ) | s, Env ] (equation 1, printed p. 3; PDF p. 4), where the expectation is over an unknown µ ∈ M. Crucially it "takes into account computational costs of all actions including proof search" (printed p. 4; PDF p. 5) — that is what makes "keep searching" a costed alternative and gives the target theorem something to compare against. Alternative formalizable utility functions (worst-case rather than expected performance, or reward intake per time interval) are allowed (printed p. 4; PDF p. 5).

A is "a defining parameter of a given Gödel machine" and "must be strong enough to permit proofs of target theorems" (printed p. 11; PDF p. 12). The consistency of A is an assumption of Theorem 4.1, not a result (printed p. 11; PDF p. 12).

5. The limitation, and what optimality is and is not

Unprovable-but-useful modifications are unreachable. Section 2.4 is unambiguous: "even a Gödel machine with unlimited computational resources must ignore those self-improvements whose effectiveness it cannot prove, e.g., for lack of sufficiently powerful axioms in A. In particular, one can construct pathological examples of environments and utility functions that make it impossible for the machine to ever prove a target theorem." A resource-limited machine additionally "cannot profit from self-improvements whose usefulness it cannot prove within its time and space constraints" (printed p. 5; PDF p. 6). FAQ 8 repeats it: an improvement whose utility is undecidable is one the machine "will therefore simply ignore" (printed p. 23; PDF p. 24). The machine rewrites only when it has a proof; there is no empirical, statistical, or provisional path to a self-change.

What Theorem 4.1 claims. "Given any formalizable utility function u, and assuming consistency of the underlying formal system A, any self-change of p obtained through execution of some program switchprog identified through the proof of a target theorem (2) is globally optimal in the following sense: the utility of starting the execution of the present switchprog is higher than the utility of waiting for the proof searcher to produce an alternative switchprog later" (printed p. 11; PDF p. 12). The proof is four sentences: the second branch of the binary decision ("keep searching") covers all, possibly infinitely many, potential later switchprogs; so if the current switchprog were not the best, the searcher could not have proven that switching beats discarding it — assuming A is consistent (printed pp. 11–12; PDF pp. 12–13).

What is not claimed. The optimality is doubly relative, and the paper says so. It is relative to the given u and A (both named in the theorem statement), and Section 2.2 adds the rest: the switch is the best of all possible relevant self-changes "relative to the given resource limitations and initial proof search strategy" (printed p. 4; PDF p. 5). So there is no claim that a beneficial rewrite exists; no claim that the machine finds anything at all if no target theorem is provable under A; no claim of optimality against policies A cannot reason about; and no claim that u is the right goal — u is stipulated. "No local maxima" is a statement about the sequence of self-changes the searcher could produce, not about the reward landscape of the environment. Theorem 5.1's O()-optimality is a separate and weaker claim about the initial searcher's time complexity, explicitly leaving "a lot of room for self-improvement hidden by the O()-notation" (printed p. 4; PDF p. 5).

Extractable Value

  1. The acceptance gate is the varying component across self-improving-system designs. Four sources now in the KB differ almost solely in what licenses a self-revision: a reward gate (Incremental Self-Improvement), a proof gate (this paper), an MDL/AIC gate (self-revising discovery systems), and a benchmark-oracle estimate (Huxley-Gödel Machine). Search and retention hold roughly constant; the gate's strength trades directly against the breadth of domains it can be applied in. This is the missing bridge between the search/evaluation/retention decomposition (which names evaluation) and oracle strength spectrum (which grades oracles without connecting the grades to self-modification architectures). [deep-dive]
  2. Meta-level collapse answers a standing open question, in principle. A proposal-selection improvement loop requires search, evaluation, and operative retention asks whether a system can represent its own search and evaluation processes as modifiable aspects. Section 4.3 answers yes for this construction and supplies the mechanism: a target-theorem proof necessarily quantifies over the self-changes the present one enables, so the regress closes at the acceptance criterion rather than in a tower of meta-levels (printed p. 12; PDF p. 13). The answer is formal, not demonstrated — no Gödel machine has been built. [deep-dive]
  3. Gated goal change is a hard-oracle answer to goal drift. The utility function and target theorem are themselves rewritable, but only on a proof of benefit under the current utility function (printed p. 16; PDF p. 17; FAQ 7, printed p. 23; PDF p. 24). For a methodology governs its own extension only as far as it settles the meta-decisions it raises this is an existence proof that a system's own acceptance rule can govern rewrites of that acceptance rule — and it names the price. [experiment]
  4. A proof-of-utility oracle checks a different thing than any oracle on the current spectrum. Oracle strength spectrum grades oracles by how cheaply correctness can be checked; the Gödel machine's oracle checks expected future utility, which is strictly harder to establish than any test suite. And what it buys is a search guarantee (no local maxima in the self-change sequence), not the training-signal guarantee the note currently attributes to oracle strength. Whether those are one property or two independent dividends is an open question the note does not raise. [deep-dive]
  5. The axiomatization burden relocates human effort; it does not remove it. The paper opens by promising to "eliminate the restrictive need for human effort in the most general way possible" (printed p. 2; PDF p. 3) and closes by asking which generally useful theorems a practitioner should hand-install into A as initial bias, so the searcher does not have to prove them from scratch (printed p. 24; PDF p. 25). That inversion is the paper's own best operational warning: a hard oracle does not abolish the human judgment it replaces, it moves it upstream into specifying the oracle. Vocabulary worth importing: target theorem, proof technique, meta-level collapse. [quick-win]
  6. Retention wired into the architecture is a negative control. In behavioral authority terms the Gödel machine has consumer, channel, and force by construction: check() is the only path to switchbit, and switchbit is the only path to executing switchprog (printed p. 10; PDF p. 11). It shows the open-loop failure mode ("approved change never applied") is contingent on architecture, not intrinsic to change loops. [just-a-reference]

Limitations (our opinion)

Editorial judgment. The lens for a scientific paper is what was not tested — and here the honest answer is nothing. There are no experiments, no baselines, no implementation, and in the two decades since v1 no working Gödel machine has been built. Every claim is a claim about a construction, never evidence about a system that runs. The paper's own Section 4.4 concedes that whether a given initial problem solver can be improved in a provably good way is generally not known in advance (printed pp. 12–13; PDF pp. 13–14).

The Global Optimality Theorem is close to analytic. Its proof amounts to: if you proved that switching now beats continuing to search, then switching now beats continuing to search. The "no local maxima" headline is real but is purchased entirely by loading the future-alternatives quantifier into the target theorem — that is, by making the theorem harder to prove, not by making the search cleverer. All the difficulty is displaced into A and into provability, exactly where Sections 2.4 and 4.4 and the closing question concede it sits. The claim is also easy to vary: swap u, A, or the initial searcher and the guarantee changes shape while the theorem survives untouched, which suggests the theorem carries less weight than its billing.

Two rhetorical moves should not be imported. "If there is no proof of some self-rewrite's utility, then humans cannot do much either" (printed p. 2; PDF p. 3, repeated in FAQ 5 and in the conclusion) is a slogan, not an argument: humans and engineering organisations routinely accept changes on empirical, statistical, and delayed evidence that no formal system will certify — that is the entire soft, interactive, and delayed region of oracle strength spectrum, and it is precisely the region a Gödel machine cannot operate in. Section 6.6's "technical justification of consciousness" (printed p. 22; PDF p. 23) is naming-as-explaining and should be treated as an aside, not a result.

Finally, do not let this source's proximity to reflection blur the reflective system definition, and do not let its name blur into Huxley-Gödel Machine. The Gödel machine has to add a proof system on top of a reflective architecture to get provable improvement; and HGM is a separate modern coding-agent system that borrows the name while replacing the proof with a fallible empirical estimate. Neither is a limit or endpoint of the other, and nothing in this paper says a fallible-oracle system converges toward a Gödel machine.

Write the comparison note kb/notes/goedel-machines-are-a-proof-governed-case-of-reflective-self-modification.md, using the Extracted Mechanics section above as its evidence base: the Gödel machine is a reflective system (a causally connected self-representation, in Maes's sense) whose self-modification is gated on a proof of higher axiomatized utility. The note's job is to state precisely what that gate buys — a globally optimal self-change relative to u, A, resource limits, and the initial searcher — and what it costs: full axiomatization of hardware, environment, and goal, plus the total unreachability of useful-but-unprovable changes. It should cite the target-theorem criterion and the "may rewrite all of p, including the proof searcher" scope, and should explicitly decline to treat the Gödel machine as a limit that fallible-oracle systems converge toward.

Relevant Notes: