Connectionists: Goedel Machines, Universal AI, Consciousness

[Juergen Schmidhuber]

Kurt Goedel was born 100 years ago. 75 years ago he
layed the foundations of theoretical computer science
with his work on universal formal languages and the limits
of proof and computation (1931), just 5 years after Julius
Lilienfeld patented the transistor, and 10 years before
Konrad Zuse completed the first working
program-controlled computer (1941).

Goedel (or Gödel) constructed self-referential statements
that talk about themselves, in particular, about whether
they can be derived from a set of given axioms through a
computational theorem proving procedure.  He went on to
construct statements that deny their own provability, to
demonstrate that traditional math is either flawed in a certain
sense or contains unprovable but true statements.

We use Goedel's self-reference trick to build a universal,
fully self-referential, self-improving, optimally efficient problem
solver. A Goedel Machine is a computer whose original software
includes axioms describing the hardware and the original
software (this is possible without circularity) plus whatever is
known about the (probabilistic) environment plus some formal
goal in form of an arbitrary user-defined utility function, e.g.,
cumulative future expected reward in a sequence of optimization
tasks. The original software also includes a proof searcher which
uses the axioms (and possibly an online variant of Levin's
universal search) to systematically make pairs ("proof'', "program'')
until it finds a proof that a rewrite of the original software
through "program'' will increase utility. The machine can be
designed such that each self-rewrite is necessarily globally
optimal in the sense of the utility function, even those rewrites
that destroy the proof searcher.

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 GM and its Global Optimality
Theorem can be viewed as providing the first technical
justification of consciousness.

Goedel Machine papers up to 2006 (Goedel Centenary):
http://www.idsia.ch/~juergen/goedelmachine.html

Juergen Schmidhuber