用形式化规范指导大模型生成无死锁的通信协议变体
Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models
- 将多方会话类型约束嵌入生成过程，确保协议正确性
- 在多个大模型上实现95.6%~99.5%的有效性，且保持语法正确
- 适合需要高可靠性通信协议的系统开发者使用
在分布式软件系统中，保障通信协议的行为正确性是核心挑战，细微不一致可能导致死锁。协议精化——即安全替换协议以保持正确性和与其他组件的兼容性——至关重要。大语言模型（LLMs）在代码生成和程序合成方面表现出色，但缺乏可靠生成正确行为输出的机制。形式化规范方法（如多边会话类型，MPST）可提供严格保证，包括无死锁，但对自动构建协议精化支持有限。本文提出Syntropy框架，通过MPST规范与大模型协同，指导协议精化的合成。该框架将精化约束直接融入生成过程，确保生成变体满足这些保证。全面评估表明，Syntropy在多个大模型上实现了95.6%~99.5%的有效性，同时保持高语法正确性，并生成多样且非平凡的精化版本。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。