Open-Source Game Theory

If we imagine a society of AI systems, we would like this society to foster collaboration and cooperation, and minimize deception and distrust. In one ideal, we solve the individual alignment problem and each person, government, corporation, or entity has AI systems that represent their values faithfully. Even in this world, these systems would have to negotiate with each other. How do we model that game-theoretic problem, and reason about it?

One approach uses the fact that, unlike human brains, we have a high degree of transparency and access to AI systems by virtue of them being able to inspect their code. Thus it makes sense to model a world of AI systems which can read each other's source code. We can try to make precise and formal the idea of “I will cooperate if you will!”

Formally, consider FairBot, which meets some OtherBot, and performs the following computation in its source code: I will cooperate with OtherBot if and only if I can prove OtherBot cooperates with me.

It is worth pausing here, because it is not technically possible to refer directly to your own source code. This type of self-reference is well studied. One may enumerate all computable functions and write, for a number f, FairBot(f) for the program which cooperates with O if and only if there is a proof that O cooperates on the function corresponding to f. Kleene's recursion theorem then gives an f such that the corresponding function is FairBot(f). This makes FairBot completely well specified, with no infinite regression.

FairBot will never be exploited: it never cooperates against an opponent that defects. But this is not sufficient, since we could get the same property by always defecting. It is a theorem of Robust Cooperation in the Prisoner's Dilemma that FairBot cooperates against itself.

Theorem (Löb's theorem). Let □ denote provability in a sufficiently strong formal theory. If the theory proves □P → P, then it proves P. Equivalently, in modal notation:

□(□P → P) → □P.

To see that FairBot cooperates with itself, let Q be the statement FairBot(FairBot) = C. By FairBot's source code, we can prove □Q → Q. Applying Löb's theorem to Q gives the conclusion.

From now on we refer to FairBot as DUPOC (Defect Unless Proof Of Cooperation).

More interesting interactions

One may define more interesting agents. CUPOD cooperates unless it can prove its opponent defects, and DUPOC defects unless it can prove its opponent cooperates. It is not immediately obvious how these robots perform against each other. Both CUPOD and DUPOC cooperate against FairBot.

Theorem (self-play for CUPOD and DUPOC). In the bounded setting of Cooperative and uncooperative institution designs, for all sufficiently large proof-length bounds k,

outcome(DUPOC(k), DUPOC(k)) = (C,C)

and

outcome(CUPOD(k), CUPOD(k)) = (D,D).

This is counterintuitive: CUPOD seems the nicer robot, yet it defects against itself. One potential source of intuition, not fully formal, is that CUPOD will cooperate against itself if there is no proof that it will not. But assuming consistency of the proof system, one can never show there is not a proof of something.

This shows up more clearly when considering DUPOC versus CUPOD. It is impossible to prove in PA that CUPOD cooperates against any opponent: to do so, one would have to prove that there is no proof of defection for the opponent. Assuming consistency, PA cannot prove that a proof of an arbitrary statement does not exist, because it cannot prove its own consistency. Hence DUPOC will not find a proof that CUPOD cooperates, and so will defect. Symmetrically, CUPOD will cooperate against DUPOC.

There are other bots, such as PrudentBot and CIMCIC (Cooperate If My Cooperation Implies Cooperation), and their behavior depends on the subtle wording of their definitions. See Cooperative and uncooperative institution designs for more details and open questions.

One issue is that programs are not guaranteed to terminate, because a search for a proof might never end. Therefore one may consider bounded versions, such as FairBot(k), which cooperates if and only if it can find a proof of length at most k that the opponent will cooperate. We use □_kφ to mean “there is a proof of φ of length at most k.”

Theorem (parametric bounded Löb). Let p(k) be a formula with one free variable, and let f(k) be an increasing computable function growing asymptotically at least like log(k). If

⊢ ∀k > k₁ (□_f(k)p(k) → p(k)),

then for some k̂,

⊢ ∀k > k̂, p(k).

Using this theorem one may prove that CUPOD(k) defects against itself and DUPOC(k) cooperates with itself for sufficiently large k. However, the following is unknown (see Critch et al., Open Problem 3).

Problem. What is the outcome of DUPOC(k) versus CUPOD(k) for sufficiently large k? Equivalently, is

outcome(DUPOC(k), CUPOD(k)) = (D,C)

eventually true?

The reason this is unclear is that it unpacks to something like X ⇔ ¬□_k¬□_kX. It asks for there not being a short proof of something, so one cannot simply apply Gödel's second incompleteness theorem. The paper has several more questions along the same lines.