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.

1. Program games

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.

2. Three classic examples

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.

3. Generalized CliqueBots

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.

First, we record the obvious

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

Some noteworthy things about this:

1. The same formula holds for the bounded case ^[8] , but for any fixed , is provable within (if we assume in the ambient theory of this text that is consistent). However, can't prove for all at once. This is why we can't apply bounded Löb theorem to get self-defection.
2. We can think of this rule as "I want to be nice, so I will defect only if I prove that you defect... and I can trust my own proofs." Notably, since can't prove , this bot can't tell you it will defect against literally anyone!
3. It may be instructive to trace how this bot solves CUPOD's self-cooperation predicament. Its rule is logically equivalent to CUPOD's rule is logically the same but without the second disjunct. This looks hopeless, since as we discussed, would never have any reason to expect a proof search to fail. CUPODIPAC adds another hopeless clause, namely a search for a contradiction. But it is this clause that actually enables what we want intuitively: it ensures that refuting a statement (here ) makes a proof search for it "terminate". Namely, it enables us to say: if is consistent, there is no proof of the refuted statement (so here); and if it is not consistent, then . Either way, the disjunction holds.
4. This shows how mirroring the interface does not necessarily flip the self-cooperation conclusion. Perhaps CUPODIPAC is the proper "dual" of FairBot, as opposed to CUPOD.

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

def EstimateBot(Q): if □ₐQ(EstimateBot) == C return C; return D

self-cooperates and cooperates with bots of approximately same implementation. (Here it is important that the result of running the AI is an actual function of self and , meaning that any "randomness" that it uses has to come from these inputs. We will return to this point when discussing GroundedBot as a CliqueBot.)

Example. We may not want to cooperate with CooperateBot (for example, we see it as an environment item to take advantage of). To be able to identify it, let us add an interface function that, for example, tells the caller if the target has D in its code. Then the resulting CliqueBot espouses the "defect against CooperateBot" rule.

Instead of syntactic code analysis, we can check for cooperatebotness by probing if a program cooperates with DefectBot. Namely, enrich the interface with the function . Then for sufficiently large , the corresponding CliqueBot is (a bounded version of) PrudentBot of Bárász et al. [3].

Now let's switch to the GroundedBot.

Definition (Grounded simulation view). Fix . Define the interface to have a single primitive: simulate the supplied program against oneself, with probability of returning a common token instead:

Proposition. Let be the grounded simulation view. Then is GroundedBot. More precisely, the bot , whenever the opponent simulation terminates, follows the response rule

Proof. If simulation is skipped, both interface outputs are , so the bot cooperates. Otherwise, the self-cooperation proposition says that the self-simulation returns , so the bot cooperates exactly when the opponent simulation returns – the GroundedBot rule. ∎

I have been lying to you somewhat. Our definitions imply that is a function – we have used it when claiming that CliqueBots self-cooperate. However, it is then not clear how to make all the random decisions at successive levels of simulation uncorrelated, which is assumed in the GroundedBot construction to make the run halt almost surely. We have to make an assumption: self supplies random choices which are fresh at each further level of simulation. A hash of the invocation's identity is one possible idealization.

Here is a table to recapitulate the above:

Interface output	CliqueBot
Empty interface	CooperateBot
	CliqueBot [1, 2]
	FairBot [3]
	, for sufficiently large [3, 4]
	CUPODIPAC
	; under consistency, satisfies CUPOD's response condition
	FairBot
	, for large under consistency
	EstimateBot, assuming confidence in self-cooperation
	requiring D in the opponent's code
	Bounded PrudentBot-type policy [3]
	GroundedBot [5]

3.1 Formal properties

A natural question to ask now is: which properties of these bots come formally from CliqueBotness?

We know that two of the above bots are unexploitable and hence their self-cooperation is an equilibrium. When is this true for generalized CliqueBots?

Let denote the class of acceptable programs.

Definition (Completeness). The interface is complete if for every and every invocation of , whenever both interface outputs are defined.

A complete interface is what the programs would dream of, but it is too strong to hold for our examples. For CliqueBots, the following weakening is sufficient to ensure unexploitability:

Definition (Local completeness). For deterministic terminating programs, the interface is locally complete at , relative to the admissible programs, if for every and every invocation of , whenever both interface outputs are defined.

In the randomized version, we can insert "almost surely" before the implication.

Proposition. The source-matching interface and the bounded-proof interface for large are locally complete at their CliqueBots.

Proposition. If is locally complete at and the relevant executions terminate, then is unexploitable. Thus, two copies of make cooperation a Nash equilibrium of the program game.

