.
Jürgen Schmidhuber's
snake trying to swallow itself
robot trying to pull 
itself out of a swamp

GÖDEL MACHINE
SUMMARY

.

FAQ

Gödel
machine
home
page

Gödel machines: self-referential universal problem solvers making provably optimal self- improvements.

Summarized summary: Any utility function (such as expected future reward in the remaining lifetime) can be plugged in as an axiom stored in initial program p. Among other things, p systematically makes pairs (switchprog, proof) until it finds a proof of: "the rewrite of p through current program switchprog implies higher utility than leaving p as is." Since the utility of `leaving p as is' implicitly evaluates all possible alternative switchprogs which an unmodified p might find later, we obtain a globally optimal self-change by executing the current switchprog.

Disclaimer: Gödel machines can be implemented on traditional computers! They have nothing to do with hypothetical super-Turing capabilities and the like.

Given is an arbitrary computational problem whose solution may require interaction with a possibly reactive environment. For example, the goal may be to maximize the future expected reward of a robot. While executing its initial (possibly sub-optimal) problem solving strategy, the Gödel machine simultaneously runs a proof searcher which systematically and repeatedly tests proof techniques. Proof techniques are programs that may read any part of the Gödel machine's storage, and write on a reserved part which may be reset for each new proof technique test. In our example Gödel machine this writable storage includes the variables proof and switchprog, where switchprog holds a potentially unrestricted program whose execution could completely rewrite any part of the Gödel machine's current software. Normally the current switchprog is not executed. However, proof techniques may invoke a special subroutine check() which tests whether proof currently holds a proof showing that the utility of stopping the systematic proof searcher and transferring control to the current switchprog at a precisely defined point in the near future exceeds the utility of continuing the search until some alternative switchprog is found. Such proofs are derivable from the proof searcher's axiom scheme which formally describes the utility function to be maximized (typically the expected future reward in the expected remaining lifetime of the Gödel machine), the computational costs of hardware instructions (from which all programs are composed), and the effects of hardware instructions on the Gödel machine's state. The axiom scheme also formalizes known probabilistic properties of the environment, and also the initial Gödel machine state and software, which includes the axiom scheme itself (no circular argument here). Thus proof techniques can reason about expected costs and results of all programs including the proof searcher.

Once check() has identified a provably good switchprog, the latter is executed (some care has to be taken here because the proof verification itself and the transfer of control to switchprog also consume part of the typically limited lifetime). The discovered switchprog represents a globally optimal self-change in the following sense: provably none of all the alternative switchprogs and proofs (that could be found in the future by continuing the proof search) is worth waiting for.

There are many ways of initializing the proof searcher. Although identical proof techniques may yield different proofs depending on the time of their invocation (due to the continually changing Gödel machine state), there are bias-optimal and asymptotically optimal proof searcher initializations based on variants of universal search (Levin, 1973) and the Optimal Ordered Problem Solver (Schmidhuber, 2002).

Our Gödel machine will never get worse than its initial problem solving strategy, and has a chance of getting much better, provided the nature of the given problem allows for a provably useful rewrite of the initial strategy, or of the proof searcher. The Gödel machine may be viewed as a self-referential universal problem solver that can formally talk about itself, in particular about its performance. It may `step outside of itself' (Hofstadter, 1979) by rewriting its axioms and utility function or augmenting its hardware, provided this is provably useful. Its conceptual simplicity notwithstanding, the Gödel machine explicitly addresses the `Grand Problem of Artificial Intelligence' by optimally dealing with limited resources in general environments, and with the possibly huge (but constant) slowdowns buried by previous approaches (Hutter, 2001, 2002) in the widely used but sometimes misleading O()-notation of theoretical computer science.

The main limitation of the Gödel machine is that it cannot profit from self-improvements whose usefulness it cannot prove in time.

.

Right: Storage snapshot of a not yet self-improved example Gödel machine, with the initial software still intact. See paper for details.


Goedel machine storage