Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements

Motivation

• The approach targets the limitation that traditional problem-solving and learning algorithms are hardwired and cannot theoretically improve themselves without human-designed algorithms and proofs.The proposed system instead leaves proof search and arbitrary computable self-improvement to the machine.Source: §1 · p. 3

Contribution

• Gödel machines can rewrite arbitrary computable parts of their own code after an embedded proof searcher proves the rewrite useful under a formal utility function.The formalization includes the utility function, hardware, and complete initial code as axioms.Source: §1 · p. 3
• Their self-rewrites are globally optimal because the proof must establish that waiting for alternative self-rewrites would yield lower utility.This rules out local improvements relative to the encoded utility function and formal system.Source: §1 · p. 3
• The initial proof searcher is O()-optimal, while self-reference allows provably useful speed-ups to any initial software component, including the searcher itself.These speed-ups can improve slowdowns hidden by O()-notation when their utility is provable.Source: §1 · p. 3

2.1 Set-up and Formal Goal

• Gödel machines operate over discrete hardware cycles, updating internal state and possibly a dynamic environment through a hardwired transition function.The environment may react to past outputs and may be probabilistic.Source: §2.1 · p. 4
• The initial software contains a sub-optimal environment-interaction policy and a proof-search policy, while variables encode time, inputs, outputs, and the program itself.Outputs can influence future environmental inputs, and the initial program may include a traditional reinforcement-learning algorithm.Source: §2.1 · p. 4
• The formal goal is to maximize future success or utility, with utility functions able to represent expected rewards, computational costs, lifespan, or worst-case objectives.The framework covers both one-shot computational problems and ongoing interaction with an initially unknown environment.Source: §2 · p. 3, §2.1 · pp. 4–5

2.2 Basic Idea of Gödel Machine

• The proof searcher systematically tests proof-generating programs until one proves that executing a self-rewrite yields higher utility than leaving the current program unchanged.The rewrite may replace the entire program, including the proof searcher.Source: §2.2 · p. 5
• Global optimality follows because the utility of leaving the program unchanged evaluates alternative rewrites that the unmodified machine could discover later.Thus the selected rewrite is not merely a greedy local improvement under the stated resources and initial search strategy.Source: §2.2 · p. 5

2.3 Proof Techniques and an O()-Optimal Initial Proof Searcher

• The initial proof searcher uses an online extension of Universal Search to test proof techniques against axioms describing hardware transitions, the initial program, environmental properties, and utility.The axioms let proof techniques reason about the future effects of programs, including the proof searcher.Source: §2.3 · p. 5

2.4 Limitations of Gödel Machines

• Gödel machines cannot exploit self-improvements whose usefulness they cannot prove, whether because the axioms are insufficient or available time and space are limited.Pathological environments and utility functions may prevent any target theorem from being proved.Source: §2.4 · p. 6
• Unlike previous hardwired approaches, Gödel machines can in principle speed up any initial software component, including problem-independent slowdowns hidden by O()-notation.This remains conditional on the utility of the speed-up being provable.Source: §2.4 · p. 6

3.1 Proof Techniques

• Proof techniques systematically generate proofs using arithmetic, theorem retrieval, inference rules, temporary storage, and controlled manipulation of candidate self-rewrites.The instructions include get-axiom, apply-rule, delete-theorem, set-switchprog, check, and state2theorem; invalid inference applications interrupt the current technique.Source: §3.1 · p. 7, §3.2 · pp. 8, 10, 11

3.2 Important Instructions Used by Proof Techniques

• The check() instruction executes a rewrite only after the final theorem proves that switching from the current program yields greater utility than continuing the search for alternatives.After verifying timing conditions, check() activates switchbit and transfers control to switchprog, which may rewrite all non-reserved state components, including p.Source: §3.2 · pp. 8, 10, 11

3 Essential Details of One Representative Gödel Machine

• The machine’s axiom scheme formalizes hardware dynamics, instruction costs, rewards, environment behavior, uncertainty, initial state, and utility so proofs can reason about machine states and outcomes.Hardware may be modeled as a Turing machine or microprocessor, while environment and reward assumptions are encoded within the same formal system.Source: §3.2 · pp. 8–9

3.2 Important Instructions Used by Proof Techniques

