技术摘要：基于大语言模型的规范引导式无死锁通信协议细化合成

1. 问题陈述

确保分布式软件系统的行为正确性是一项关键挑战，因为通信协议中微妙的不一致往往会导致死锁。尽管大语言模型 (LLMs) 在生成语法正确的代码和满足局部语义属性（如类型安全）方面表现出熟练程度，但它们缺乏保证全局行为正确性的机制，尤其是在复杂的交互场景中。

相反，多方会话类型 (Multiparty Session Types, MPST) 通过异步多方子类型化 (Asynchronous Multiparty Subtyping, AMS) 提供了严格的形式化保证，包括通信安全和死锁自由。AMS 允许一个协议（子类型）安全地替换另一个协议（超类型），同时保留这些属性。然而，自动合成此类子类型并非易事。由于 AMS 通常是不可判定的，且现有的工具链在自动构建有效的协议细化方面支持有限，这一问题变得更加复杂。

本研究解决的核心研究问题是：如何在异步多方子类型化下，系统地合成能够保持行为正确性（特别是死锁自由）的协议细化？

2. 方法论：Syntropy 框架

作者提出了 Syntropy 框架，该框架连接了 LLM 与形式化规范，用于合成有效的协议细化。该框架由两个互补的模块组成：Syntropy-Train 和 Syntropy-Gen。

2.1 Syntropy-Train：学习子类型生成

• 微调： 作者使用 LoRA (Low-Rank Adaptation) 对开源 LLM（如 Qwen2.5-Coder-7B）进行微调。
• 数据构建： 训练数据集包含源自 MPST 文献和合成基准测试的（超类型，子类型）对。子类型通过基于异步子类型算法的启发式程序生成，并由形式化检查器进行验证。
• 表示法： 会话类型被转换为模型友好的 BNF 风格语法（例如，显式的 p!m; T 表示发送，p?m; T 表示接收，以及 REC_X_OPEN/CLOSE 表示递归），以减少歧义。
• 提示词 (Prompting)： 提示词包含了描述转换规则（Identity, RefA, RefB, RefIn, RefOut, Unfold）的理论背景，以引导模型进行结构有效的转换。
• 损失函数： 使用加权标记级损失，优先考虑生成有效的子类型序列而非辅助标签。

2.2 Syntropy-Gen：基于两级监控的约束生成

为了确保超越 LLM 本身所能保证的语义正确性，Syntropy-Gen 在束搜索 (Beam Search) 生成过程中采用了两级监控策略：

• 第 1 级：标记级导数检查（前缀过滤）：
  • 在每个解码步骤，将当前前缀解析为部分会话树。
  • 一个轻量级的共归纳导数检查验证该前缀是否仍能扩展为超类型的有效子类型。
  • 如果检查失败（即不存在有效的完成路径），则立即剪枝该束。这作为一种粗略的过近似，用于尽早消除不可行的路径。
• 第 2 级：基于拓宽算子的不动点检查器（最终验证）：
  • 当候选序列到达结束符 (EOS) 时，将其解析为完整的会话树。
  • 一个完整的子类型检查器（基于导数推理和处理递归的拓宽算子）验证完整的树是否为超类型的有效子类型。
  • 该步骤是保守的；它接受有效的子类型，但由于一般问题的不可判定性，可能会拒绝一些有效的子类型。

这种两级设计平衡了计算效率（第 1 级）与语义严谨性（第 2 级），确保仅保留满足异步子类型关系的候选序列。

3. 核心贡献

1. 具有行为保证的 LLM 生成： 一种能够使 LLM 合成具有保证的死锁自由和通信安全性的 MPST 协议细化的新方法。
2. 规范引导的协议细化： 一种系统化的 MPST 规范编码方式，用于引导并约束 LLM 生成，使其超越局部语法正确性，转向全局行为属性。
3. 集成约束的生成： 一种通过前缀过滤和随后的验证，将约束验证直接集成到合成过程中的两级生成工作流。
4. Syntropy 框架及其评估： 实现并全面评估了该框架，证明了其实现高有效性以及生成多样化、非平凡细化的能力。

4. 实验结果

该框架在两个数据集（文献衍生和合成数据集）上使用多个 LLM（7B 到 32B 参数）进行了评估。

• 有效性： 当使用两级监控时，Syntropy 在所有模型中实现了 95.6%–99.5% 的语义有效性，相比之下，不使用监控的直接生成率显著较低（例如 60.4%）。语法有效性保持在高水平（95.4%–98.1%）。
• 多样性： 该框架能够产生结构上截然不同的细化方案，包括重排序（RefA, RefB）和变异（RefIn, RefOut）转换，而非平凡的变化。
• 数据规模： 性能在约 9,500 个训练对处达到饱和；超过此规模的数据带来的收益微乎其微。
• 消融实验：
  • 移除 两级监控 会导致语义有效性大幅下降（降至 ~60%），证实了其必要性。
  • 移除 提示词 (Prompting) 会降低结构多样性并略微降低语义有效性，表明其在引导转换覆盖范围方面的作用。
• 与前沿模型对比： 虽然前沿模型（如 GPT-5.5, DeepSeek-V4-Pro）在涵盖的少数案例中可以生成高有效性的有效子类型，但其覆盖率极其有限（仅为 4%–18%）。相比之下，Syntropy 在整个基准测试套件中提供了全覆盖。

5. 意义与主张

本文声称 Syntropy 成功解决了 LLM 的生成能力与分布式系统正确性的严苛要求之间的差距。通过将形式化规范 (MPST) 直接集成到生成循环中，该框架确保了合成的协议细化是无死锁且行为兼容的。

作者强调，虽然前沿 LLM 展示了潜力，但它们目前缺乏进行全面协议细化所需的系统化覆盖。Syntropy 证明，经过微调的模型在结合形式化验证约束时，能够可靠地生成难以手动构建的多样且正确的协议变体。这项工作是将 LLM 应用于行为保证不可或缺的安全关键型软件工程任务迈出的重要一步。

承认的局限性：

• 语义有效性指标依赖于一个虽完备但非完全的检查器（由于 AMS 的不可判定性）；因此，被拒绝的候选方案并非被证明一定错误。
• 目前的评估侧重于 MPST 内的子类型生成，向其他形式化体系或生成任务的泛化仍是未来的工作。