发表机构
University of Oxford（牛津大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出Syntropy框架，结合多方会话类型规范与大语言模型合成无死锁通信协议精化，经评估其有效性达95.6%-99.5%，可生成多样且语法正确的协议精化方案。
AI 中文摘要
确保通信协议的行为正确性是分布式软件系统的核心挑战，因为细微的不一致可能导致死锁。在此类场景中，协议精化（即保留正确性及与其他组件兼容性的协议安全替换）至关重要。大语言模型（LLMs）在代码生成与程序综合方面展现出强大能力，但缺乏可靠生成正确行为输出的机制。形式化规范方法（如多方会话类型（MPST））提供包括无死锁在内的严格保证，但对自动构建协议精化的支持有限。本文提出Syntropy框架，用于在MPST规范与LLMs引导下合成协议精化，将精化约束直接纳入生成过程，确保生成变体满足相关保证。全面评估表明，Syntropy在维持高语法正确性的同时，实现95.6%-99.5%的有效性，且在多个LLMs上生成多样、非平凡的精化方案。
英文摘要
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.
