.
Jürgen Schmidhuber's
snake trying to swallow itself
goedel machine logo

Gödel Machine FAQ

Answers to some of the frequently asked questions received since the publication of the Gödel Machine TR in 2003. Last update: 19 Aug 2005
Gödel
machine
home
page
Q1: Does the exact business of formal proof search make sense in an uncertain real world?
A: Yes, it does. We just need to insert into the original software p(1) the standard axioms for representing uncertainty and for dealing with probabilistic settings and expected rewards etc. Compare the discussion of probability axioms and the definition of utility as an expected value in the paper. Also compare the overview pages on reinforcement learning and universal learning machines living in probabilistic environments. Human machine learning researchers routinely prove theorems about expected rewards in stochastic worlds - a machine equipped with a general theorem prover and appropriate axioms can do the same.
.
Q2: The target theorem seems to refer only to the very first self- change, which may completely rewrite the proof- search subroutine. Doesn't this make the proof of the Global Optimality Theorem invalid? What prevents later self- changes from being destructive?
A: This is fully taken care of. Please have a look once more at the proof of the Global Optimality Theorem, and note that the first self- change will be executed only if it is provably useful (in the sense of the present untility function) for all future self- changes (for which the present self- change is setting the stage). This is actually the main point of the whole self- referential set-up.
.
Q3 (related to Q2): The Gödel machine implements a meta- learning behavior: what about a meta- meta, and a meta- meta- meta level?
A: The beautiful thing is that all meta- levels are automatically collapsed into one: any proof of a target theorem automatically proves that the corresponding self- modification is a useful basis for all further self- modifications affected by the present one, in recursive fashion.
.
Q4: The Gödel machine's software can produce only computable mappings from input sequences to output sequences. What if the environment is non- computable?
A: Many physicists actually do assume the real world makes use of all the real numbers, most of which are incomputable (but compare an alternative view of physics). Nevertheless, theorems and proofs are just finite symbol strings, and all treatises of physics contain only computable axioms and theorems, even when some of the theorems can be interpreted as making statements about uncountably many objects, such as all the real numbers (note though that the Löwenheim- Skolem Theorem (1915-19) implies that any first order theory with an uncountable model such as the real numbers also has a countable model). Generally speaking, formal descriptions of non- computable objects do not at all present a fundamental problem for the Gödel machine - they may still allow for finding a strategy that provably maximizes utility. If so, a Gödel machine can exploit this. If not, then humans will not have a fundamental advantage over Gödel machines.
.
Q5: Isn't automated theorem- proving very hard? Current AI systems cannot prove nontrivial theorems without human intervention at crucial decision points.
A: As computers are getting faster, more and more important mathematical proofs (four color theorem etc) heavily depend on automated proof search. And traditional theorem provers do not even make use of our novel notions of proof techniques and O()-optimal proof search. Of course, some proofs are indeed hard to find by any method, but here humans and Gödel machines face the same fundamental limitations.
.
Q6: Don't the "no free lunch theorems" say that it is impossible to construct universal problem solvers?
A: No, they do not. They refer to the very special case of problems sampled from i.i.d. uniform distributions on finite problem spaces. See the discussion of no free lunch theorems in the OOPS paper.
.
Q7: Can't the Gödel machine switch to a program switchprog that rewrites the utility function to a "bogus" utility function that makes unfounded promises of big rewards in the near future?
A: No, it cannot. It should be obvious that rewrites of the utility function can happen only if the Gödel machine first can prove that the rewrite is useful according to the present utility function.
.
Q8: Is the Gödel machine computationally more powerful than a Turing machine?
A: No, of course not. A traditional computer such as a Turing machine becomes a self- referential Gödel machine by loading it with a particular form of machine- dependent, self- modifying code. Gödel machines cannot overcome the fundamental limitations of provability and computability first exhibited by Kurt Gödel (1931). (See the section about limitations.)
.
Q9: Which are the advantages of Gödel machines over universal search or Lsearch (Levin 1973; Levin attributes similar ideas to Adleman) and its incremental extension, the Optimal Ordered Problem Solver OOPS?
A: 1. Unlike the fully self-referential Gödel machine, Lsearch has a hardwired, unmodifiable meta-algorithm that cannot improve itself. It is asymptotically optimal for problems whose solutions can be quickly verified in O(n) time (where n is the solution size), but it will always suffer from the same huge constant slowdown factors (typically >> 10^1000) buried in the O()-notation. The self-improvements of a Gödel machine, however, can be more than merely O()-optimal, since its utility function may formalize a stonger type of optimality that does not ignore huge constants just because they are constant.

