AoA：重新设计语言抽象语法树上的定理证明代理

交互式定理证明 (ITP) 是程序验证和形式化数学的基础，但其手动工作限制了可扩展性。基于 LLM 的证明代理有望减轻这项工作，但其大量的词元消耗和 API 成本仍然是主要障碍。我们将这种成本追溯到一个共享的根源：当前代理使用序列化的具体语法进行操作，将证明作为源文本发出，并通过单独的、基于行号的查询恢复证明状态，因此每次编辑都会移动后面的行并强制重复重新定位错误和状态。这种对具体语法的同样依赖也阻碍了 Minilang 的采用，Minilang 是一种最新的证明语言，在基于 LLM 的证明上达到了 SOTA，但对于 LLM 的训练语料库来说太新了。我们通过将代理从源文本提升到抽象语法树 (AST) 来解决这两个问题：模型提供 Minilang AST 的 JSON 表示形式的证明（原生于工具调用 LLM），并通过树编辑模型驱动证明者，该模型将证明操作和状态融合到一个证明树中，因此每个操作都带有自己的子目标状态，可以直接从树中读取。我们在 \emph{Agent over AST} (AoA) 中实现了这一设计。与 Amazon 在 miniF2F 和 NTP4VC-Pearl 常见成功集上的 Isabelle Agent 相比，AoA 将 API 成本降低了 2.3--4.7 倍（标准化输入缓存核算），使用的词元减少了 2.9--6.9 倍，工具调用减少了 3.9--8.9 倍，完成速度提高了 1.4--2.0 倍，同时还解决了更严格的验证基准上的更多问题。