Wei_Dai comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All - Less Wrong

23 Post author: orthonormal 06 September 2012 04:23PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (45)
Tags: tdt decision_theory prisoners_dilemma timeless

Comments (45)

You are viewing a single comment's thread. Show more comments above.

Comment author: Wei_Dai 09 September 2012 10:10:24PM *  5 points [-]

While trying to understand Masquerade better, I came up with the following design, which seems to accomplish something similar, while being much simpler:

def OpportunisticBot(X):
- if "X(OpportunisticBot)=C" is provable in PA-1:
-- return D
- if "X(OpportunisticBot)=C" is provable in PA-2:
-- return C
- return D

where PA-1 is PA with a limit on proof length, and PA-2 is PA with a sufficiently larger limit such that it can prove all true statements of the form "X is not provable in PA-1" by exhaustive search. I claim the following:

  1. OB(DB)=OB(CB)=D
  2. OB(FB)=FB(OB)=C
  3. OB1(OB2)=OB2(OB1)=C

Proof of 3: If either "OB1(OB2)=C" or "OB2(OB1)=C" is provable in PA-1, then PA-2 must be unsound, therefore they are not provable in PA-1. PA-2 can prove that they are not provable in PA-1 by exhaustive search which implies PA-2 can prove that both OB1(OB2) and OB2(OB1) will reach the second if statement, which sets up a Loebian circle.

Can you think of a problem that the Masquerade approach solves but OB doesn't?

Comment author: Wei_Dai 10 September 2012 10:12:29PM *  0 points [-]

It seems possible to generalize this OpportunisticBot idea and port it to the UDT framework (where "opponents" and "the rest of the environment" are not provided separately). I'm not sure if this leads anywhere interesting, but I better write it down before I forget.

Define UDT-OB(input) as follows: (Define "U", "us", "actions", and "mappings" as in Benja's recent post.) For each u in us in descending order, for each m in mappings, check if "UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u" is provable in PA-j, with j incrementing by 1 each time. If it is provable in PA-j, then return m[input].

This works in simple cases where "UDT-OB(i) == m[i] for every i in actions.keys() IMPLIES U() >= u" is easily provable for optimal m* and u*, because assuming PA is sound, UDT-OB will reach the step with m=m* and u=u*, and since PA-j can prove that it reaches this step, it can (using the above IMPLIES statement) prove 'if "UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u" is provable in PA-j then UDT-OB(i) == m[i] for every i in actions.keys() AND U() >= u'.

This also works for some cases where Löbian circles are needed, provided that when each agent tries to prove the necessary statements, they are using proof systems that are strong enough to prove that both agents reach that step. I'm not sure how to arrange this in general.

Powered by Reddit Powered by Reddit