一句话：提出 Syntropy，将多播会话类型规范作为精化约束注入 LLM 生成过程，合成无死锁且多样的通信协议精化。
分布式软件系统中，通信协议的行为正确性至关重要，细微的不一致就可能引发死锁；协议精化——在保持正确性与组件兼容性的前提下安全替换协议——因而十分关键。大语言模型（LLM）在代码生成与程序合成上表现优异，却缺乏可靠产出行为正确结果的机制；多播会话类型（MPST）虽能提供包括死锁自由在内的严格保证，却难以支持自动构造协议精化。本文提出 Syntropy：一个以 MPST 规范为引导、结合 LLM 的协议精化合成框架，它将精化约束直接嵌入生成过程，从而确保生成的协议变体满足这些保证。在多个 LLM 上的综合评估表明，Syntropy 的有效性达到 95.6%–99.5%，同时保持较高的语法正确性，并能产生多样且非平凡的精化。
Ensuring behavioural correctness in communication protocols is a central challenge in distributed software systems, as subtle inconsistencies can lead to deadlocks. In such settings, protocol refinement – the safe substitution of a protocol that preserves correctness and compatibility with other components – is essential. Large language models (LLMs) have demonstrated strong capabilities in code generation and program synthesis, yet lack mechanisms to reliably produce outputs with correct behaviour. Formal specification approaches, such as multiparty session types (MPST), offer rigorous guarantees, including deadlock freedom, but provide limited support for automatically constructing protocol refinements. In this paper, we present Syntropy, a framework for synthesising protocol refinements guided by MPST specifications and LLMs. It incorporates refinement constraints directly into the generation process, ensuring the generated variants satisfy these guarantees. Our comprehensive evaluation indicates that Syntropy achieves 95.6%–99.5% validity while maintaining high syntactic correctness, and produces diverse, non-trivial refinements across multiple LLMs.
@inproceedings{abs-2607-27964,
title = {Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models},
author = {Yang Li and Ping Hou and Nobuko Yoshida},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3837469}
}