Gödel Machines: Provably Optimal Self-Rewriting AI

This episode explores Jürgen Schmidhuber's 2003–2006 paper on Gödel Machines, a proposed self-referential problem solver that can rewrite any part of its own source code — including the module that decides whether to rewrite itself — but only after producing a formal mathematical proof that the change improves expected utility. The discussion traces the paper's core mechanics: an axiomatic system encoding the machine's hardware, environment, and utility function, a proof searcher hunting for a "target theorem" justifying a switch to new code, and the Bias-Optimal Proof Search (BIOPS) strategy that allocates search effort by technique probability rather than brute force. A central debate centers on the paper's Global Optimality Theorem, which claims any triggered self-rewrite is provably optimal rather than just locally better — with one host pushing back on the strength of that claim while the other points to the theorem's explicit conditionality on the consistency of the underlying formal system. The episode contrasts this proof-driven approach with mainstream reinforcement learning, where algorithms tune policies but never formally justify changes to their own update rules. Listeners interested in the theoretical limits of self-improving AI, formal verification, and the gap between provable guarantees and real-world reliability will find the tension between rigor and practicality especially compelling.

Sources: 1. Goedel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements — Juergen Schmidhuber, 2003 http://arxiv.org/abs/cs/0309048 2. Tiling Agents for Self-Modifying AI, and the Löbian Obstacle — Eliezer Yudkowsky, Marcello Herreshoff, 2013 https://scholar.google.com/scholar?q=Tiling+Agents+for+Self-Modifying+AI,+and+the+Löbian+Obstacle 3. Self-Modification of Policy and Utility Function in Rational Agents — Tom Everitt, Daniel Filan, Mayank Daswani, Marcus Hutter, 2016 https://scholar.google.com/scholar?q=Self-Modification+of+Policy+and+Utility+Function+in+Rational+Agents 4. Space-Time Embedded Intelligence — Laurent Orseau, Mark Ring, 2012 https://scholar.google.com/scholar?q=Space-Time+Embedded+Intelligence 5. The fastest and shortest algorithm for all well-defined problems — Marcus Hutter, 2002 https://scholar.google.com/scholar?q=The+fastest+and+shortest+algorithm+for+all+well-defined+problems 6. Universal Artificial Intelligence: Sequential Decisions based on Algorithmic Probability — Marcus Hutter, 2004 https://scholar.google.com/scholar?q=Universal+Artificial+Intelligence:+Sequential+Decisions+based+on+Algorithmic+Probability

Interactive Visualization: Gödel Machines: Provably Optimal Self-Rewriting AI