web3-基于贝尔曼福特算法（Bellman-Ford ）与 SMT 的 Web3 DeFi 套利策略研究

如何找到Defi中的交易机会

把defi看做是一个完全开放的金融产品图表，可以看到所有的一切东西；我们要沿着这些金融图表找到一些最优的路径，就有可能会发现一些有利可图的机会。这些有利可图的机会对于项目方来说可能是一种攻击

如何在Defi中发现套利或者获利的机会

• 贝尔曼福特算法Bellman Ford Algorithm
  • 负循环检测（Negative cycle detection）
  • 适用于多个市场
  • 在传统金融和DeFi中都被广泛使用
• 定理求解器（SMT）
  • 需要对defi模型编码
  • 可能需要一些启发式算法（heuristic）来进行路径修剪（path pruning）

DeFiPoser-ARB和DeFiPoser-SMT

• DeFiPoser-ARB
  • 建立defi市场图标
  • 检测负周期
  • Bellman Ford-Moore 算法
• DeFiPoser-SMT
  • 状态转换模型
  • 修剪搜索空间
  • 定理证明者
    

📌 图解说明：

这张图其实是货币兑换套利问题的一个例子，常用贝尔曼-福特算法来检测是否存在套利机会（即经过一圈兑换后，能赚到钱，兑换前后资产数量增加）。

📌 图中元素含义：

• 红、黄、绿、蓝的小房子 代表四个不同货币交易市场。
• 每个房子标记了汇率：
  • $\frac{A}{B}=p_1$
  • $\frac{B}{C}=p_2$
  • $\frac{C}{A}=p_3$
  • $\frac{B}{A}=p_4$
• 箭头代表交易路径，箭头上的公式是交易后的资产数量。
• 初始带着 1×A，尝试通过不同路径回来，看是否能变成大于1×A。

📌 中间两张图讲了两种套利路径：

▶️ 中间图（路径一）：

从 A → B → A
利润条件是：
$$p_1\times p_4>1$$
即：如果你先把 A 换成 B，再把 B 换回 A，资产增值了，就存在套利。

---

▶️ 右边图（路径二）：

从 A → B → C → A
利润条件是：
$$p_1\times p_2\times p_3>1$$
同理，如果沿这个路径资产增值了，就存在套利。

📌 这和贝尔曼-福特算法的关系：

贝尔曼-福特算法原本用来在带权图中找最短路径，也能用来检测负权环。

在套利问题中：

• 我们把汇率取对数（通常是 $\log (\text{汇率})$），然后取相反数，变成权值。
• 如果存在一条回路，回到起点，路径和小于0，说明存在套利机会。

📌 算法步骤：

1. 初始化每个点到起点的距离。
2. 对所有边松弛 (Relax) N-1 次。
3. 再执行一次松弛，如果还能更新，说明存在负权环（即套利机会）。
   
   这张图就是用交易路径的方式形象化表示套利路径和条件，而检测这些路径是否满足套利条件，就是贝尔曼-福特算法擅长的事情。

货币套利问题 和 贝尔曼-福特算法 的应用场景

📌 左边这张图：

是一个带权有向图，每个节点代表一个货币，每条有向边代表汇率交易。

• $A\to B$ 的权值是 $-\log p_1$
• $B\to C$ 的权值是 $-\log p_2$
• $C\to A$ 的权值是 $-\log p_3$

为什么用 $-\log p$ 呢？

• 因为原本套利条件是：

$$p_1\times p_2\times p_3>1$$

两边取对数：
$$\log (p_1\times p_2\times p_3)>0$$
转化成：
$$\log p_1+\log p_2+\log p_3>0$$
再乘个 $-1$：
$$-(\log p_1+\log p_2+\log p_3)<0$$

📌 中间部分：

把套利条件转化为：
$$(-\log p_1)+(-\log p_2)+(-\log p_3)<0$$
意思是：
如果图中存在一个环，环上的边权之和 < 0，说明存在套利机会。

📌 右上角小公式：

总结了一下这件事：

• 如果：

$$\prod p_i>1$$

等价于：
$$\sum (-\log p_i)<0$$

📌 右下角框：

说明解决这个问题的方法：

• 使用 Bellman-Ford-Moore 算法
• 时间复杂度：

$$O(|N{|}^2\cdot |E|)$$

（其实一般 Bellman-Ford 是 $O(N\cdot E)$，这里写成 $|N{|}^2\cdot |E|$ 可能是指对所有顶点多轮松弛或特殊实现）

这张图其实讲了一个套利检测的问题：

1. 汇率相乘 > 1 就是套利。
2. 用 $-\log$ 把乘法变加法。
3. 看图中是否存在负环。
4. 用Bellman-Ford算法检测负环。

DeFiPoser-SMT

DeFiPoser 评估

• 96笔在Uniswap，Bancor和Marker DAO上的操作，总共覆盖了25种资产
• Block910000（Dec-13-2019）到10050000（May-12-2020）
• 通过具体执行来进行验证
  

贝尔曼福特算法 VS SMT

总结

本文研究了基于贝尔曼-福特算法和SMT求解器的DeFi套利策略。将DeFi市场建模为金融产品图，利用贝尔曼-福特算法检测负权环（套利机会），并通过SMT对DeFi模型编码进行路径优化。研究提出两种方法：DeFiPoser-ARB建立市场图并检测负周期，DeFiPoser-SMT采用状态转换模型进行空间修剪。实验验证了该策略在Uniswap等平台的有效性，比较了两种算法在检测套利路径时的性能差异。该研究为DeFi领域的套利检测提供了量化分析框架。