Robust Cooperation in the Prisoner's Dilemma

Incidentally, at the MIRI workshop, we soon started referring to the source-code-swap Prisoner's Dilemma between two modal agents as "modal combat".

Or "MODAL COMBAT!", if you prefer.

One downside of having a bot that's too complicated is that it makes the other bot less likely to trust you.

Wow, MIRI is just churning out [1] math papers now.

[1]: Using this expression entirely in a positive sense.

Patrick, congrats on writing this up! It's nice to see MIRI step up its game.

Will two PrudentBots cooperate if they're using theories of different strength?

I don't have any background in automated proofs; could someone please outline the practical implications of this, considering the algorithmic complexity involved?

How effective would a real PrudentBot be if written today? What amount of complexity in opponent programs could it handle? How good are proof-searching algorithms? How good are computer-assisted humans searching for proofs about source code they are given?

Are there formal languages designed so that if an agent is written in them, following certain rules with the intent to make its behavior obvious, it is significantly easier (or more probable) for a proof-finding algorithm to analyze its behavior? Without, of course, restricting the range of behaviors that can be expressed in that design.

Stupid question: are there clear examples of any real-life events that would actually correspond to classic, one-shot Prisoner's Dilemma? I thought that I knew of plenty of examples before, but when I was challenged to name some, all the ones I could think of failed some of the conditions, like being tragedies of the commons rather than PD, or being iterated PD rather than one-shot PD, or the players being able to adapt their plans based on the way the opponent reacts instead of it being a single all-or-nothing choice (arms races are sometimes held up as an example of PD, but there both sides have access to intelligence reports on the kind of strategy that the enemy seems to be adopting, and can adjust their strategy accordingly).

Of course, one can always construct hypothetical scenarios in a way that makes them classic one-shot PD by construction, but being unable to name any clear real-life examples would seem to suggest that this particular scenario isn't that interesting to focus on.

I found situation where PrudentBot behaves suboptimally and a more intelligent agent can do better. I'm considering an opponent I call pseudo tit-for-tat at level N, or PsTitTatBot[N]. PsTitTatBot[0] is simply CooperateBot. For N>0, the strategy for PsTitTatBot[N] is to simulate its opponent running against PsTitTatBot[N-1], and do the same thing its opponent did in the simulation. PrudentBot would have an outcome of (D,D) against PsTitTatBot[N] for any N. However, it's easy for an agent to ensure that against sufficiently high level tit-for-tat agent the outcome will be (C,C). To do this, there must be a specific N such that this agent plays suboptimally against PsTitTatBot[N]. However, the benefit of mutual cooperation at higher levels should compensate for that.

Sounds awesome, great job !

But there is something I didn't get : what does Con() mean in PA+Con(PA) ? Maybe it's stupid question and everyone is supposed to know, but I don't remember ever encountering that symbol, and I can't find it's meaning, neither on Wikipedia nor on mathworld...

Suppose we decide that proving systems are too (NP) hard and we want to restrict agents to polynomial time. If an agent has access to a random coin, can it interactively prove that its opponent is cooperative?

I stumbled across an interesting class of agent while attempting to design a probabilistically proving bot for AlexMennen's contest. The agent below always cooperates with opponents who always cooperate back, (almost) always defects against opponents who always defect against them, and runs in probabilistic polynomial time if its opponent does as well.

def mimic_bot(opponent):
    if random() > ε:
        my_source = quine_my_source()
        return eval(opponent, my_source)      # do as your opponent does to you
    else:
        # unlikely, but necessary to break out of recursive simulations in polynomial time
        return COOPERATE

This particular agent is a bit naïve, but more sophisticated versions (e.g ones that do not cooperate with CooperateBot) are possible. Does anyone have any insight on probabilistically proving opponents will cooperate?

Stupid question... Can one construct ImpudentBot, specifically designed to defeat the analysis done by PrudentBot, say, by forcing it to never halt or something? Or PrudeBot, which resists all attempts at uncovering its true appearance?

I'm coming to this quite late, and these are the notes I wrote as I read the paper, before reading the comments, followed by my notes in the comments.

