AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

技术摘要：基于重新设计的语言抽象语法树（AST）的定理证明智能体

问题陈述
交互式定理证明（ITP）对于程序验证和形式化数学至关重要，但面临着高昂的人力成本和有限的可扩展性问题。虽然大语言模型（LLM）智能体有望实现这一过程的自动化，但目前的实现方式面临着极高的 API 成本和 Token 消耗。本文识别了导致这种低效的两个根本原因：

1. 对具体语法的依赖： 当前的智能体在序列化的源代码文本上运行。它们将证明输出为纯文本，并通过基于行号的单独查询来恢复证明状态。这导致每当编辑导致行号偏移时，都需要重复进行位置定位，从而导致过多的工具调用和 Token 使用。
2. 与新语言的不兼容性： 一种名为 Minilang 的新型证明语言旨在通过将细粒度推理委托给经典的自动定理证明器（ATP），并将语法与自然语言推理对齐，从而提高 LLM 的效率。然而，由于 Minilang 是全新的（其语料库发布于 2025 年底），通用 LLM 缺乏掌握其具体语法的训练数据，且由于数据稀缺和成本问题，进行微调通常是不切实际的。

方法论：基于 AST 的智能体 (AoA)
作者提出了 基于 AST 的智能体 (Agent over AST, AoA)，这是一种将交互层从源代码文本提升到 Minilang 抽象语法树 (AST) 的证明智能体。该方法由三个核心组件组成：

1. 以 AST 为中心的表示法：

   • 智能体不再生成源代码，而是将证明输出为 Minilang AST 的 JSON 表示形式。这种格式原生适用于支持工具调用的 LLM，并消除了对特定具体语法的依赖。
   • AST 使用 JSON Schema 进行形式化，使 LLM 能够专注于证明的语义构建，而非语法拼写。

2. 树编辑证明模型：

   • 智能体通过一个 树编辑模型 与证明器进行交互，该模型将证明操作和证明状态融合为一个单一的、不断演进的证明树。
   • 状态融合： 不同于传统的智能体需要单独检索状态，证明树中的每个节点都携带其子目标的（subgoal）状态。当应用一个操作时，证明器会计算结果状态（目标、假设、错误）并将其直接附加到该操作节点上。
   • 编辑操作： 智能体使用工具（READ、EDIT、QUERY、SUBAGENT）来操作树。EDIT 工具支持填充槽位、插入节点、修改操作或删除子树。
   • 增量同步： 在进行编辑后，系统返回一个压缩视图的树，仅显示发生变化的统计信息和消息，而不是整个树。这消除了 LLM 重新阅读整个上下文或通过脆弱的行号进行导航的需求。

3. 无需模型修改的系统设计：

   • AoA 使通用 LLM 能够在无需微调的情况下构建 Minilang 证明。通过抽象掉具体语法并通过 JSON 暴露语义结构，该系统允许此前从未接触过 Minilang 语料库的模型也能高效执行任务。

核心贡献

• 树编辑证明模型： 一种新颖的交互模型，用证明树编辑取代了源代码文件补丁，消除了对单独的基于行号的证明状态查询的需求。
• AoA 智能体： 一个具体的实现，证明了通过系统设计，通用 LLM 可以构建新语言（Minilang）的证明，而无需大规模语料库的接触或模型微调。
• 实证评估： 在 miniF2F（数学）和 NTP4VC-Pearl（程序验证）基准测试上针对 Amazon 的 Isabelle Agent 进行了全面的评估。

结果
在 miniF2F 和 NTP4VC-Pearl 的共同成功集上进行评估，AoA 展示了相对于 Amazon Isabelle Agent 的显著效率提升：

• 成本降低： 实现 2.3–4.7 倍更低的 API 成本（针对输入缓存复用进行归一化处理）。
• Token 效率： 使用了 2.9–6.9 倍更少的总 Token 以及 3.9–8.9 倍更少的工具调用。
• 速度： 完成案例的速度快了 1.4–2.0 倍。
• 性能：
  • miniF2F： 实现了 99.6% 的通过率（匹配最先进的 SeedProver）。
  • NTP4VC-Pearl： 实现了 89.2% 的通过率，创下了验证条件证明领域的新纪录。
• 泛化能力： 在对 Claude Opus 4.5（发布于 Minilang 公开语料库之前）进行测试时，AoA 保持了 98.6% 的通过率，证实了该方法在无需先前大规模语料库接触的情况下依然有效。

意义与主张
本文声称，当前证明智能体的高成本源于在序列化的具体语法上进行操作。通过重新设计证明语言（Minilang）并在树编辑模型中暴露其 AST，可以实现：

1. 大幅降低证明智能体的 API 成本和 Token 消耗。
2. 使通用 LLM 能够在无需昂贵的微调或大规模训练语料库的情况下，操作新的形式化语言。

作者强调，这种方法抽象了证明语言的语义信息，并将其重新表达为 LLM 原生的格式（JSON/AST），从而允许智能体专注于证明构建逻辑而非语法导航。本文结论指出，该方法论为将 LLM 集成到形式化验证中提供了一条可扩展的路径，并建议类似的基于 AST 的方法也可以使针对新设计的编程语言的编码智能体受益。