Next: Fast Initial Proof Searcher Up: Introduction and Overview Previous: Previous Work: Best General

## Basic Principles of Gödel Machines

Our novel Gödel machine1derives its name and its power from exploiting provably useful changes of any part of its own code in self-referential fashion. Its theoretical advantages over the previous approaches can be traced back to the fact that its notion of optimality is less restricted and that it has no unmodifiable software at all.

Its bootstrap mechanism is based on a simple idea. Its initial software or program includes an axiomatic description of (possibly stochastic) environmental properties and of the Gödel machine's goals and means. The latter not only include some initial -encoded problem soving strategy but also a -encoded systematic proof searcher seeking some program switchprog for modifying the current together with a formal proof that the execution of switchprog will improve , according to some -encoded utility function or optimality criterion represented as part of the -encoded goals. Any utility function (such as some robot's expected or worst-case future reward in its remaining lifetime) can be plugged in as an axiom stored in the initial . In particular, utility may take into account expected computational costs of proof searching and other actions, to be derived from the -encoded axioms. During runtime, systematically makes pairs (switchprog, proof) until it finds a proof of: `the immediate rewrite of p through current program switchprog implies higher utility than leaving p as is'. Then it executes switchprog, which may completely overwrite . The Global Optimality Theorem (Theorem 2.1) shows that this self-improvement strategy is not greedy: since the utility of `leaving as is' implicitly evaluates all possible alternative switchprogs which an unmodified might find later, we obtain a globally optimal self-change--the current switchprog represents the best of all possible relevant self-improvements, relative to the given resource limitations and the initial proof search strategy.

Unlike HSEARCH, the Gödel machine does not waste time on finding programs that provably compute for all when the current is the only object of interest. It is neither limited to AIXI(t,l)'s assumption of an enumerable environmental distribution nor to its particular expected reward utility function, since we may plug in worst-case or other types of utility functions as well.

Next: Fast Initial Proof Searcher Up: Introduction and Overview Previous: Previous Work: Best General
Juergen Schmidhuber 2003-12-11