From: Nick Hay (nickjhay@hotmail.com)
Date: Sun Sep 11 2005 - 14:01:08 MDT
Wei Dai wrote:
> Another direction, taken by Marcus Hutter's AIXI-tl and Schmidhuber's
> Godel Machine, is to essentially hard wire difficult-to-prove/unprovable
> mathematical conjectures into the AI as unchangeable assumptions. This
> may not be obvious at first glance so I'll explain. The way those AIs
> work is to start with an initial policy (handcrafted program for making
> decisions) and then systematically search for provable improvements to
> the policy. The initial policy necessarily makes implicit or explicit
> assumptions about the truth value of mathematical conjectures. Such an
> assumption can't be changed unless it can be proved to be false,
> otherwise it's impossible to prove that changing it won't lower expected
> utility.
This is not how AIXI-tl works.
In its proving phase, AIXI-tl searches through all proofs of length
smaller than a fixed size, extracting all proofs that prove:
VA(p) = "for any fixed history, policy p's estimate of its future value
is <= its (uncomputable, but lower semicomputable and well defined)
xi-expected value"
for some policy p. After extracting this set of policies, it leaves
proof theory behind. This "mathematical reasoning" is about probability
theory not within it, and is done in a standard brute-force way.
The formal system F, and the formalisation of VA in F, are unchecked
inputs to the AIXI-tl: it doesn't attempt to validate them in any sense.
The formalisation of VA, in particular, is assumed correct. But this
doesn't fall within "difficult-to-prove/unprovable mathematical
conjectures".
-- Nick Hay
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT