Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Provably Correct Distributed Protocols Without Human Knowledge

Yujie Hui, Xiaoyi Lu, Andrew Perrault, Yang Wang

TL;DR

This work addresses the challenge of automatically synthesizing provably correct distributed protocols under crashes and message losses by treating protocol design as a search over imperfect-information strategies and enforcing correctness via SMT-model checking. The authors introduce GGMS, a framework that combines Monte Carlo Tree Search with a transformer-based action encoder, a global depth-first search to resolve ambiguity, and iterative model-checking feedback to produce state machines that are exhaustively verified for a bounded setting. They prove completeness under mild assumptions and demonstrate that GGMS learns correct protocols where standard MCTS fails, including FloodSet-like consensus and a novel synchronous atomic commit protocol, showing improved success rates over baselines. The work suggests a promising direction for automated, verified protocol synthesis and hints at strong synergy with LLM-based methods for broader generalization, while outlining limitations and future extensions to more expressive fault models and larger process counts.

Abstract

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.

Learning Provably Correct Distributed Protocols Without Human Knowledge

TL;DR

This work addresses the challenge of automatically synthesizing provably correct distributed protocols under crashes and message losses by treating protocol design as a search over imperfect-information strategies and enforcing correctness via SMT-model checking. The authors introduce GGMS, a framework that combines Monte Carlo Tree Search with a transformer-based action encoder, a global depth-first search to resolve ambiguity, and iterative model-checking feedback to produce state machines that are exhaustively verified for a bounded setting. They prove completeness under mild assumptions and demonstrate that GGMS learns correct protocols where standard MCTS fails, including FloodSet-like consensus and a novel synchronous atomic commit protocol, showing improved success rates over baselines. The work suggests a promising direction for automated, verified protocol synthesis and hints at strong synergy with LLM-based methods for broader generalization, while outlining limitations and future extensions to more expressive fault models and larger process counts.

Abstract

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.
Paper Structure (51 sections, 3 theorems, 1 equation, 4 figures, 5 tables, 7 algorithms)

This paper contains 51 sections, 3 theorems, 1 equation, 4 figures, 5 tables, 7 algorithms.

Table of Contents

  1. Introduction
  2. A concrete example.
  3. Can we automate the discovery of such protocols?
  4. Relationship to LLMs.
  5. Background
  6. Distributed Protocols as State Machines
  7. The FloodSet algorithm.
  8. Model Checking
  9. Problem Formulation
  10. State Machine Model
  11. Execution Model
  12. Modeling crashes.
  13. Formal Problem Definition
  14. Assumptions and Limitations
  15. Learning a Distributed Protocol
  16. ...and 36 more sections

Key Result

Theorem 4.1

With a feasible setting, assuming GGMS's unfreezing condition is accurate, GGMS can eventually find a correct state machine.

Figures (4)

  • Figure 1: Simulating the FloodSet protocol. P3 crashes in Round 1 and causes P1 and P2 to have divergent inputs, but P1 and P2 still converge eventually following the protocol.
  • Figure 2: Applying MCTS. Adversarial chooses initial states and lost messages that are likely to violate correctness. Protocol chooses transitions that are likely to achieve correctness.
  • Figure 3: Number of counter examples for ac-3-2 (no unfreezing).
  • Figure 4: Number of counter examples for ac-3-2 (with unfreezing).

Theorems & Definitions (8)

  • Definition 3.1: Protocol Specification
  • Definition 3.2: Setting
  • Definition 3.3: Scenario
  • Definition 3.4: State Machine
  • Theorem 4.1: Search Completeness
  • Theorem 4.2: Group Freezing Preserves Completeness
  • Theorem 2.2
  • proof