Our novel Gödel machine^{1}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 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

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.

Back to Goedel machine home page