发表机构
Nanyang Technological University Singapore; Imperial College London London, UK; University of Edinburgh Edinburgh, UK（南洋理工大学新加坡分校; 伦敦帝国理工学院伦敦分校; 爱丁堡大学爱丁堡分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究针对交互式定理证明中人工操作限制可扩展性及基于LLM的证明智能体成本高的问题，提出将智能体从源文本提升到抽象语法树的方法，实现了AoA，在多个方面有显著提升且解决更多难题。
AI 中文摘要
交互式定理证明（ITP）是程序验证和形式化数学的基础，但人工操作限制了其可扩展性。基于大语言模型（LLM）的证明智能体有望减轻这一负担，但其高昂的令牌消耗和API成本仍是主要障碍。我们将此成本追溯到一个共同根源：当前智能体在序列化的具体语法上运行，将证明作为源文本发出，并通过单独的基于行号的查询恢复证明状态，因此每次编辑都会移动后续行，并迫使错误和状态重复重新定位。对具体语法的这种依赖也阻碍了Minilang的采用，Minilang是一种最近的证明语言，在基于LLM的证明方面达到了当前最优水平，但对于LLMs的训练语料库来说太新了。我们通过将智能体从源文本提升到抽象语法树（AST）来解决这两个问题：模型以Minilang的AST的JSON表示形式提供证明，这是工具调用LLMs原生的，并通过树编辑模型驱动证明器，该模型将证明操作和状态融合到一个证明树中，因此每个操作都携带其自己子目标的状态，可直接从树中读取。我们在“AST上的智能体”（AoA）中实现了这一设计。与亚马逊的Isabelle智能体在miniF2F和NTP4VC-Pearl常见成功集上相比，AoA将API成本降低了2.3-4.7倍（归一化输入缓存计算），使用的令牌减少了2.9-6.9倍，工具调用减少了3.9-8.9倍，并完成速度快1.4-2.0倍，同时在更难的验证基准上解决了更多问题。
英文摘要
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.
Comments13 pages
