arXiv：cs.AI· Yang Li, Ping Hou, Nobuko Yoshida·· 6 小时前
Syntropy：用 LLM 与 MPST 规范合成无死锁通信协议精化
Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
AI 导读
研究者提出 Syntropy 框架，将 multiparty session types（MPST）规范约束直接注入 LLM 生成过程，用于合成无死锁的通信协议精化版本。评估显示其生成结果有效性达 95.6%-99.5%，并保持高语法正确性，在多个 LLM 上均能产出多样且非平凡的精化方案。
正文
Abstract: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.
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2607.27964 [cs.SE] |
| (or arXiv:2607.27964v3 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2607.27964 arXiv-issued DOI via DataCite |
Submission history
From: Ping Hou [view email]
[v1]
Thu, 30 Jul 2026 10:11:33 UTC (415 KB)
[v2]
Sun, 2 Aug 2026 10:30:36 UTC (415 KB)
[v3]
Tue, 13 Oct 2026 17:13:06 UTC (415 KB)
来源：arXiv：cs.AI · arxiv.org