Re: mathematical reasoning

From: Wei Dai (
Date: Sun Sep 11 2005 - 20:35:58 MDT

Nick Hay wrote:
> 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"

Oh, right. AIXI-tl works a bit differently in this regard from Schmidhuber's
Godel Machine, and what I wrote only applies to the Godel Machine. But the
situation here isn't any better. In the case of AIXI-tl, a policy isn't
allowed to make use of unproved conjectures in estimating its future value,
because then it would be unable to prove that the estimated value is not
more than the xi-expected value. So a policy that implicitly or explicitly
assumes a conjecture that is likely to be true has no advantage over a
policy that assumes the opposite. Instead of the assumed conjectures being
fixed as in Godel Machine's case, in an AIXI-tl they would instead change
randomly from policy to policy.

This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT