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.

翻译：近年来，大语言模型的进步推动了软件系统（即智能体）的发展，这些系统在开放、多方的环境中代表用户以日益增强的自主性执行任务，与不可信对手交互并管理私有信息。编舞编程为此类场景提供了“正确性即构设计”的协议制定方法，但其假设参与者是合作的——缺乏对智能体自利行为的描述，即智能体为何会遵循协议。本报告中，我们引入Pact，一种扩展了描述智能体选择与偏好操作的编舞语言，其核心借鉴了博弈论的丰富理论。每个Pact协议均可映射为形式化博弈，使协议设计者能够分析协议的博弈论特性，例如求解决策策略。我们展示了Pact的设计与初步实现——一种在Pact协议上计算决策策略的有理有界求解器——以及将该语言应用于含自利智能体参与者的多方协调场景中的发现。