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% 的有效性，同时保持高语法正确性，并能生成多样且非平凡的精化结果。
正文 · AI 翻译
摘要：确保通信协议的行为正确性是分布式软件系统中的一个核心挑战，因为细微的不一致可能导致死锁。在此类场景中，协议精化——即安全地替换协议，同时保持正确性并与其他组件兼容——至关重要。大型语言模型（LLM）在代码生成和程序合成方面展现出强大能力，但缺乏可靠地生成行为正确输出的机制。形式化规约方法，如多参与者会话类型（MPST），提供了严格的保证，包括无死锁性，但对自动构建协议精化的支持有限。在本文中，我们提出了 Syntropy，一个由 MPST 规约和 LLM 引导的协议精化合成框架。它将精化约束直接纳入生成过程，确保生成的变体满足这些保证。我们的综合评估表明，Syntropy 在保持高语法正确性的同时达到了 95.6%-99.5% 的有效性，并在多个 LLM 上产生了多样且非平凡的精化。
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI） |
| 引用为： | arXiv:2607.27964 [cs.SE] |
| （或使用 arXiv:2607.27964v3 [cs.SE] 查看此版本） | |
| https://doi.org/10.48550/arXiv.2607.27964 arXiv 颁发的 DOI，经由 DataCite |
提交历史
来自：Ping Hou [查看电子邮件]
[v1]
2026年7月30日星期四 10:11:33 UTC（415 KB）
[v2]
2026年8月2日星期日 10:30:36 UTC（415 KB）
[v3]
2026年10月13日星期二 17:13:06 UTC（415 KB）
来源：arXiv cs.AI · arxiv.org