arXiv cs.AI· Yang Li, Ping Hou, Nobuko Yoshida·· 3 天前AI 评分23
Syntropy：用 LLM 与 MPST 规范合成无死锁通信协议精化
Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
AI 导读
Syntropy 是一个由 MPST 规范与大语言模型引导、用于合成通信协议精化的框架，它将精化约束直接嵌入生成过程，确保生成的协议变体满足无死锁等保证。评估显示，Syntropy 在多个 LLM 上达到 95.6%-99.5% 的有效性，同时保持高语法正确性，并能生成多样且非平凡的精化结果。
正文 · 原文
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