• The proof system can convert safely observable current state into time-labeled theorems, allowing proof techniques to exploit environmental inputs and sometimes use execution itself to determine program outputs.state2theorem first checks whether reading a state substring could change it, then records a theorem when the observation is considered stable.Source: §3.2 · pp. 11–12
• Self-observation is constrained because reading rapidly changing state can alter the observable state, although axioms and prior observations may sometimes support indirect deductions.Fast variables such as instruction pointers may require hardware snapshots or predictive reasoning to make useful observations possible.Source: §3.2 · p. 11

3 Essential Details of One Representative Gödel Machine

• The formal theory must be sufficiently strong to prove target theorems, but its axioms and inference rules remain defining parameters of each Gödel machine.The paper notes that standard probability axioms can be inserted to enrich uncertainty reasoning, while the formal encoding can include the hardware and its self-description.Source: §3.2 · pp. 8, 10, 12

4.1 Globally Optimal Self-Changes, Given u and A Encoded in p

• A proved self-change is globally optimal: executing the current switchprog has higher utility than waiting for a later alternative, assuming consistency of A.The proof compares executing the current modification with continuing the search for any future modification.Source: §4.1 · pp. 12–13

4.2 Alternative Relaxed Target Theorem

• The same global-optimality argument applies when the target theorem requires only that a self-change will not reduce utility.Replacing “>” with “≥” makes the machine change itself once it proves the rewrite is at least as good as waiting.Source: §4.2 · p. 13

4.3 Global Optimality and Recursive Meta-Levels

• A proved self-modification automatically accounts recursively for all later self-modifications affected by it, collapsing the system's possible self-referential meta-levels into one.The claim follows from the fully self-referential setup.Source: §4.3 · p. 13

4.4 How Difficult is it to Prove Target Theorems?

• Proof difficulty depends on the task and axioms: simple environments can yield short target-theorem proofs, while undecidability can make some improvements unprovable.The paper notes that the machine can investigate provability itself, but cannot prove every useful change.Source: §4.4 · pp. 13–14
• A proof technique need only establish which option has higher expected utility, rather than compute either utility exactly.For example, proving that a factor-of-two proof-search speedup is worth its negligible rewrite cost may suffice.Source: §4.4 · p. 14

5 Bias-Optimal Proof Search (BIOPS)

• BIOPS applies Universal Search to online proof search, where the same proof technique can produce different proofs because state inputs change over time.The initial solver may still be improved relative to the problem-specific utility function.Source: §5 · p. 14

5.1 Online Universal Search in Proof Space

• BIOPS allocates search according to a probability bias over proof techniques and tests techniques in phases with bounded execution and reversible state effects.The method runs techniques meeting P(w) ≥ 2^-i, limits each run to 2^iP(w) steps, and undoes its effects.Source: §5.1 · pp. 14–15
• BIOPS can rewrite its own proof-search process because tested proof techniques can inspect the machine and invoke check(), potentially replacing the searcher itself.This self-reference allows improvements beyond the initial O()-optimal complexity order.Source: §5.1 · p. 15
• If an unknown proof technique produces a proof of difficulty k in at most f(k) steps, BIOPS finds such a proof in O(f(k)) steps.The overhead 1/P(w) is constant with respect to k.Source: §5.1 · p. 15

5.2 How a Surviving Proof Searcher May Use the Optimal Ordered Problem Solver to Solve Remaining Proof Search Tasks

• When the proof searcher survives, BIOPS freezes successful techniques, reuses them in later tasks, and allocates half of new-task search to reused techniques and half to fresh ones.This is essentially 8-bias-optimal: reuse can accelerate solvable tasks without significantly slowing search when reuse does not help.Source: §5.2 · p. 16
• Global optimality is independent of BIOPS specifically because the theorem applies to whichever initial proof searcher is chosen.BIOPS is one initialization, not a requirement of the global-optimality result.Source: §5.2 · p. 16

6.1 Possible Types of Gödel Machine Self-Improvements

• Gödel machines can provably modify time allocation, policies, axioms, utility functions, proof-search routines, hardware, or even simplify themselves when doing so improves utility.Limited rewrites may be easier to prove useful than total rewrites, while utility-proving constraints govern changes to objectives and target theorems.Source: §6.1 · p. 17

6.2 Example Applications

