arXiv cs.AI· Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, Conrad Watt·· 3 小时前AI 评分38
基于抽象语法树的定理证明智能体 AoA 发布于 ICSE 2027
Theorem-Proving Agent over Abstract Syntax Tree
AI 导读
论文提出 Agent over AST（AoA），让定理证明智能体直接在抽象语法树上操作：模型以 JSON 形式给出 Minilang AST 证明，通过树编辑模型将证明操作与状态融合为一棵证明树。
正文 · 原文
Abstract:Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to a shared root: current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries, so every edit shifts later lines and forces repeated relocation of errors and states. This same dependence on concrete syntax also blocks adoption of Minilang, a recent proof language that reaches SOTA on LLM-based proving but is too new for LLMs' training corpora. We address both problems by lifting the agent off source text and onto the abstract syntax tree (AST): the model supplies proofs as JSON representations of Minilang's AST -- native to tool-calling LLMs -- and drives the prover through a tree-edit model that fuses proof operations and states into one proof tree, so each operation carries its own subgoal's state, readable directly off the tree. We realize this design in \emph{Agent over AST} (AoA). Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3--4.7x (normalized input-cache accounting), uses 2.9--6.9x fewer tokens and 3.9--8.9x fewer tool calls, and finishes 1.4--2.0x faster -- while also solving far more problems on the harder verification benchmark.
| Comments: | 13 pages. Accepted at International Conference on Software Engineering (ICSE) 2027 |
| Subjects: | Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Programming Languages (cs.PL) |
| Cite as: | arXiv:2607.16372 [cs.SE] |
| (or arXiv:2607.16372v2 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2607.16372 arXiv-issued DOI via DataCite |
Submission history
From: Joshua Jun Leang Ong [view email]
[v1]
Fri, 17 Jul 2026 14:43:43 UTC (44 KB)
[v2]
Thu, 12 Nov 2026 08:49:16 UTC (55 KB)
来源：arXiv cs.AI · arxiv.org