用AI自动生成可验证的分布式系统规范，正确率提升三倍以上。
TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation
- 通过自我修复机制让模型自动修正错误的规范代码。
- 在30个测试问题上，黄金级通过率达30%，钻石级达30%。
- 适合开发安全关键系统、需要形式化验证的工程师和研究者。
TLA+是一种用于验证分布式系统和安全关键协议的形式化规范语言。大型语言模型（LLMs）常生成语义错误的TLA+规范，导致TLC模型检测器失败。在25个主流LLM中，最佳公开基线的语法解析率为26.6%，语义验证通过率仅为8.6%。本文提出TLA-Prover，一个200亿参数的TLA+规范生成模型。训练结合监督微调（SFT）与基于修复的组相对策略优化（GRPO），使模型学会修正自身被拒绝的规范。采用直接偏好优化（DPO）作为消融对比。使用TLC提供奖励信号，无需训练奖励模型。输出按四层评级：青铜（可解析）、白银（无警告）、黄金（通过TLC）、钻石（需微调正确性属性仍通过才算达标）。若调整后仍通过，说明属性恒真，不具意义，判定为钻石失败。实验显示，TLA-Prover在30题独立测试集上，黄金与钻石通过率均为9/30（即30%），约为未调优基线8.6%的3.5倍。DPO变体钻石通过率为20%。所有检查点下黄金与钻石结果一致，有效避免了恒真属性的漏洞。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。