Pact: A Choreographic Language for Agentic Ecosystems

TL;DR

Pact is a choreographic language that incorporates agent choices and preferences, enabling formal reasoning about game-theoretic properties in multi-agent systems with self-interested participants.

Contribution

It extends choreographic programming with game-theoretic concepts, allowing protocol design that accounts for agent self-interest and decision-making.

Findings

Mapped Pact protocols to formal games for reasoning about decision policies

Developed a bounded-rational solver for computing agent decision policies

Applied Pact to multi-party coordination with self-interested agents

Abstract

Recent advances in large language models have led to the rise of software systems (i.e. agents) that execute with increasing autonomy on behalf of users in open, multi-party settings, interacting with untrusted counterparts and managing private information. Choreographic programming offers correct-by-construction protocol-design for such settings, but assumes cooperative participants -- it has no notion of agent self-interest, that is, why an agent will follow a protocol. In this talk we introduce Pact, a choreographic language extended with operations to describe agent choices and preferences, drawing from the rich literature of game theory. Every Pact protocol maps to a formal game, allowing protocol designers to reason about game-theoretic properties of their protocols, such as solving for decision policies. We present Pact's design and a preliminary implementation -- a bounded-rational solver that computes decision policies over Pact protocols -- and findings from applying this language to multi-party coordination with self-interested agentic participants.