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
读得到对方源码的一次性囚徒困境里，FairBot 凭 Löb 定理与自己稳健合作且不可剥削；PrudentBot 还能对 CooperateBot 背叛，并与 FairBot 互合。
一次性囚徒困境里，两个完全理性、互相知道对方理性的人该不该合作，争论了几十年。Hofstadter 的「超理性」说相似的认知能力就该推出互合，多数博弈论不买账。更强的设定是：双方能读到对方源码，再同时输出合作或背叛。
这个设定叫 program equilibrium。Howard、McAfee、Tennenholtz 各自给过 CliqueBot：用 quine 认出「源码与自身字面相同」就合作，否则背叛。它不可剥削，永远吃不到傻瓜收益。代价是合作圈极脆，换一套 Gödel 编码就会互叛。一群 CliqueBot 等于一堆互相开战的小圈子。互相模拟对方则容易无穷回归。这篇要的是：合作对语义而不是对字符串，并且对方背叛时自己绝不合作。
工作在两个层面。算法层面，两个图灵机互给源码，输出 C 或 D，并保证停机。证明层面，把 agent 写成带一个自由变元的 Peano 算术公式，在 PA、PA+1、PA+2 这串系统里判定合作。PA+(n+1) 的公理是 PA+n 再加上「PA+n 一致」。作者相信有界证明长度的 Löb 定理能把逻辑结果搬回可停机程序；2019 年 Critch 后来给出了有界 FairBot。
FairBot 的规则极短：若 PA 能证明「对方对 FairBot 合作」，就合作，否则背叛。定义里引用了自己，对角引理让这合法。假定 PA 可靠，FairBot 不可剥削。
自己对上自己时，定义恰好给出 PA ⊢ (□[FB(FB)=C] → [FB(FB)=C])。Löb 定理说：如果系统能证明「可证 φ 蕴含 φ」，那它就能证明 φ。于是 PA ⊢ FairBot(FairBot)=C（定理 3.1）。两条不同实现的 FairBot 也能走同一圈 Löbian cycle，不要求源码字面相同，甚至形式系统可以不兼容：跑在 PA+¬Con(PA) 上的 FairBot，仍能和跑在 PA+1 上的 FairBot 互合。
FairBot 会对 CooperateBot 合作，白送效用。PrudentBot 补一刀：PA 证明对方对自己合作，并且 PA+1 证明对方会对 DefectBot 背叛，两条件同时成立才合作。查 DefectBot 必须用更强系统；用同一档次会失去与自己互合的能力。
再往上是模态 agent：合作与否由一条完全模态化的 GL 公式决定，公式只看对方对自己、以及对若干更低 rank 的简单 agent 的可证行为。CooperateBot、DefectBot、FairBot、PrudentBot 都在这个类里。CliqueBot 不在，因为它会认字符串，认不出行为等价的变体（推论 4.9）。
没有基准分数，产出是一组定理，并被作者写的程序核对过。
| agent | 对自身 | 对 FairBot | 对 CooperateBot | 对 DefectBot | 可剥削？ |
| CliqueBot | 合作（仅字面相同） | 通常背叛 | 背叛 | 背叛 | 否 |
| FairBot | 合作 | 合作 | 合作 | 背叛 | 否 |
| PrudentBot | 合作 | 合作 | 背叛 | 背叛 | 否 |
定理 3.2：PrudentBot 不可剥削，与自己、与 FairBot 互合，并对 CooperateBot 背叛。定理 4.10 说明 PrudentBot 多看的那一眼 DefectBot 不是装饰：任何 rank 0 的模态 agent，一旦能与 FairBot 互合，就必然也对 CooperateBot 合作。想要「跟公平的人合作、对盲信的人背叛」，必须借助更简单的第三方。
最优性没有非空且非平凡的定义。任意两个行为不同的模态 agent，都能造出一个第三方对其中一个合作、对另一个背叛。TrollBot 按「你是否对 DefectBot 合作」来赏罚；JustBot 和 FairBot 对模态对手行为等价，却能被非模态程序剥削。WaitFairBotK 把 FairBot 架到更高的 PA+K 上，任何会对 DefectBot 背叛的模态 agent，在 K 足够大时都跟它对不上。这和 Anderlini、Canning 关于源码博弈里不存在最优策略的结论同方向。
对写会互相读代码、互相预测的 agent 的人，这篇把「超级理性互合」从哲学口号收成一条可核验的逻辑机制。合作条件是可证行为，不是源码字符串，换语言、换编码、甚至换一套不完全兼容的形式系统，仍可能互合。PrudentBot 给出一个最小补丁：别给无条件合作的傻瓜送钱。
它也划出做不到的事。模态框架里没有干净的最优 agent。只看双方、不看第三方，分辨不了 FairBot 和 CooperateBot。想在开源博弈里做「公平且精明」，至少要能问「对方对 DefectBot 会怎样」。
作者写得很直：源码互换是极度人工的设定，有界版本的证明搜索可以长到无法实用。定理不直接适用于人类读心，也不宜直接套到公司或政府。多「超级理性均衡」的协调博弈里，FairBot 与 PrudentBot 的自然推广只会把原博弈变成讨价还价，给不出怎么分钱。
最优性一节是一串障碍，不是一个定理说「不存在好定义」。加入量词、概率、三人以上联盟，现有反例有些会失效，有些会更糟，论文没做完。哲学第 6 节用感冒病毒当 CooperateBot 的类比来为「该背叛 CooperateBot」辩护，类比能说明直觉，证明不了规范性。开源问题清单本身就是局限清单。