Basic Principles of Gödel Machines

Our novel Gödel machine¹derives 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 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. We provide it with 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 problem soving strategy but also a systematic proof searcher seeking an algorithm for modifying the current Gödel machine together with a formal proof that the execution of this algorithm will improve the Gödel machine, according to some utility function or optimality criterion represented as part of the goals. Any utility function (such as expected future reward in the remaining lifetime) can be plugged in as an axiom stored in initial program $p$. In particular, utility may take into account expected computational costs of proof searching and other actions, to be derived from the axioms. During runtime, $p$ 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. This self-improvement strategy is not greedy: 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--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 AIXI$(t,l)$ and HSEARCH, the Gödel machine can improve the proof searcher itself. Unlike HSEARCH it does not waste time on finding programs that provably compute $f(z)$ for all $z \in X$ when the current $x \in X$ 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. While the hardwired brute force theorem provers of AIXI$(t,l)$ and HSEARCH systematically search in raw proof space--they can hide the proof search cost (exponential in proof size) in their asymptotic optimality notation [16,15]--the initial, not yet self-improved Gödel machine already produces many proofs much faster as it searches among online proof techniques: proof-generating programs that may read the Gödel machine's current state. Hence, unlike AIXI$(t,l)$, the Gödel machine can profit from online proof search which may exploit information obtained through interaction with the environment.

This approach raises several unconventional issues concerning the connection between syntax and semantics though. Proofs are just symbol strings produced from other symbol strings according to certain syntactic rules. Such a symbol string, however, may be interpreted in online fashion as a statement about the computational costs of the program that computes it (a semantic issue), and may suggest a Gödel machine-modifying algorithm whose execution would be semantically useful right now as the proof is being created. The proof searcher must deal with the fact that the utility of certain self-modifications may depend on the remaining lifetime, and with the problem of producing the right proof at the right time.

Section 2 will formally describe details of a particular Gödel machine, focusing on its novel aspects, skipping over well-known standard issues treated by any proof theory textbook. Section 2.2.1 will introduce the essential instructions invoked by proof techniques to compute axioms and theorems and to relate syntax to semantics. Section 2.3 will describe one possible initialization of the Gödel machine's proof searcher: Bias-Optimal Proof Search (BIOPS) uses a variant of the already mentioned Optimal Ordered Problem Solver OOPS [38,40] to efficiently search the space of proof techniques. Section 3 will discuss the Gödel machine's limitations, possible types of self-improvements, and additional differences from previous work.

Back to Goedel Machine Home Page