Recursive Improvement in Schmidhuber's Artificial Intelligence
Anonymous manuscript for Higher Categorical Semantics.
Abstract
This survey traces Schmidhuber’s recursive AI from meta-learning to Gödel machines. It models timed rewrites by certificate families in the effective topos and by spans. A Lean 4 specification proves the switch rule and its invariant, and a halting reduction rules out total exact comparison in the unbounded class.
Research context
Schmidhuber’s 1987 thesis makes the method of learning part of the learner’s problem. The Success-Story Algorithm later made modifications persistent by comparing observed reward histories and permitting rollback. The Optimal Ordered Problem Solver (OOPS) froze successful code for reuse on an ordered sequence of tasks. OOPS search guarantees depend on the candidate bias, testing cost and allotted time. PowerPlay searches for a new task together with a modified solver that passes the new task and retains previously recorded skills. These are different ways to make an agent’s experience change how it approaches future tasks. 1987 thesis · Success-Story Algorithm · OOPS · PowerPlay
A neural line uses fast weights and later self-referential matrices whose writable state contributes to computing its own updates. LSTM instead provides a recurrent memory mechanism that supports learning long-range dependencies within a specified training rule. A related line uses learned recurrent world models to guide action or to train a controller. The object being changed matters. A new memory state, a new update strategy and a new proof checker create different claims about future behavior. Fast weights · LSTM · World Models · Modern self-referential weight matrix
The Gödel machine is the central example of proof-driven self-rewrite. Its live image contains a task policy, a searcher for proof-producing programs, a formal theory and checking machinery. The initial theory describes the machine, its utility and relevant environmental facts. A proof technique can propose a switch program and derive a comparison of two settings of the switch bit at a designated future time. The check instruction verifies the form of the theorem and the feasibility of setting the bit in time. Executing the switch program can change the solver, the searcher or the formal system itself. Schmidhuber, Gödel Machines, revised 2006, §§2–5
The checkpoint comparison
A snapshot $s\in S$ records the clock, current code and the working state used by the model. A rewrite $r=(p,\tau)$ supplies program code and a future activation checkpoint. An admissible request $b=(s,r)\in B$ can be bound to the actual snapshot and scheduled in time. The branch $\mathrm{commit}(r)$ commits to that rewrite. The branch $\mathrm{wait}$ continues the actual search process and includes any future rewrites it finds and takes.
For a fixed environment law and objective, let $V(s,a)$ be the value of the entire continuation under branch $a$, starting with the same information at $s$. For example, take the expected sum of discounted net rewards, including computation costs or the opportunity cost of delay. The target is
$$ J(s,r)\quad\Longleftrightarrow\quad V(s,\mathrm{commit}(r))>V(s,\mathrm{wait}). $$
Schmidhuber’s Theorem 4.1 uses global optimality in this specified comparison with continued proof search. To interpret a derivation as a true comparison in the chosen model, we assume semantic soundness of the live checker and theory for these claims. Syntactic consistency is a separate property. A commit paying $8$ can dominate waiting for a payoff of $12$ with probability $1/4$ and $4$ otherwise, since the wait value is $6$. A candidate outside the two compared branches may still have value $10$. The target theorem is a claim about the chosen continuation and the expected reward from the same checkpoint. Original target theorem and Theorem 4.1
Effective and categorical semantics
In the effective topos $\mathbf{Eff}$, encode finite machine descriptions and proof texts by natural numbers. A bounded deterministic computation relation $\mathrm{Run}(p,x,n,y)$ presents a partial universal evaluator. Its domain $D$ is the subobject of $\mathbb N\times X$ defined by $\exists n,y\,\mathrm{Run}(p,x,n,y)$. Determinism gives a map $D\to Y$. Pullback of domains implements composition of partial computations. Code identity remains observable to the machine, which can inspect addresses or elapsed time. Kleene’s recursion theorem supplies an index $q$ with $\varphi_q\simeq\varphi_{f(q)}$ for a total computable transformation $f$ of indices. This equality of partial behavior supports self-reference. The authorization of a rewrite is a further judgment on a timed request. Hyland, The Effective Topos · Kleene, 1938 · Kavvos, 2017
For $b=(s,r)$ let $c_s,T_s$ denote the live checker and theory. Form the object of accepted derivations
$$ C=\{(b,\pi)\mid \mathrm{Check}(c_s,T_s,b,\pi)\}, \qquad q:C\to B . $$
This construction uses a bounded check or a witness of successful checking. In a finite rational environment model, take $j:J\hookrightarrow B$ to be the internal subobject of true comparisons. For more general real-valued models one can instead interpret the certificate family and its truth externally in sets.
Soundness. The live certificate family is sound if and only if $q$ factors uniquely through $j$. Indeed, the soundness sequent says exactly that every point of $C$ projects to $J$. Monicity gives uniqueness. Equivalently, $\operatorname{im}(q)\subseteq J$. For any context map $f:X\to B$, pullback gives the corresponding factorization for $X\times_B C\to X$ and preserves the image. An individual proof lives in a fiber of $q$, while the image remembers its existence. Streicher, Fibered Categories
Composition. A proof-labeled commit is represented by a point of a span $S\leftarrow R\to S$ with an elapsed-time label $\ell:R\to\mathbb N$. The apex retains the rewrite and certificate. Compose two such spans by pullback over the intermediate snapshot, and add their elapsed times. The second event therefore uses the checker and theory in the image produced by the first. Maps preserving both legs and the label are 2-cells. Each association of a finite composite represents the same compatible family of witnesses, so the canonical comparison maps satisfy the bicategory coherence laws. Passing to the image in $S\times S\times\mathbb N$ forgets proof multiplicity and generally gives a noninvertible 2-cell. Shulman, Framed Bicategories and Monoidal Fibrations
The run invariant and its failure
Let $F:S\to S$ be the chosen checkpoint transition, including continued search. A deterministic run can carry its environment stream in the state. Let $\mathrm{Sound}(s)$ mean that the checker and theory at $s$ are semantically sound for the target. Assume $I(s_0)$, $I(s)\Rightarrow I(F(s))$ and $I(s)\Rightarrow\mathrm{Sound}(s)$. Induction gives $I(F^n(s_0))$ for every $n$. Whenever the machine commits, the gate has accepted a proof for that snapshot and rewrite. Soundness then yields the strict comparison at that checkpoint. This is a local-value guarantee at each commit with its own wait baseline.
The greatest $F$-invariant predicate inside an audit predicate $A$ is $A^\infty(s)\Longleftrightarrow\forall n\,A(F^n(s))$. The case $n=0$ gives containment in $A$. Advancing the run shifts the quantifier by one step and preserves the predicate. Any invariant inside $A$ implies this condition by induction.
Initial soundness alone fails to yield this invariant. In the checked example, checker $40$ accepts a rewrite worth $8$ against a wait value of $6$. It installs checker $41$, which accepts every claim. The new searcher selects a second rewrite worth $2$ at a checkpoint where continuing would be worth $5$. The first change satisfies the target while the second fails it. Preserving the checker’s semantic obligation is therefore an independent condition on the path of rewrites.
Lean specification
The companion GodelMachine.lean represents the policy, searcher, theory and checker by writable codes and supplies a parameterized checkpoint interpreter. An offered rewrite commits after four checks: the claim matches the live snapshot, activation lies in the future, scheduling is feasible and the live verifier accepts its proof code. The branch value is a separate parameter.
def Target {U : Type} [LT U] (value : Snapshot → Choice → U)
(s : Snapshot) (r : Rewrite) : Prop :=
value s .keepSearching < value s (.commit r)
def SoundAt {U : Type} [LT U] (rt : Runtime)
(value : Snapshot → Choice → U) (s : Snapshot) : Prop :=
∀ (r : Rewrite) (proofCode : Nat),
rt.check s.image.checker s.image.theory ⟨s, r⟩ proofCode = true →
Target value s rThe kernel checks that a commit has an accepted certificate, that an accepted offer commits, and that stale or expired offers keep searching. It proves the local comparison, the invariant theorem and maximality of the invariant core. It evaluates both choices in the counterexample and proves the failure of preserved soundness. Running lean GodelMachine.lean under Lean 4.24.0 reproduces the checks with the core distribution. The four principal proofs print empty axiom dependency reports. The interpreter callbacks abstract machine instructions, scheduling and utility evaluation, so connecting the specification to a concrete interpreter requires proving the corresponding premises. Lean 4.24.0
Undecidability in the unbounded class
Fix rational $0<\gamma<1$. Given arbitrary code $e$ and input $x$, construct a single proposed rewrite that simulates $e(x)$ and pays $1$ at its first halt, with zero reward otherwise. Let the wait policy yield zero forever. If the program halts and the payoff occurs at time $T$, the commit has value $\gamma^T>0$. If it never halts, the value is zero. A total exact test of the target on this infinite-horizon class would decide halting. The value is nevertheless uniformly approximable since a payoff appearing after cutoff $N$ is at most $\gamma^{N+1}$. Finite rational models with an explicit finite horizon admit exact evaluation of the two specified branches. Computability background
Authorship, automation and supporting files
The manuscript uses an anonymous review byline. ChatGPT assisted with literature synthesis, drafting and development of the Lean specification. The full manuscript gives the formal proofs and linked bibliography. The supporting files are recursive-improvement-in-schmidhubers-ai.pdf and GodelMachine.lean.