







. 
Jürgen Schmidhuber's



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



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 setup.
 
. 
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 (191519)
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.)
 
. 

A:
1.
Unlike the fully selfreferential Gödel machine,
Lsearch
has a hardwired, unmodifiable metaalgorithm
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 selfimprovements
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, nonselfreferential, unmodifiable, brute force metaalgorithms
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 selfreferential 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 metaalgorithms.
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 selfimprovements
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 selfimprovement 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 speedups 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 selfinspection and provably
useful selfchange (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 MultiAgent Systems III
LNCS 3394, p. 123, Springer, 2005.
 
. 