TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation

📄 arXiv: 2606.06133v1 📥 PDF

作者: Eric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad

分类: cs.SE, cs.AI, cs.LG, cs.LO

发布日期: 2026-06-04

备注: 12 pages, 5 tables, 3 figures. Submitted at the 21st International Conference on Software Technologies (ICSOFT 2026)

💡 一句话要点

提出TLA-Prover以优化TLA+规范合成问题

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: TLA+ 规范合成 大型语言模型 模型检查 修复策略优化 监督微调 分布式系统 安全关键协议

📋 核心要点

  1. 现有的大型语言模型在生成TLA+规范时，常因语义错误导致无法通过TLC模型检查，表现不佳。
  2. 论文提出TLA-Prover，通过结合监督微调和修复策略优化，提升TLA+规范的合成质量。
  3. 实验结果表明，TLA-Prover在Gold和Diamond等级的通过率分别达到了30%和20%，显著优于现有基线。

📝 摘要（中文）

TLA+是一种用于验证分布式系统和安全关键协议的形式规范语言。现有的大型语言模型（LLMs）在生成TLA+规范时，常因语义原因导致无法通过TLC模型检查器。本文提出了TLA-Prover，一个拥有200亿参数的模型，旨在合成TLA+规范。该模型通过在经过验证的示例上进行监督微调（SFT）和基于修复的群体相对策略优化（GRPO）进行训练。在GRPO阶段，模型学习修复自身被拒绝的规范。实验结果显示，TLA-Prover在一个持出30个问题的基准测试中，Gold和Diamond等级的通过率分别达到了30%和20%，显著高于未调优基线的8.6%。

🔬 方法详解

问题定义：现有的大型语言模型在生成TLA+规范时，常常因语义错误而无法通过TLC模型检查，导致其生成的规范质量较低，表现不佳。

核心思路：论文提出的TLA-Prover模型通过结合监督微调（SFT）和修复策略优化（GRPO），使模型能够在生成规范后自我修复，从而提高生成的TLA+规范的正确性和有效性。

技术框架：TLA-Prover的整体架构包括两个主要阶段：首先是监督微调阶段，在此阶段模型在经过验证的示例上进行训练；其次是修复策略优化阶段，模型学习如何修复自身生成的被拒绝的规范。

关键创新：TLA-Prover的主要创新在于引入了修复策略优化（GRPO），使模型能够在生成规范后进行自我修复，从而显著提升了生成规范的质量和通过率。与现有方法相比，该方法有效减少了语义错误的发生。

关键设计：模型的训练过程中，采用了直接的奖励信号来自TLC，而不是依赖学习的奖励模型。此外，输出结果被分为四个等级：Bronze、Silver、Gold和Diamond，确保模型在生成规范时能够逐步优化其正确性。

🖼️ 关键图片

fig_0

📊 实验亮点

TLA-Prover在持出30个问题的基准测试中，Gold和Diamond等级的通过率分别达到了30%和20%，相较于未调优基线的8.6%提升了约3.5倍，显示出该模型在生成TLA+规范方面的显著优势。

🎯 应用场景

TLA-Prover的研究成果在分布式系统和安全关键协议的验证中具有重要应用价值。通过提高TLA+规范的生成质量，能够有效支持软件工程师在设计和验证复杂系统时，减少错误和提高效率，进而提升系统的安全性和可靠性。

📄 摘要（原文）

TLA+ is a formal specification language for verifying distributed systems and safety-critical protocols. Large language models (LLMs) frequently produce TLA+ specifications that fail the TLC model checker for semantic reasons. Across 25 LLMs, the best public baseline is 26.6% syntactic parse and 8.6% semantic model-check. We present TLA-Prover, a 20-billion-parameter model for TLA+ specification synthesis. Training combines supervised fine-tuning (SFT) on verified examples with repair-based group-relative policy optimization (GRPO). In the GRPO stage, the model learns to fix its own rejected specifications. We also train a direct preference optimization (DPO) variant from the same SFT checkpoint as an ablation. TLC provides the reward signal directly, with no learned reward model. Four tiers grade each output: Bronze (parses), Silver (no warnings), Gold (passes TLC), and Diamond. To reach Diamond, the model's correctness property is automatically altered in a small way; TLC must then detect a violation. If TLC still passes, the property was always-true and contributes nothing; the output fails Diamond. TLA-Prover reaches 9/30 (i.e. pass@1 = 30%) at both Gold and Diamond on a held-out 30-problem benchmark. This is roughly 3.5x the 8.6% untuned baseline. The DPO variant reaches 20% at Diamond. Gold and Diamond coincide at every checkpoint; this prevents the trivial-property failure mode.