AI cooperation in practice

I notice a curious pattern in this post: technically illiterate critical comments get voted up to +1/+2 (even after getting debunked), while technically accurate arguments (replies) stay at 0/+1. Please vote up only things you know you understand, and do vote up comments that debunk incorrect arguments.

ETA: Mostly corrected now.

Cousin_it, do you have an argument that n1 ... n6 < nmax? It seems like one way for the proof to fail is if no matter what nmax is, step 11 forces n1 > nmax.

var s = "...";
return implies(
           proves(s, n1),
           eval(outputs(1)));

Actually, someone shot down my proposed my.C = (my.C == your.C) algorithm, because if two prisoners both defect, that is in a mathematical sense "cooperating if and only if you cooperate". So if the other prisoner is Defection Rock, then my.C = (my.C == your.C) has no consistent solution.

In the first version, there are different ways to go about programming algorithm A, and some will output 1, and some will output 0. In other words, "if A finds a proof that A returns 1" is ambiguous, because it depends on the exact value of A, not the generic description given.

In the second version, both programs output 1, since this is the only possible consistent result. If either program might output a 0, then both programs would have to, which implies that both should have output 1.

\exists n1 \exists n2 \forall code (n1<n2 & proves'(code,n1)=proves(code,n2) )

Edit: The following is not obviously possible, see this comment.

This can be generalized to provide even better algorithms for more general games. Let the following be a simplified outline of the algorithm for cooperation problem, with bounds omitted (players are A and B, our player is A):

function main1() {
    if (proves("A()==B()"))
        return "Cooperate";
    return "Defect";
}

The proof that the outcome is "Cooperate" basically hinges on the provability of Löb statement

proves("A()==B()") => (A()==B())

from which we conclude that A()==B() and so A()=="Cooperate". The statement can be constructed from

proves("A()==B()") => (A()=="Cooperate")
proves("A()==B()") => (B()=="Cooperate")

and so

proves("A()==B()") => (A()==B())

Now, we can get basically the same proof if we use a simpler algorithm for the players:

function main2() {
    if (proves("A()=="Cooperate" && B()=="Cooperate""))
        return "Cooperate";
    return "Defect";
}

This gets rid of the more general relation, but achieves basically the same result. We can improve on this by defecting against cooperating rocks:

function main3() {
    if (proves("A()=="Defect" && B()=="Cooperate""))
        return "Defect";
    if (proves("A()=="Cooperate" && B()=="Cooperate""))
        return "Cooperate";
    return "Defect";
}

This suggests a general scheme for construction of decision-making algorithms: for all possible actions a and b of players A and B, sort the pairs by utility for A, starting from highest, and implement the Löb algorithm for each possibility in turn:

function main4() {
    for(action pairs <a,b> in order of descending utility for A) {
        if (proves("A()==a && B()==b"))
            return a;
    }
    return something;
}

This plays against arbitrary opponents quite well.

function main()
{
    if (proves(outputs(1), n1))
        return 1;
    else if (proves("implies(!proves(outputs(1), n1), eval(outputs(2)))", n2))
        return 2;
    else
        return 0;
}

Does the obvious Lobian proof for 1 still go through if there's a bound on the proof length built into all the sentences?

The generalized action idea, applied to this setting, works as follows. Agents A and B can surrender control over their output to procedures they don't fully understand, but expect to produce good results. That they expect good result is reflected, as in previous construction, in the order in which they check for the possibility:

function main_A() {
    if (proves("A()==Foo() && B()==Bar()"))
        return Foo();
    ...
}

function main_B() {
    if (proves("A()==Foo() && B()==Bar()"))
        return Bar();
    ...
}

Here, the programs might be unable to prove anything specific about the output of Foo() and Bar(), but can still use the trick to coordinate their simultaneous invocation. This is also one way to look at how to solve the coordination problem.

Note that Foo() and Bar() might as well implement the algorithms similar to what we have in main(), so choosing them is a high-level decision, while the low-level decisions still remain to be made by them. Deciding hierarchically makes individual proofs, and individual decisions, easier to perform, so that you don't need a ridiculously big upper bound on which proofs to consider. That we can forget how the hierarchical code is written (say, by inlining most functions) also shows the potential for finding similarly simplifying patterns in the more monolithic code.

This is awesome - great post!

I've scanned briefly through the comments, and didn't see anyone ask this, but apologies if I missed it:

You use the diagonal lemma to establish that there is a piece of code called "box" such that the following is provable:

eval(box) == implies( proves(box, n1), eval(outputs(1)))

But couldn't there likewise be a "box2" such that:

eval(box2) == implies( proves(box2, n1), eval(outputs(2)))

And then couldn't you patch up the proof somehow to show that program has to output 2? Specifically, to get the analogue of step 2, can't you prove that proves(outputs(2), n) implies the negation of proves(outputs(1), n), and hence prove that proves(outputs(2), n) implies outputs(2)?

Even if this is correct, it only applies to the program you use in your proof, where if proves(outputs(2), n) then 2 is returned; whereas the puzzle above doesn't allow for 2 to be returned at all. However, if I'm right then presumably something must be going wrong in the proof?

Edit: Wow, I really am an idiot. I assumed the second statement was true about every statement, but I just realized (by reading one extra comment after posting) that by Lob's Theorem that's not true. But my original idea, that the first statement is all that's required to prove anything, still seems to hold.

Okay, I can follow the first proof when I assume statement 1, but I don't quite understand how cousin_it got to 1. The Diagonal Lemma requires a free variable inside the formula, but I can't seem to find it.

In fact, I think I totally misunderstand the Diagonal Lemma, because it seems to me that you could use it to prove anything. If you replace "outputs(1)" by "2==3", the proof still seems to hold. Statement 2 would still be true with "2==3" (it is true about any statement, after all), and all the logic that follows from those two statements would be true. In fact, by an unclearly written chain of reasoning which I originally intended to post before realizing that it would be much simpler to just say this, all you seem to require is the first statement to be able to prove anything. If I am mistaken, which is probable, then I expect my error lies in the assumption that "outputs(1)" could be replaced by any string of code.

For my original unclear explanation of why the first statement in the proof seems to allow anything to be proven, in case anyone cares for it:

Also, I must be an idiot, but it seems to me that you can prove pretty much anything using 1. As far as I can tell, the "eval(outputs(1))" could be "2==3" or any other statement, and the only reason "eval(outputs(1))" is used is because it's useful in the proof. Given that statement 1 is proven, "eval(box)" must return true, because if it returns false, then "proves(box,n1)" cannot return true, and therefore "implies(proves(box, n1),eval(outputs(1)))" must return true, and false!=true. Assuming that my reasoning is correct (a very questionable assumption, I know), I have just proven that "eval(box)" is true, therefore "prove(box,n1)" is also true for some arbitrarily large n1. Therefore, the "implies" will return "eval(outputs(1))", which must be true for "eval(box)" to equal it. So given my earlier assumption (which I suspect is my error) that "eval(outputs(1))" can be replaced by anything, then I can replace it by any statement, which must return true to equal "eval(box)". So through this, I seem to have proven that "2==3".

Anyone care to point me to my mistake (or, to satisfy my wildest of dreams, say that I appear to be right ;) )?