Has any of the (roughest) analysis been done to bound proving time for PrudentBot? It should be fairly trivial to get very bad bounds and if those are not so bad that seems like a worthwhile thing to know (although what does "not so bad" really mean I guess is a problem.)

Is there a good (easy) reference for the statement about quining in PA (on page 6 below CliqueBot)? Under modal agents Kleene's recursion algorithm is mentioned; should probably be mentioned at first use rather than second?

The proof of theorem 5.1 is losing me where other proofs didn't; I don't understand how minimality of modal rank gives other results.

Reading the comments to answer some of my own questions: orthonormal seems to believe that PrudentBot couldn't be implemented for the LessWrong PD competition, although he did say with algorithmic proof search, would he change his opinion using Kripke semantics?

Vaniver's comment seems like a promising way of thinking about how to identify TrollBots. Or at least, the most promising thing about it I've seen; has this been pursued any further? Perhaps as a possibly-answerable question: call a bot a troll if it can't survive in a population with only itself or only itself and CB and DB (since these are the simplest bots to describe). I'll also note that PseudoTitForTatBot seems like an interesting basic candidate to play against; or say "TimeLimitTitForTatBot" which plays tit for tat until the time limit is near, so no single N can always fool it. Is there a way to (modally; if that is the right word for not-by-quoting-source-code) defeat TLTFTB?

Overall I still have no understanding of theorem 5.1 though. I'm not terribly familiar with the field in general but the other proofs were still fairly straightforward, whereas this proof loses me in the first sentence, without referencing a result I can look up either inside or outside of the paper. Was this written by a different person/at a different time from the rest of the paper? The second sentence is less bad than the first but still worse than the entire rest of the paper.

The nice part about modal agents is that there are simple tools for finding the fixed points without having to search through proofs; in fact, Mihaly and Marcello wrote up a computer program to deduce the outcome of the source-code-swap Prisoner's Dilemma between any two (reasonably simple) modal agents. These tools also made it much easier to prove general theorems about such agents.

Would it be possible to make this program publicly available? I'm curious about how certain modal agents play against each other, but struggling to caculate it manually.

It seems to me that TrollBot is sufficiently self-destructive that you are unlikely to encounter it in practice.

I wonder if there are heuristics you can use that would help you not worry too much about those cases.

Here is another obstacle to an optimality result: define UnfairBot as the agent which cooperate with X if and only if PA prove that X defect against UnfairBot, then no modal agent can get both FairBot and UnfairBot to cooperate with it.

I have two proposed alternatives to PrudentBot.

1. If you can prove a contradiction, defect. Otherwise, if you can prove that your choice will be the same as the opponent's, cooperate. Otherwise, defect.

2. If you can prove that, if you cooperate, the other agent will cooperate, and you can't prove that if you defect, the other agent will cooperate, then cooperate. Otherwise, defect.

Both of these are unexploitable, cooperate with themselves, and defect against CooperateBot, if my calculations are correct. The first one is a simple way of "sanitizing" NaiveBot.

The second one is exactly cousin_it's proposal here.

This is excellent stuff. (And well written, too!)

Thanks for posting this! I'm glad to see more work explained well and formally, and hope to continue seeing preprints like this here.

I'm much happier with this approach than I was a year ago. I don't know how much of that is change on its part, and how much is change on my part; probably some of both.

This echoes the impossibility-of-optimality results of Anderlini [2] and Canning [6] on game theory for Turning machines with access to each others' source codes.

Turning -> Turing

FairBot references itself in its definition, but as with CliqueBot , this can be done via Kleene's recursion theorem

Should there be a reference to Kleene's recursion theorem, or is this common background knowledge for your target audience?

