In this post, I suggest the notion of an interface-relative CliqueBot in open-source game theory. Such a bot cooperates only with the likes of it – from the point of view of a finite number of probing functions. There are several reasons the notion could be valuable. First, it suggests a perspective where programs are secondary to the interface they use – or at least are to be regarded in the context of this interface. This helps put existing bots within one coherent picture and points to their deeper nature. Second, it provides a factory for new bots; I illustrate how it gives rise to many existing and some arguably new ones. Moreover, properties of CliqueBots can perhaps be used to define or study the properties of the corresponding interfaces.

The first sections provide an overview; new material starts from Section 3.

In classic game theory, players commit to actions . Program games add a new layer to this: instead of submitting their actions directly, players submit programs to act on their behalf. Each program takes programs of other players as inputs and outputs the action that its owner will then play. If we let the index denote "all except ", programs have signature . This dependence on is what makes this "open-source"; note however that programs are not players or agents with their own utility.

Example. The original game sits inside the program game via constant-function programs – those that refuse to use the open-sourcedness.

Consider the Prisoner's Dilemma. Classically, only mutual defection is a Nash equilibrium. However, program games can promote mutual cooperation to an equilibrium [1] in different ways:

The easiest way was shown by Tennenholtz in [1] (the idea going back to McAfee, [2]). The program, called CliqueBot , cooperates iff it faces a copy of itself: [2]

def Cl(Q): if Cl == Q return C; return D Clearly, if two players submitted this program, nobody is incentivised to deviate.

CliqueBots catch some flak for being too detail-oriented: any minor change to the code of will break the equilibrium built on " Cl == Q ". This is fair, but the relevance depends on the context: if I know that you are rational and I can show you my Cl code and say "I'll submit this", it is reasonable for you to assume I won't win from lying, copy-paste my code and happily cooperate.

In many contexts we would indeed want a less egoistic and more flexible bot to represent our interests. One interesting attempt is FairBot of Bárász et al. [3]:

def FB(Q): if □Q(FB) == C return C; return D Here assigns True to a statement iff is provable. To speak of provability, one needs a so-called "formal system", the standard example being Peano Arithmetic.

What is ? Pause and try to resolve the question. You will notice that it feels recursive: iff we can prove (that is, ). Turns out that this is not a problem: denote the statement " " by . Then we can prove in our formal system. Löb's theorem gives a proof of . Hence, .

Here is some intuition for this result for those who accept Gödel's incompleteness theorems on intuitive level. Both mutual cooperation and defection are solutions to the fairness equation "cooperate iff the opponent does". However, carries the following asymmetry: since can't prove its own consistency, it has no reason to expect the (unbounded) proof search to fail – even if it searches for a proof of a statement it has already refuted! On the other hand, the proof search for provable statements succeeds, obviously. For mutual defection, we need a proof search to fail – and as we just discussed, we should not expect that even if we can prove defection. Thus, in this setup mutual defection is not such an obvious fixed point [3] as mutual cooperation. For the bounded case (see below), likewise has no reason to expect defection for all . But on the other hand if for some mutual cooperation is provable, it will obviously be provable for all larger .

The same Löbian reasoning shows a stronger claim: for programs denote and . If the theory proves and then and cooperate [4] .

Thus, the resulting equilibrium is much thicker than in the CliqueBot case in the sense that FB engages in mutual cooperation with a variety of programs. Additionally, FairBot seems much more… fair! For example, it cooperates with the CooperateBot that always returns .

There is one problem: FB absolutely need not halt. It may get stuck in a perpetual search for a proof that does not exist. To fix this, Critch introduces in [4] a bounded version of , denoted by , that only considers proofs of length at most . Surprisingly, the corresponding FairBots still cooperate for large .

Even if is finite, proof search can be ridiculously slow. Another problem with programs like this that rely on provability is that they quickly start to depend on consistency axioms of formal systems used, making cooperation seem fragile. Moreover, this approach runs into trouble when programs are somewhat opaque or rely on randomization. Oesterheld suggests a different approach in [5]: perhaps just executing a program is faster than running through all strings checking if each happens to be a proof of cooperation? Then we'd want to remove from FairBot's code and write

def UngroundedBot(Q): return Q(UngroundedBot) Of course, this time nothing saves us from infinite recursion when we pit this bot against itself. The way out is to give up on simulating… sometimes. Let .

def εGroundedBot(Q): if sample(0,1) < ε return C; return Q(εGroundedBot) This bot simulates the opponent with probability and otherwise hopes for the best and cooperates. If it plays itself, the chance to run recursion forever is . In all other cases—basically always—one of the copies cooperates unconditionally, thus convincing the other copy to cooperate.

Here we will again only discuss the Prisoner's Dilemma.