I think it's possible to coordinate without the huge computational expense, if the programs would directly provide their proofs to each other. Then each of them would only need to check a proof, not find it.

The input to the programs would be a pair (opponent's source, opponent's proof), and the output would be the decision: cooperate or defect.

The algorithm for A would be: Check the B's proof, which must prove that B would cooperate if the proof it gets in its input checks out. If the proof checks out - cooperate, otherwise - defect.

The most obvious implementation for the easy version will return 0 (or, if the length limit is lifted, fail to return at all).

It's important, however, to be clear on just what constitutes a valid proof. Consider the following implementation:

main() {return 1;}

Not valid because it didn't find a proof, you say? On the contrary, assuming we are dealing with idealized mathematical computers that are perfectly deterministic and have no outside inputs, the fact that a program returns a given value on this run does indeed constitute a proof that it will do so on every run.

The point being that, while you can use concepts like proof to draw rigorous conclusions, in the face of counterintuitive things like self reference, you need some experience actually nailing things down before you can be sure you've closed all the loopholes.

Without the very long limit you've added, the easy problem becomes formally undecidable as it leads to an infinite regress. In order to return 1, the program has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and in order to do that it has to determine whether it will return 1, and..... You'll use up your 3^^...^^3 iterations and return 0.

It's a bit like this problem. http://en.wikipedia.org/wiki/Halting_problem

I believe Program A in "the easy version" would return 0. Assuming zero run-time errors, its structure implements the logical structure:

• If A can be proven to return 1 in under n steps, then A returns 1.
• If A cannot be proven to return 1 in under n steps, then A returns 0.

However n is defined (the post proposes n = 3^^^^3), it can be shown by the definition of the word "proof" that:

• If A can be proven to return 1 in under n steps, then A returns 1.

and therefore the first proposition holds for every program, and cannot be used to show that A returns 1.

However, the second proposition also cannot be used to show that A returns 1. If the given condition holds, A does not return 1; if the given condition does not hold, the second proposition demonstrates nothing.

Therefore no property of the program can be used to demonstrate that the program must return 1. Therefore no proof can demonstrate that the program must return 1. Therefore the program will find no proof that the program returns 1. Therefore the program will return 0.

Q.E.D.

This second puzzle is a formalization of a Prisoner's Dilemma strategy proposed by Eliezer: "I cooperate if and only I expect you to cooperate if and only if I cooperate". So far we only knew how to make this strategy work by "reasoning from symmetry", also known as quining. But programs A and B can be very different - a human-created AI versus an extraterrestrial crystalloid AI. Will they cooperate?

And interestingly, posters here only started criticizing this game-theoretic reasoning when I used it. c=/

Why?