In the alternative algorithm for the five-and-ten problem, why should we use the first proof that we find? How about this algorithm:

A2 :=
  Spend some time t searching for proofs of sentences of the form
  "A2() = a → U() = x"
  for a ∈ {5, 10}, x ∈ {0, 5, 10}.
  For each found proof and corresponding pair (a, x):
    if x > x*:
      a* := a
      x* := x
  Return x*

If this one searches long enough (depending on how complicated U is), it will return 10, even if the non-spurious proofs are longer than the spurious ones.

I guess then it would have to prove that it will find a proof with x > 0 within t. This is difficult.

Decision Theory

by abramdemski, Scott Garrabrant 1 min read31st Oct 201837 comments


Ω 24

Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.

(A longer text-based version of this post is also available on MIRI's blog here, and the bibliography for the whole sequence can be found here.)

The next post in this sequence, 'Embedded Agency', will come out on Friday, November 2nd.

Tomorrow’s AI Alignment Forum sequences post will be 'What is Ambitious Value Learning?' in the sequence 'Value Learning'.