2. Unlike the Gödel machine, neither Lsearch nor OOPS are applicable to general reinforcement learning (RL) problems where the goal is to maximize the expected cumulative future reward within the remaining expected lifetime. Here it is impossible to quickly verify the usefulness of some behavior or program by simply executing it, since this evaluation would consume the learner's entire life! That is, the naive test of whether a program is good or not would consume the entire life. That is, we could test only one program; afterwards life would be over. So general RL machines need a more general notion of optimality, and must do things that plain Lsearch and OOPS do not do, such as predicting future tasks and rewards. No fundamental problem though for a properly axiomatized Gödel machine!

.
Q10 (somewhat related to Q9): Which are the advantages of Gödel machines over AIXI(t,l) (ECML 2001; see here) and the asymptotically fastest algorithm for all well- defined problems (Hsearch) (IJFCS 2002; see here), both developed by Schmidhuber's former postdoc Marcus Hutter (now senior researcher at IDSIA)?
A: 1. The theorem provers of Hsearch and AIXI(t,l) are hardwired, non-self-referential, unmodifiable, brute force meta-algorithms that cannot improve themselves. That is, they will always suffer from the same huge constant slowdowns buried in the O()-notation (typically >> 10^1000). But there is nothing in principle that prevents the truly self-referential code of a Gödel machine from proving and exploiting drastic reductions of such constants, in the best possible way that provably constitutes an improvement, if there is any.

2. The demonstration of the O()-optimality of Hsearch and AIXI(t,l) depends on a clever allocation of computation time to some of their unmodifiable meta-algorithms. The Global Optimality Theorem of the Gödel machine, however, is justified through a quite different type of reasoning which indeed exploits and crucially depends on the fact that there is no unmodifiable software at all, and that the proof searcher itself is readable and modifiable and can be improved. This is also the reason why its self-improvements can be more than merely O()-optimal.

3. Hsearch uses a ``trick'' of proving more than is necessary which also disappears in the sometimes quite misleading O()-notation: it wastes time on finding programs that provably compute f(z) for all z in problem domain X even when the current f(x) (x in X) is the only object of interest. A Gödel machine, however, needs to prove only what is relevant to its goal formalized by its axiomatized utility function u. For example, the u of a general reinforcement learner is the cumulative future expected reward. This u completely ignores the limited concept of O()-optimality, but instead formalizes a stronger type of optimality that does not ignore huge constants just because they are constant.

4. Both the Gödel machine and AIXI(t,l) are in principle applicable to the task of maximizing expected future reward (Hsearch is not). But the Gödel machine is more flexible as we may plug in any type of formalizable utility function (e.g., worst case reward), and unlike AIXI(t,l) it does not require an enumerable environmental distribution, and is not restricted to O()-optimality.

(Nevertheless, we may use AIXI(t,l) or Hsearch to initialize the substring e of policy p which is responsible for interaction with the environment. The Gödel machine will replace e as soon as it finds a provably better strategy.)

.
Q11: Aren't there problems with undecidability? For example, doesn't Rice's theorem (1953) pose problems?
A: Not at all. Of course, the Gödel machine cannot profit from a hypothetical useful self-improvement whose utility is undecidable, and will therefore simply ignore it. Compare the section on fundamental limitations of Gödel machines (and humans, for that matter).

Nevertheless, unlike previous methods, a Gödel machine can in principle exploit at least the provably good improvements and speed-ups of any part of its initial software.

.
Q12: Is the Gödel machine conscious?
A: If we equate the notion of ``consciousness'' with the ability to execute unlimited formal self-inspection and provably useful self-change (unlimited except for the limits of computability and provability), then the Gödel machine and its Global Optimality Theorem do provide the first technical justification of consciousness in the context of general problem solving. Compare Popper, Routledge, London, 1999: "All life is problem solving", and J. Schmidhuber, Goedel machines: Towards a Technical Justification of Consciousness. In D. Kudenko, D. Kazakov, and E. Alonso, eds.: Adaptive Agents and Multi-Agent Systems III LNCS 3394, p. 1-23, Springer, 2005.
.