It turns out that, even within the class of modal agents, it's hard to formulate a definition of optimality that's actually true of something, and which meaningfully corresponds to our intuitions about the "right" decisions on decision-theoretic problems. (This intuition is not formally defined, so I'm using scare quotes.)

This seems too simple, but why can't PrudentBot search for a proof that (X(PrudentBot) = C and PrudentBot(X) = D) and defect if a proof is found. If no proof is found, search for the proof of (X(PrudentBot) = C) as before.

I propose a variation of fairbot, let's call it two-tiered fairbot (TTF).

If the opponent cooperates iff I cooperate, cooperate
else, if the opponent cooperates iff (I cooperate iff the opponent cooperates), check to see if the opponent cooperates
and cooperate iff he/she does*
else, defect.

It seems to cooperate against any "reasonable" agents, as well as itself (unless there's something I'm missing) while defecting against cooperatebot. Any thoughts?

*As determined by proof check.

How is "Given an opponent that defects against Defectbot, PrudentBot's behavior is to cooperate with that program IFF PrudentBot can prove that it cooperates with that program" proven? (That is the case stated where PrudentBot plays against itself)

Has it been shown in general that there exists a proof in PA that all agent Y cooperates with PrudentBot for complicated agents Y?

Didn't know about the problems setting. So cool!

Some random thought, sorry if none is relevant:

I think my next step towards optimality would have been not to look for an optimal agent but for an optimal act of choosing the agent - as action optimality is better understood than agent optimality. Than I would look at stable mixed equilibria to see if any of them is computable. If any is, I'll be interested at the agent that implement it (ie randomise another agent and then simulate it)

BTW now that I think about it I see that allowing the agent to randomise is probably strongly related to allowing the agent to not be fully transparent about its program, as it may induce uncertainty about which other agent it is going to simulate.

I finally had time to read this, and I must say, that's an extremely creative premise. I'm puzzled by the proof of theorem 3.1, however. It claims "By inspection of FairBot, PA⊢◻(FB(FB) = C)-->FB(FB=C)."

However, by inspection of fairbot, the antecedent of the conditional should be FB(FB) = C rather than ◻(FB(FB) = C). The code says "if it's a theorem of PA that X cooperates with me, then cooperate." It doesn't say "if it's a theorem of PA that it's provable in PA that X cooperates with me, then cooperate." So I don't believe you can appeal to Lob's theorem in this case. .

I am bothered by the fact that the reasoning that leads to PrudentBot seems to contradict the reasoning of decision theory. Specifially, the most basic and obvious fact of behavior in these competitive games is: if you can prove that the opponent cooperates if and only if you do, then you should cooperate. But this reasoning gives the wrong answer vs. CooperateBot, for Lobian reasons. Is there an explanation for this gap?

What about the agent represented by the formula "P iff provable(P iff Q)"? It clearly cooperates with itself, and its bounded version should be able to do so with much less computing power than PrudentBot would need. What does it do against PrudentBot and FairBot? Is there anything wrong with it?

Two questions about the paper:

Would it be possible to specify FairBot directly as a formula (rather than a program, which is now the case)?

Also, I'm somewhat confused about the usage of FB(FB)=C, as FB(FB) should be a formula/sentence and not a term. Is it correct to read "FB(FB)=C" as "\box FB(FB)" and "FB(FB)=D" as "\box ~FB(FB)"? Or should it be without boxes?

Why do you associate a rank with each modal agent? It looks like it's designed to prevent situations where there are 2 modal agents X and Y such that X tests its opponent against Y and Y tests its opponent against X, but why do such situations need to be avoided? Doesn't the diagonal lemma make them possible?

Hmm... isn't FairBot theoretically imposible because of Halting problem?

I'm not convinced that FairBot cooperates with itself. If we call the statement that FairBot self-cooperates S, then it is not the case that we know that (There exists a proof of S) -> S [which would imply S by Lob's Theorem]. Instead, what we know is (There exists a proof of S of length at most Ackermann(20)) -> S. I'm not convinced that this is enough to conclude S. In fact, I am somewhat doubtful that S is true.

In particular, I can also prove (There exists a proof of (not S) of length at most Ackermann(20)) -> (not S). This is by case analysis:

1. If S is false: By simulating FairBot, I can prove not S, and thus the statement
2. If S is true: Since the axioms are consistent, there is no proof of (not S). Thus, by enumerating all proofs of length at most Ackermann(20), I can prove that there is no proof of (not S) of at most this length, thus proving the above statement. Then again, it is likely that any proof of this implication would need to be longer than Ackermann(20)...

On the other hand, you do need more than Lob's Theorem to prove that FairBot self-cooperates. Anybody know enough logic to resolve this issue?