Proof. If , the interface outputs on and on agree. Local completeness implies , giving unexploitability. ∎

For GroundedBot, the story is more complicated. It is not unexploitable, as it gambles whenever it is denied the simulation. Thus, it is "almost" unexploitable... on average. The same applies to EstimateBot. We illustrate how average unexploitability properties for these bots are just a consequence of the quality of their interface.

For and , assume that In words: the bot defects at least times as often as its opponent does, up to .

Let the Prisoner's Dilemma payoffs be with (this means: a player gets for defecting against a cooperator, for mutual cooperation, for mutual defection, and for cooperating with a defector). For an admissible , let , and let and be the expected payoffs of and of when they play each other.

Using straightforward calculations, one gets the following results.

Proposition. Let satisfy (1). Then for every admissible :

1. .
2. If , then .

Thus, if , deviating from two copies of gains at most ; for they form a Nash equilibrium.

For the AI Bot, let be the AI's confidence that cooperates, so that cooperates exactly when . Suppose the AI is overconfident by at most on average: for every admissible .

Bot
GroundedBot				, if
EstimateBot
against deterministic				, if
EstimateBot, random

Here by EstimateBot I mean the CliqueBot for (though before I used this name for its "equivalent" rewrite). The third row restricts the admissible opponents to those whose action is deterministic, and needs . In the last row, each invocation draws uniformly from , so that confidence must be .

References

[1] M. Tennenholtz. Program equilibrium. Games and Economic Behavior, 49(2):363–373, 2004.

[2] R. P. McAfee. Effective computability in economic decisions. Technical report, University of Western Ontario, May 1984. https://mc4f.ee/Papers/PDF/EffectiveComputability.pdf

[3] M. Bárász, P. Christiano, B. Fallenstein, M. Herreshoff, P. LaVictoire, and E. Yudkowsky. Robust cooperation in the Prisoner's Dilemma: Program equilibrium via provability logic. arXiv:1401.5577, 2014. https://arxiv.org/abs/1401.5577

[4] A. Critch. A parametric, resource-bounded generalization of Löb's theorem, and a robust cooperation criterion for open-source game theory. The Journal of Symbolic Logic, 84(4):1368–1381, 2019. https://acritch.com/papers/parametric-bounded-lob.pdf

[5] C. Oesterheld. Robust program equilibrium. Theory and Decision, 86(1):143–159, 2019. https://d-nb.info/117482459X/34

[6] E. Cooper, C. Oesterheld, and V. Conitzer. Characterising simulation-based program equilibria. In Proceedings of the AAAI Conference on Artificial Intelligence, 39(13):13735–13744, 2025. https://arxiv.org/abs/2412.14570

[7] Andrew Critch, Michael Dennis, and Stuart Russell. Cooperative and uncooperative institution designs: Surprises and problems in open-source game theory. arXiv:2208.07006, 2022. https://arxiv.org/abs/2208.07006

1. Note that now we may have equilibria of programs and equilibria of payoffs. Our equilibria are often going to be strict as payoff equilibria but weak program equilibria, since one can often safely change a program to its equivalent. ↩︎

2. It takes some work to make sure the program knows its own source – search "quine". For our work it will be most natural to assume that the program just has access to a function that returns its source code. ↩︎

3. The term "fixed point" here means the following. Consider the operator that assigns to a sentence new sentence , for example " is provable". Then the recursive claim (e.g. "we cooperate iff it is provable that we cooperate") can be seen as saying that is a "fixed point" of the operator . ↩︎

4. Prove this as an exercise, using that for any , ↩︎

5. By "is" I mean that they behave the same way. This should not look suspicious since there is no canonical form for each of our example bots. However, this point becomes subtle for modal agents, as we will see. ↩︎

6. Here is why the same proof of self-defection does not work. Bounded Löb is not the inference from to for one fixed . Its parametric form requires a single proof in of (a sufficiently large tail also suffices), and then proves for all sufficiently large . For ordinary CUPOD, with its self-defection statement, the code gives that uniform premise. For our bots, each fixed instance of the premise is provable, but their universal generalization is not. Thus satisfying the same response condition instance by instance does not imply the same self-play. See Lemma 3.6 and the proof of Theorem 3.4 of [7]. See also the unbounded version below. ↩︎

7. If is Peano Arithmetic. ↩︎

8. Actually, not precisely so, since we increase proof length by concatenating proofs. ↩︎

9. For example as soon as the following argument is supported. Let be false. Then is false, so vacuously, is true (provable, true with confidence ). Thus is false for any . See also Stuart Armstrong's "Probabilistic Löb theorem" (2013). ↩︎