Towards Language Model Guided TLA+ Proof Automation

这是一篇关于利用大语言模型（LLM）辅助 TLA+ 形式化证明自动化的技术论文总结。

论文标题

Towards Language Model Guided TLA+ Proof Automation (迈向语言模型引导的 TLA+ 证明自动化)

1. 研究背景与问题 (Problem)

• 背景：TLA+ 是一种用于规范化和验证复杂系统（特别是分布式系统）的强大形式化语言，被 Amazon、Intel 和 Microsoft 等公司广泛采用。虽然模型检测（Model Checking）在工业界很流行，但定理证明（Theorem Proving）对于验证无界/无限状态系统至关重要。
• 核心挑战：
  1. 高门槛：构建 TLA+ 形式化证明需要深厚的专业知识和大量精力，成为验证过程的瓶颈。
  2. 结构差异：现有的基于 LLM 的定理证明自动化（如针对 Lean 或 Coq）主要基于策略（Tactic）驱动的模式（即通过一系列命令逐步转换证明状态）。然而，TLA+ 采用分层（Hierarchical）证明结构，即通过引入中间子断言（Sub-claims）来构建证明树，而非线性的策略序列。
  3. 数据匮乏：与 Lean 或 Coq 相比，TLA+ 缺乏大规模的形式化证明数据集，难以直接训练或微调模型。
  4. 语法错误：直接让 LLM 生成完整的 TLA+ 证明会导致大量的语法错误，因为 TLA+ 的语法规范严格，且 LLM 容易混淆不同证明助手（如 Isabelle）的语法。

2. 方法论 (Methodology)

作者提出了一种名为 LMGPA (Language Model Guided Proof Automation) 的系统，其核心思想是利用 LLM 进行逻辑分解，利用符号证明器进行验证。

核心架构与流程

1. 递归分解策略 (Recursive Decomposition)：

   • 系统不要求 LLM 生成完整的证明，而是引导 LLM 将复杂的证明目标（Goal）分解为更简单的子断言（Sub-claims）。
   • 这是一个递归过程：对于每个子断言，系统尝试直接证明；如果失败，则继续递归分解，直到所有叶子节点都能被后端证明器（如 Z3, Zenon, Isabelle）直接验证。

2. 归一化断言结构 (Normalized Claim Structure)：

   • 为了解决语法错误问题，系统强制 LLM 生成归一化格式的子断言。
   • 格式约束：每个子断言必须包含明确的假设列表（Assumptions）和一个目标（Hypothesis/Goal）。
   • 语法限制：提示词中嵌入了严格的语法规则（如仅使用 ASCII 字符、特定的逻辑符号如 \A, \E, /\ 等，禁止使用 Unicode 或非法操作符）。
   • 转换：系统负责将 LLM 生成的归一化文本转换为合法的 TLA+ ASSUME-PROVE 语句，从而消除了大部分语法错误。

3. 混合验证机制：

   • 自动证明生成 (Symbolic Auto Proof)：对于简单的断言，系统使用启发式方法自动生成 OBVIOUS 或 BY DEF 指令，直接交由 TLAPS 验证，无需调用 LLM。
   • 验证反馈循环：如果分解后的子断言无法被验证，TLAPS 的错误反馈会被送回 LLM，引导其修正分解策略。

4. 算法逻辑：

   • 输入：证明义务（上下文 + 目标）。
   • 步骤 1：尝试直接生成自动证明（Auto Proof）。
   • 步骤 2：若失败，调用 LLM 分解目标为子断言。
   • 步骤 3：验证子断言是否逻辑上支持父目标。
   • 步骤 4：递归处理每个子断言。
   • 输出：构建完整的分层证明树。

3. 关键贡献 (Key Contributions)

1. 针对 TLA+ 的专用架构：首次提出适应 TLA+ 分层证明结构的 LLM 引导方法，而非简单套用针对策略式证明器（如 Lean）的方法。
2. 归一化分解策略：通过限制 LLM 仅生成“归一化的断言分解”而非完整证明，显著降低了语法错误率，解决了 LLM 在形式化语言中常见的“幻觉”和语法混淆问题。
3. 基准测试套件 (Benchmark Suite)：构建了一个包含 119 个定理 的基准测试集，包括：
   • 93 个来自 miniF2F 和 ProofNet 的数学定理（手动翻译为 TLA+）。
   • 26 个来自分布式协议归纳不变式（Inductive Invariants）的证明。
4. 实证结果：在多个 SOTA LLM（如 Claude 3.7, GPT-5, o3-mini 等）上进行了评估，证明了该方法的有效性。

4. 实验结果 (Results)

• 成功率提升：LMGPA 在所有基准测试和所有测试的 LLM 上，其证明成功率均显著优于基线方法（包括纯符号方法 TLAPS OBVIOUS、符号自动证明生成 SAPG 以及直接 LLM 生成证明 DLPG）。
  • 例如，在分布式协议基准中，LMGPA (使用 DeepSeek-V3.2) 的成功率达到了 50.0%，而直接 LLM 生成仅为 0.0%。
  • 在数学基准中，LMGPA 的成功率普遍在 50%-60% 之间，远超直接生成方法。
• 语法正确性：LMGPA 生成的分解内容具有极高的语法有效性（约 65%-86%），而直接生成完整证明的方法语法错误率极高（通常低于 20%）。
• 效率与成本：虽然 LLM 调用增加了时间成本，但通过减少无效尝试和利用符号证明器处理简单步骤，整体效率优于盲目重试。
• 局限性分析：
  • 部分失败源于 LLM 生成了逻辑上有效但后端证明器无法在超时时间内验证的分解（如需要复杂数学变换）。
  • 生成的证明有时不够简洁（包含冗余的中间步骤），不如人类专家编写的证明精炼。

5. 意义与影响 (Significance)

• 降低形式化验证门槛：通过自动化处理繁琐的中间步骤和断言发现，大幅降低了使用 TLA+ 进行定理证明的专家门槛，使形式化验证在工业界更具可扩展性。
• 方法论创新：展示了“LLM 负责高层逻辑推理与分解，符号工具负责底层验证”的混合范式在处理非策略式证明系统时的优越性。
• 未来方向：论文指出了未来工作的方向，包括针对 TLA+ 证明语料库进行微调（Fine-tuning）、改进提示工程以生成更简洁的证明，以及增强 LLM 对后端证明器能力的理解，以避免生成无法被验证的分解。

总结：该论文成功地将大语言模型的推理能力与 TLA+ 的分层证明结构相结合，通过“归一化分解”策略有效克服了语法错误和结构不匹配的挑战，显著提升了 TLA+ 定理证明的自动化水平，为复杂分布式系统的形式化验证提供了新的解决方案。