TLA-Prover：通过偏好优化的低秩适应进行可验证的 TLA+ 规范综合

TLA+ 是一种用于验证分布式系统和安全关键协议的正式规范语言。 大语言模型 (LLM) 经常生成由于语义原因无法通过 TLC 模型检查器的 TLA+ 规范。在 25 个 LLM 中，最佳公共基线是 26.6% 句法解析和 8.6% 语义模型检查。我们推出了 TLA-Prover，这是一个用于 TLA+ 规范综合的 200 亿参数模型。训练将经过验证的示例上的监督 微调 (SFT) 与基于修复的组相对策略优化 (GRPO) 相结合。在 GRPO 阶段，模型学习修复自己被拒绝的规范。我们还从相同的 SFT 检查点训练直接偏好优化 (DPO) 变体作为消融。 TLC 直接提供奖励信号，无需学习奖励模型。每个输出有四个等级：青铜级（解析）、白银级（无警告）、黄金级（通过 TLC）和钻石级。为了达到钻石级，模型的正确性属性会自动进行小幅改变； TLC 随后必须检测违规行为。如果 TLC 仍然通过，则该属性始终为真并且没有任何贡献；输出失败 Diamond。 TLA-Prover 在 30 个问题基准测试中，黄金级和钻石级的得分均达到 9/30（即 pass@1 = 30%）。这大约是 8.6% 未调整基线的 3.5 倍。 Diamond 的 DPO 变体达到 20%。黄金和钻石在每个检查站都重合；这可以防止平凡属性故障模式。