用AI自动设计可验证的分布式协议，省去数十年人工调试。
Learning Provably Correct Distributed Protocols Without Human Knowledge
- 将协议设计转为带不完美信息的博弈搜索，用SMT约束保证正确性。
- 在3个以上节点的复杂场景中成功生成正确协议，超越现有方法。
- 适合系统验证、安全协议开发等需要高可靠性的研究者。
可验证的分布式协议是现代分布式系统的核心，但设计极其困难，常需数十年人类投入。这些协议使多个实体在不确定和故障环境下协同达成一致。本文将协议设计建模为具有不完美信息的博弈中的策略搜索问题，并以满足模理论（SMT）形式指定正确性条件。然而，标准多智能体博弈求解方法在此设置下无法学习到正确协议，即使智能体数量较少。为此，我们提出一种学习框架GGMS，结合改进的蒙特卡洛树搜索、基于Transformer的动作编码器、全局深度优先搜索以跳出局部最优，并引入模型检测器反复反馈。通过穷尽模型检查，可验证GGMS输出的协议在有限场景下的所有执行路径均正确。进一步证明，在温和假设下，该搜索过程是完备的：若存在正确协议，GGMS终将找到。实验表明，相较于现有方法，GGMS可在更大规模场景中学习出正确协议。
原文摘要 · Abstract (English)
Provably correct distributed protocols, which are a critical component of modern distributed systems, are highly challenging to design and have often required decades of human effort. These protocols allow multiple agents to coordinate to come to a common agreement in an environment with uncertainty and failures. We formulate protocol design as a search problem over strategies in a game with imperfect information, and the desired correctness conditions are specified in Satisfiability Modulo Theories (SMT). However, standard methods for solving multi-agent games fail to learn correct protocols in this setting, even when the number of agents is small. We propose a learning framework, GGMS, which integrates a specialized variant of Monte Carlo Tree Search with a transformer-based action encoder, a global depth-first search to break out of local minima, and repeated feedback from a model checker. Protocols output by GGMS are verified correct via exhaustive model checking for all executions within the bounded setting. We further prove that, under mild assumptions, the search process is complete: if a correct protocol exists, GGMS will eventually find it. In experiments, we show that GGMS can learn correct protocols for larger settings than existing methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。