一句话：提出 AMM 的抽象操作模型，形式化证明其结构与经济性质，并给出套利问题的一般解。
自动做市商（AMM）是 DeFi 中最突出的应用之一，允许用户无需交易对手即可交换加密代币，已有实现采用多种复杂经济机制。本文提出一种 AMM 理论，核心是用户与 AMM 交互的抽象操作模型，可通过实例化经济机制具体化。作者利用该理论形式化证明 AMM 的一系列基本性质，涵盖结构与经济方面；证明时抽象掉具体实现中的经济机制，识别保证性质的充分条件。特别地，他们为套利问题给出一般解，该问题是 AMM 经济机制背后的主要博弈论基础。
Automated market makers (AMMs) are one of the most prominent decentralized finance (DeFi) applications. AMMs allow users to trade different types of crypto-tokens, without the need to find a counter-party. There are several implementations and models for AMMs, featuring a variety of sophisticated economic mechanisms. We present a theory of AMMs. The core of our theory is an abstract operational model of the interactions between users and AMMs, which can be concretised by instantiating the economic mechanisms. We exploit our theory to formally prove a set of fundamental properties of AMMs, characterizing both structural and economic aspects. We do this by abstracting from the actual economic mechanisms used in implementations, and identifying sufficient conditions which ensure the relevant properties. Notably, we devise a general solution to the arbitrage problem, the main game-theoretic foundation behind the economic mechanisms of AMMs.
@article{paperbot1637,
title = {A theory of Automated Market Makers in DeFi},
author = {Massimo Bartoletti and James Hsin-yu Chiang and Alberto Lluch-Lafuente},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 4},
year = {2022},
doi = {10.46298/lmcs-18(4:12)2022}
}