arXiv cs.AI· Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, Conrad Watt·· 1 天前AI 评分34
Agent over AST：基于抽象语法树的定理证明智能体
Theorem-Proving Agent over Abstract Syntax Tree
AI 导读
研究提出定理证明智能体 AoA（Agent over AST），让模型以 JSON 形式输出 Minilang 的抽象语法树而非源码文本，并通过树编辑模型将证明操作与状态融合为一棵证明树。
正文 · AI 翻译
摘要：交互式定理证明（ITP）是程序验证与形式化数学的基础，但其人工投入限制了可扩展性。基于 LLM 的证明智能体有望减轻这一负担，但其巨大的 token 消耗与 API 成本仍是主要障碍。我们将这一成本追溯到一个共同根源：当前智能体基于序列化的具体语法运行，将证明以源文本形式输出，并通过独立的、基于行号的查询来恢复证明状态，因此每次编辑都会移动后续行，迫使错误与状态被反复重新定位。这种对具体语法的依赖同样阻碍了 Minilang 的采用——Minilang 是一种近期出现的证明语言，在基于 LLM 的证明上达到 SOTA，但对 LLM 的训练语料而言过于新颖。我们通过将智能体从源文本提升到抽象语法树（AST）来解决这两个问题：模型以 Minilang AST 的 JSON 表示形式提供证明——这对工具调用的 LLM 而言是原生的——并通过树编辑模型驱动证明器，该模型将证明操作与状态融合为一棵证明树，因此每个操作都携带其自身子目标的状态，可直接从树上读取。我们在 \emph{Agent over AST}（AoA）中实现了这一设计。在 miniF2F 和 NTP4VC-Pearl 公共成功集上，与 Amazon 的 Isabelle Agent 相比，AoA 将 API 成本降低 2.3–4.7 倍（归一化输入缓存核算），使用的 token 减少 2.9–6.9 倍，工具调用减少 3.9–8.9 倍，完成速度快 1.4–2.0 倍——同时在更难的验证基准上解决了远更多的问题。
| 评论： | 13 页。已被 International Conference on Software Engineering (ICSE) 2027 接收 |
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；机器学习（cs.LG）；编程语言（cs.PL） |
| 引用为： | arXiv:2607.16372 [cs.SE] |
| （或 arXiv:2607.16372v2 [cs.SE] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2607.16372 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Joshua Jun Leang Ong [查看邮箱]
[v1]
2026 年 7 月 17 日星期五 14:43:43 UTC（44 KB）
[v2]
2026 年 11 月 12 日星期四 08:49:16 UTC（55 KB）
来源：arXiv cs.AI · arxiv.org