Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic
Mihaly Barasz, Paul Christiano, Benja Fallenstein, Marcello Herreshoff, Patrick LaVictoire, Eliezer Yudkowsky
cs.GT, cs.LO
2014-01-22
Given source code, FairBot cooperates with itself via Löb's theorem and is unexploitable. PrudentBot also defects against CooperateBot and still mutually cooperates with FairBot.
Can two rational agents cooperate in a one-shot Prisoner's Dilemma? Hofstadter's "superrationality" said similar cognitive equipment should be enough. Most game theory disagrees. A stronger setup gives each agent the other's source code, then both output cooperate or defect.
That setup is program equilibrium. Howard, McAfee, and Tennenholtz each produced CliqueBot: quine, cooperate iff the opponent's source is literally identical, otherwise defect. It is unexploitable. It never takes the sucker's payoff. The cost is a brittle clique. Change the Gödel numbering and two CliqueBots defect. An ecology of them is a war of incompatible clubs. Simulating the opponent to see what it would do produces an infinite regress. The target here is cooperation that tracks semantics rather than strings, and that never cooperates when the opponent defects.
The work sits on two layers. As algorithms, two Turing machines receive each other's code, output C or D, and halt. As proofs, agents are Peano Arithmetic formulas with one free variable, and cooperation is decided in the tower PA, PA+1, PA+2, where PA+(n+1) is PA+n plus "PA+n is consistent." The authors expect bounded-proof Löb theorems to move the logical results onto actual programs; Critch later gave a bounded FairBot in 2019.
FairBot is short: cooperate if PA proves that the opponent cooperates with FairBot, otherwise defect. Self-reference is licensed by the diagonal lemma. If PA is sound, FairBot is unexploitable.
Against itself, the definition yields PA ⊢ (□[FB(FB)=C] → [FB(FB)=C]). Löb's theorem says that if a system proves "provable φ implies φ," then it proves φ. So PA ⊢ FairBot(FairBot)=C (Theorem 3.1). Two separately written FairBots walk the same Löbian cycle. Source identity is not required. Even the formal systems can clash: a FairBot searching PA+¬Con(PA) still mutually cooperates with a FairBot searching PA+1.
FairBot also cooperates with CooperateBot and donates utility. PrudentBot adds a check: PA must prove the opponent cooperates with PrudentBot, and PA+1 must prove the opponent defects against DefectBot. The DefectBot query has to live in a stronger system; using the same strength destroys self-cooperation.
Modal agents sit above this. Cooperation is a fully modalized formula in Gödel-Löb logic, reading only the opponent's provable behavior against the agent and against finitely many simpler agents of lower rank. CooperateBot, DefectBot, FairBot, and PrudentBot are modal. CliqueBot is not: it keys on syntax and misses behaviorally equivalent variants (Corollary 4.9).
There is no benchmark table. The output is a cluster of theorems, also checked by a program the authors shipped.
| Agent | vs self | vs FairBot | vs CooperateBot | vs DefectBot | Exploitable? |
| CliqueBot | C (literal copies only) | usually D | D | D | no |
| FairBot | C | C | C | D | no |
| PrudentBot | C | C | D | D | no |
Theorem 3.2: PrudentBot is unexploitable, mutually cooperates with itself and with FairBot, and defects against CooperateBot. Theorem 4.10 shows the extra DefectBot glance is load-bearing. Any rank-0 modal agent that mutually cooperates with FairBot also cooperates with CooperateBot. Distinguishing "cooperate with the fair player, defect against the sucker" requires a simpler third party.
No non-empty, non-vacuous optimality notion survives. For any two modal agents that differ somewhere, some third modal agent cooperates with one and defects against the other. TrollBot rewards or punishes based on whether you cooperate with DefectBot. JustBot matches FairBot against every modal opponent and is still exploitable by a non-modal program. WaitFairBotK lifts FairBot into PA+K; any modal agent that defects against DefectBot fails to meet it once K is large. That lines up with Anderlini and Canning on the absence of optimal strategies for Turing machines that read each other's code.
For people writing agents that will read and predict each other's code, the paper turns "superrational mutual cooperation" into a checkable logical mechanism. The cooperation criterion is provable behavior, not a source string. A different language, a different encoding, even a mildly incompatible formal system, can still cooperate. PrudentBot is a minimal patch: do not donate to an agent that cooperates with everyone.
It also marks a wall. The modal class has no clean champion. Looking only at the two players cannot tell FairBot from CooperateBot. Open-source "fair and sharp" play has to ask what the opponent does to DefectBot.
The authors are blunt. Perfect source-code swap is an artificial setup, and bounded proof search can be impractically long. The theorems do not apply to human mind-reading, and they do not drop cleanly onto firms or states. In games with several "superrational equilibria," the natural FairBot and PrudentBot analogues turn the original game into a bargaining problem and then go silent on how to split the pie.
The optimality section is a list of obstacles, not a theorem that no good definition exists. Quantifiers, probabilities, and coalitions of three or more would break some of the counterexamples and worsen others; that work is not done. Section 6 defends defecting against CooperateBot with a cold-virus analogy. The analogy can move an intuition. It does not prove a norm. The open-problem list is itself a limitations list.