In the previous post, we looked at how networks of counterfactual mechanisms can be used to make logical commitments in open source games. And this post goes through an example!

I Reject Your Incentives and Substitute My Own

Alice and Bob are designing open-source programs to play the game $G$ on their behalf. Alice decides that a negotiation process is a useful mechanism to handle an incentive misalignment in $G$ , and designs AliceBot to direct its logical crystal ball to a different game $N (G)$ , which is a negotiation over conditional commitments for $G$ .

Since AliceBot has BobBot's source code, it simulates how a negotiation between them would go. This introduces new instances of AliceBot and BobBot, so let's call the instances that will actually implement any policy Implementers, and the instances which negotiate conditional commitments over those policies Negotiators.

Implementer AliceBot supplies both Negotiators with all the relevant information they need for this negotiation. Conveniently, this negotiation game includes a communication channel where Negotiators can send each other messages. This happens to make it a lot easier to coordinate than in the underlying game $G$ .

Negotiator AliceBot sends over a preliminary message offering to negotiate over of conditional joint commitments $Φ \subseteq Π$ , and sends over the conditions that Implementer AliceBot will be verifying before implementing its part of $Φ$ . In this negotiation protocol, it is now Negotiator BobBot's turn to reply with Implementer BobBot's or else terminate negotiations.

Transitive Logical Line-Of-Sight

To understand how that instance of BobBot responds, we need to switch over to Bob's POV. Inconveniently, the strong superrationality postulate failed to hold: Bob reasoned differently than Alice about how to solve their incentive misalignment and designed BobBot to look first at some completely different mechanism-counterfactual game. That instance of AliceBot has enough information to know that its Implementer instance isn't going to condition its behavior on the output of this hypothetical game, and so helpfully terminates with an error message rather than make conditional commitments that its Implementer instance won't uphold.

Conveniently, BobBot was also designed with a fallback in this case, and launches a powerful formal verification tool that quickly builds a model of...