An example of self-fulfilling spurious proofs in UDT

More generally, what makes Q dangerous is that (1) it only settles for a spurious moral argument, doesn't accept natural ones, and (2) what it finds is taken seriously by the agent, acted out. As a result, provability of a spurious moral argument provably implies its truth, which by Loeb's theorem makes it true and forces the agent to be thus misled.

The only difference between Q and normal proof search procedures is that the normal procedures are OK with any proof, while Q dislikes natural proofs and ignores them. And this bit of "motivated skepticism" is sufficient to make the preferred spurious proofs come true, Q doesn't just loop without finding anything.

This is a whole new level of Oracle AI unsafety... Take what it says seriously, and it can argue you into doing anything at all. :-)

Excellent! I wonder how far the malicious behavior can be extended.

Here the problem is that A directly uses a valid but malicious inference module Q. If A were built to enumerate proofs by length and act on the first one of the form "A()==a implies U()==u, and A()!=a implies U()<=u", can U be rewritten to guarantee that a particular spurious proof comes up first?

Or if A uses a halting oracle to check through statements of that form, can U be written (incorporating that oracle) so that the halting oracle fails to return for the genuine counterfactual and only returns "True" for a particular spurious one?

def A():  
  Enumerate proofs (in PA) by length  
    if found a proof that "A()==a implies U()==u, and A()!=a implies U()<=u"  
       then return a  

def U():  
  Enumerate proofs in PA+Consistent(PA) by length up to a very large N  
    if found a proof that "A()==1"  
       then return (A()==1 ? 5 : 0)  
  if(A()==2) return 10  
  return 0

1.  U⊦ ProvableU(T) => S              // by inspection of U  
2.  U⊦ S => ~X                        // by definitions of X and S  
3.  U⊦ ProvableU(T) => ~X             // from the previous two  
4.  U⊦ ~X => ~ProvableA(X)            // by the axiom Consistent(PA)  
5.  U⊦ ProvableA(ProvableU(T) => S)              // by A's inspection of U  
6.  U⊦ ProvableA(ProvableU(T)) => ProvableA(S)   // from the previous  
7.  U⊦ ProvableU(T) => ProvableA(ProvableU(T))
        // because PA is sufficient to model provability in any formal system  
8.  U⊦ ProvableU(T) => ProvableA(S) and ~ProvableA(X)    // from 3, 4, 6, and 7  
9.  U⊦ ProvableA(S) and ~ProvableA(X) => T        // by inspection of A  
10. U⊦ ProvableU(T) => T              // from the previous two  
11. U⊦ T                              // by Loeb's theorem  

def Q():
   return Proof1("IsValidProof(X, Q()) => X") +
          Proof2("IsValidProof(X, Q())") +
          X

def A():  
  Enumerate proofs by length and act on the first one of the form
   "A()==a implies U()==u, and A()!=a implies U()<=u"

def U():  
  Enumerate proofs by length up to a very large N
    if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"
    then if(A()==1) return 5  
  if(A()==2) return 10
  return 0

# Hello world
print 'Hello World!'

def U():  
  Enumerate proofs by length up to a very large N  
    if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"  
       then return (A()==1 ? 5 : 0)  
    if found any other proof of the form "A()==a implies U()==u, and A()!=a implies U()<=u"  
       then return (A()==a ? u-1 : u+1)  
  if(A()==2) return 10  
  return 0

def U():  
  Enumerate proofs by length up to a very large N  
    if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"  
       then return (A()==1 ? 5 : 0)  
  Enumerate proofs by length up to a very large N  
    if found any other proof of the form "A()==a implies U()==u, and A()!=a implies U()<=u"  
       then return (A()==a ? u-1 : u+1)  
  return (A()==2  ?  10  :  0)  

def U():  
  Enumerate proofs by length up to a very large N
    if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"
       then if(A()==1) return 5  
    if found any other proof of the same form
       then whatever A() return 0
  if(A()==2) return 10
  return 0

What is your definition of UDT?

If you use the definition given in this paper, then that definition of A is not UDT, simply because it is not guaranteed to "[find] a function mapping sense data to actions that will maximize the utility of outcomes weighted by the probability that the outcome will be caused by the procedure returning that mapping."

It is implicit in the definition that the agent must be able to choose from a set of counter-factual action-selection-functions {f: S -> A}, because it is in this choice the optimisation happens.

P can only be a valid proof that a is the best action exactly when a is the only option, because all other actions where excluded, by the use of non-counter-factual logic.

I know that counter-factual calculations are problematic. But if you take the counter-factual-nes out of UDP, then there are literally nothing left to the definition. Without the counter-factual-nes, everything goes. Any choice is the optimal one, because it was the only one, because that was the choice that actually happened.

Other conclusion is: don't feed the agent it's source code when you feed it a proof that it's output effects a change. Blackbox the output as a variable. When you output a, the world gives u, which is the largest U of any a. Works on newcomb's too (note that this makes no distinction between stuff being put into the boxes before, or after the decision; if the 100% accurate prediction is a given. It simply knows nothing of the causality beyond that implied in the problem)

Let X be the statement "A(Q())==1 implies U()==5, and A(Q())!=1 implies U()<=5". Let Q be the program that enumerates all proofs trying to find a proof of X, and returns that proof if found. (The definitions of X and Q are mutually quined.) If X is provable at all, then Q will find that proof, and X will become true (by inspection of U and A). That reasoning is formalizable in our proof system, so the statement "if X is provable, then X" is provable. Therefore, by Löb's theorem, X is provable. So Q will find a proof of X, and A will return 1.

Doesn't this amount to saying that we've got a proof system that can prove false statements, and is therefore unsound?

ETA: I suppose this relies on the fact that "A(Q())!=1 implies U()<=5" can be made true simply by ensuring that A(Q())=1, regardless of what U equals?