Let's use the word "interface" to describe the way programs can learn about the world. FairBot seems like one of the most "natural" attempts to use the provability interface; meanwhile, the GroundedBot is its brother from the "simulationist" world. Is there a universal way to assign programs to interfaces that would formalize this?

Let us try to construct a reasonable program with a restricted interface . On the one hand, it can only tell those opponents apart whose image under is different. On the other hand, it is reasonable to cooperate with oneself. If we stop right here, we get something like a CliqueBot: a program that cooperates only with its equal – except the interface determines what "equal" means. Here is a more formal definition.

Define a finite interface as a collection of functions whose primitives each take one code input, together with the implicit self . (We will need self primarily for consistent randomization and for access to the code of oneself.) Write their signatures and their combined output as

Note that there is certain rigidity here: first, each is a genuine (partial) function, which restricts how randomness can behave; second, there is a finite number of these. We will also assume that the codomains have decidable equality.

Given such an interface , define its CliqueBot to be the program whose policy is "I cooperate iff you look like me":

def Cl_I(Q): if I_X(X) == I_X(Q) return C; return D Here is self , the current invocation of , and abbreviates .

Example. CooperateBot is [5] ; the classic CliqueBot is for , or, alternatively, for .

I will show how to obtain the other programs from Section 2 as CliqueBots.

Proposition. cooperates with itself whenever evaluating its interface on itself terminates.

Let's start with obtaining FairBot as a CliqueBot.

Definition (Bounded proof interface). Fix a formal system , such as Peano arithmetic. Fix . Define the interface to have a single primitive, which tests whether has a -proof of length at most . Namely, define by where means that has a -proof of length at most .

Proposition. Let , where is large enough to contain the short self-cooperation proof above. Then follows the rule of :

Proof. By the proposition, , and by our choice of its short proof fits the budget. Thus , and (Here means that has a proof in of length at most .) This is exactly FairBot's definition. ∎

We have not used Löb's theorem – what is going on? Do we actually need it to prove that the FairBot self-cooperates? Well, the way I'd draw the line is: we don't need it to prove cooperation, but we need it for the question to make sense. Indeed, to speak of the FairBot, we need to know that different implementations of the same rule yield the same bot. This is Theorem 4.7 from Bárász et al. [3]. This theorem uses Löb's rule, and conversely, such implementation-independence implies this rule.

Note that we could swap and in the definition of FairBot, getting again a reasonably-looking policy, which however fails to self-cooperate. Before we know about this failure, is there a clear reason to prefer FairBot? One answer could be: "it's easier to prove something than to establish proof absence". Now we can also answer this by pointing to FairBot's nature as a well-known program type.

Example. It is still remarkable how this "twin" of FairBot, called CUPOD in Critch et al. [7], fails to self-cooperate (for sufficiently large proof budgets). Note that our FairBot also has a twin. Namely, consider the interface such that Write . The bot by definition has the rule Note that since this bot self-cooperates like any CliqueBot, we would not expect the search for a proof of self-defection on the right-hand side to succeed. If we assume is consistent, then for any , it will indeed fail and so our bot satisfies CUPOD's response condition: For each fixed , can itself prove this equivalence by finitely verifying that the self-defection search fails.

I encourage you to think about why this is not in contradiction with the fact that self-defects. See the footnote for an explanation [6] .

It may be instructive to see what happens for the unbounded version. It's easy to show that our bot is what should be called CUPODIPAC – Cooperate Unless Proof Of Defection and Peano Arithmetic is Consistent [7] : write and put , where is "False". Then proves

Finally, there is a combined interface that searches for both proof of defection and proof of cooperation. In the unbounded case, the resulting bot is equivalent to FairBot. The same holds in the bounded case for large , if is consistent.

Example. Imagine that instead of proof search, the interface method analyzes the opponent with an AI agent and returns if it has confidence that the opponent cooperates. Write for the judgment that the AI's confidence in exceeds . If it also "understands" that , then the rule of the corresponding CliqueBot is Discussing what could mean rigorously is beyond the scope of this text, but regardless, we can anticipate here how the related CliqueBot construction can be valuable. There may be no Löb theorem for . [9] Thus there is no "Löbian" cooperation in this case; however, the above argument still works as soon as the AI agent is smart enough to recognize that is trivially true.

Then this CliqueBot could potentially be a seed to sprout a family of self-cooperating "probabilistic" FairBots. As we discussed above, implementation-independence for modal agents implies Löb's rule, which limits our ambitions a priori. However, we could still hope for restricted implementation-independence. Assume that our AI agent can find short proofs such as that of and thus assigns confidence to them. Assume moreover that its confidence in cooperation depends "continuously" on implementation. For example, if and only differ by an equivalent rewrite of one expression and only looks at the behavior of its opponent, the AI finds and approximately equally likely. Then the Bot