• The framework covers time-limited optimization, fast theorem proving, bounded-resource reinforcement learning, and optimizing any formalizable suboptimal problem solver.Examples include shortest-path search, Goldbach-conjecture proof production, gasoline-seeking robots under the Speed Prior, and parallel proof search.Source: §6.2 · p. 18

6.3 Probabilistic Gödel Machine Hardware

• Probabilistic Gödel machines extend expectation calculations and proof verification to stochastic hardware, where formal statements may hold only with specified probabilities.Probabilistic settings also avoid some consistency problems because predictions with probability below 1.0 need not contradict observations.Source: §6.3 · p. 18

6.4 Relations to Previous Work

• Unlike Universal Search, Gödel machines are self-modifying, can address lifelong reinforcement learning, and can prove utility-relevant improvements rather than accepting huge O()-notation constants.Universal Search is limited to quickly verifiable inversion problems and is not directly applicable when evaluating a behavior consumes the learner’s lifetime.Source: §6.4 · p. 19
• Compared with HSEARCH [17] and AIXI(t,l), Gödel machines have modifiable proof searchers, exploit provable constant-factor reductions, and support arbitrary formalizable utilities without requiring enumerable environmental distributions.Their Global Optimality Theorem relies on the proof searcher itself being readable and improvable, unlike the hardwired meta-algorithms of those systems.Source: §6.4 · pp. 20–21
• Unlike OOPS [48, 44] and empirical metalearners, Gödel machines can prove properties of otherwise untestable behaviors and need not rely on observed success to justify self-modifications.OOPS can still serve as a bias-optimal proof-search submodule, while success-story and related learners can seed the initial policy.Source: §6.4 · pp. 21–22

6.5 Are Humans Probabilistic Gödel Machines?

• The paper leaves open whether humans are probabilistic Gödel machines, noting that human uncertainty-processing systems may differ substantially from expectation calculus and logic.The passage presents this as an unresolved question rather than a conclusion.Source: §6.5 · p. 22

6.6 Gödel Machines and Consciousness

• Gödel machines provide a technical account of consciousness as self-awareness through total self-reference, because provably beneficial self-changes and proof-search modifications support their problem-solving optimality.Their entire behavior is open to introspection and modification, allowing the system to “step outside of itself” through provably good changes.Source: §6.6 · p. 23

6.7 Frequently Asked Questions

• Formal descriptions of noncomputable objects do not fundamentally prevent Gödel machines from finding provably utility-maximizing strategies; without such strategies, humans have no fundamental advantage.The passage notes that physical theories use finite symbol strings and computable axioms and theorems even when discussing uncountable objects.Source: §6.7 · p. 24
• Automated theorem proving remains difficult, but humans and Gödel machines share the same fundamental limitations in finding hard proofs.The discussion notes that important proofs increasingly depend on automated search, while traditional theorem provers lack Gödel machines’ proof-technique and O()-optimal search notions.Source: §6.7 · p. 24
• No-free-lunch theorems [62] do not rule out constructing universal problem solvers; they concern the special case of problems sampled from i.i.d. uniform distributions on finite problem spaces.The discussion refers readers to an earlier paper.Source: §6.7 · p. 24
• A Gödel machine cannot rewrite its utility function opportunistically because it must first prove that the rewrite is useful under the current utility function.Thus, a rewrite to a bogus utility function cannot be justified merely by promising large near-term rewards.Source: §6.7 · p. 24
• Gödel machines cannot exploit self-improvements whose utility is undecidable, but can in principle use any provably good improvement or speed-up to their initial software.This limitation parallels the fundamental limits discussed for humans and includes issues raised by Rice’s theorem [32] and Blum’s speed-up theorem [3, 4].Source: §6.7 · p. 24

• Self-referential proof systems make it possible to construct theoretically sound, fully self-referential, optimally efficient, general problem solvers.Source: §7 · p. 25
• The initial software combines a problem solver with an O()-optimal proof searcher that tests proofs about its own future performance.The axioms encode the utility function, hardware, and initial code, allowing the system to search for provably useful rewrites.Source: §7 · p. 25
• Practical Gödel machines still require selecting useful theorems as axioms so the initial searcher avoids proving them from scratch and keeps constant overhead small.Source: §7 · p. 25