核心发现
方法论
本文提出将证明代理从源代码文本转向抽象语法树（AST），利用JSON Schema定义Minilang的AST结构，使LLMs以JSON格式表达证明。通过树编辑模型，将证明操作与状态融合为单一证明树，避免反复定位错误和状态迁移。实现的AoA系统在多项验证任务中显著降低API调用成本（2.3-4.7倍），减少令牌消耗（2.9-6.9倍），并提升速度（1.4-2.0倍），同时在复杂验证场景中表现优异。
关键结果
- 在miniF2F和NTP4VC-Pearl基准测试中，AoA的API成本较Amazon Isabelle Agent降低2.3-4.7倍，令牌消耗减少2.9-6.9倍，工具调用次数减少3.9-8.9倍，验证速度提升1.4-2.0倍。
- 在验证难度较高的任务中，AoA达成89.2%的成功率，超越现有SOTA方法，且在miniF2F中达成99.6%的成功率。
- 通过抽象语法树模型，有效解决了新型证明语言Minilang的训练数据缺乏问题，增强了模型的泛化能力。
研究意义
该研究突破了传统基于源文本的证明代理在成本和效率上的瓶颈，为大规模程序验证和形式化数学的自动化提供了新路径。通过抽象语法树的设计，增强了模型对新语言的适应性，降低了训练和微调的门槛，推动了LLM在形式化推理中的应用落地。这不仅提升了验证流程的可扩展性，也为未来自动化证明系统的普及奠定基础。
技术贡献
本文提出的树编辑模型创新性地融合了证明操作与状态信息，避免了传统文本操作中的反复定位问题。利用JSON Schema定义AST结构，使LLMs可以直接操作抽象语法树，减少对具体语法的依赖。实现的AoA系统在多项验证任务中表现出显著的成本节约和性能提升，展示了在无需微调的情况下，利用系统设计实现跨语言推理的潜力。这为大模型在形式化推理中的应用提供了新思路。
新颖性
本研究首次将证明代理从源文本操作转向基于抽象语法树的树编辑模型，解决了新语言训练数据匮乏和操作效率低下的问题。通过定义通用的JSON Schema，模型无需微调即可在未见过的证明语言中构建证明，突破了传统依赖大规模语料的限制。这一设计为大模型在形式化推理中的泛化能力提供了新范式，具有重要创新意义。
局限性
- 当前模型对复杂证明策略的处理仍有限，特别是在多步骤、多分支的证明中，树结构可能变得庞大复杂，影响效率。
- 系统在极端资源受限环境下的表现尚未充分验证，未来需优化树操作的计算成本。
- 对某些特定证明语言的适应性仍需验证，未来需扩展到更多语言和验证场景。
未来方向
未来将探索多模态交互方式，结合视觉和自然语言增强证明操作的直观性。同时，计划引入更智能的树编辑策略，提高复杂证明的处理能力。还将结合微调与迁移学习，进一步提升模型在不同证明语言中的表现，推动自动化验证的普及与工业应用。
AI 总览摘要
Interactive theorem proving (ITP)在程序验证和数学形式化中扮演核心角色，但其高度依赖人工操作限制了规模扩展。近年来，大型语言模型（LLMs）被引入作为自动证明的工具，显著提升了自动化水平，但同时带来了高昂的API调用成本。传统方法依赖于源代码文本的序列化操作，导致每次编辑都需反复定位错误位置，造成效率低下和成本高企。本文提出的AoA（Agent over AST）创新性地将证明操作从源文本转向抽象语法树（AST），利用JSON Schema定义证明语言的AST结构，使LLMs可以直接操作抽象语法树中的节点。通过树编辑模型，将证明操作与状态信息融合在一棵证明树中，每次操作都携带子目标的状态信息，避免了繁琐的文本定位和状态恢复过程。实验结果显示，AoA在miniF2F和NTP4VC-Pearl基准测试中，API成本降低2.3-4.7倍，令牌消耗减少2.9-6.9倍，验证速度提升1.4-2.0倍，且成功率显著优于现有方法。这一设计不仅大幅降低了成本，也增强了模型在新型证明语言（如Minilang）上的泛化能力，为大模型在形式化推理中的应用开辟了新路径。未来，AoA有望通过多模态交互和智能树编辑策略，进一步提升复杂证明的处理能力，推动自动化验证的工业化落地。
深度分析
研究背景
形式化验证和定理证明在软件安全、硬件设计及数学研究中具有重要应用。传统的自动定理证明（ATP）依赖搜索算法，效率有限，难以应对复杂场景。近年来，交互式定理证明（ITP）因其表达能力强，成为主流工具，如Isabelle、Coq等。随着大模型的发展，LLMs被尝试引入自动化证明中，显著提升了推理效率，但成本高昂、操作繁琐，限制了其规模应用。现有系统多依赖源代码文本，导致频繁的错误定位和状态恢复，效率低下。新兴的证明语言Minilang提出高层次结构化证明，旨在改善模型理解能力，但缺乏大规模训练数据，限制了其推广。整体来看，自动化证明的瓶颈在于操作效率和数据依赖，亟需创新的系统设计以突破瓶颈。
核心问题
当前的证明代理主要依赖源代码文本操作，导致每次编辑都需重新定位错误和状态，成本高且不易扩展。新型证明语言Minilang虽有潜力，但缺乏足够的训练数据，模型难以直接理解和操作。如何在不依赖微调的情况下，使大模型高效构建新语言证明，成为核心难题。此外，传统方法在处理复杂、多步骤证明时，树结构庞大，操作繁琐，影响性能。解决这些问题，既需要降低成本，也要提升模型的泛化能力和操作效率。
核心创新
本文提出基于抽象语法树的证明代理（AoA），实现以下创新：1）将证明操作从源文本转向树结构，利用JSON Schema定义AST，减少对具体语法的依赖；2）设计树编辑模型，将证明状态与操作融合在一棵树中，避免繁琐的状态恢复和错误定位；3）实现无需微调的系统架构，使大模型能在未见过的证明语言中构建证明。此设计突破了传统依赖大规模语料和微调的限制，显著提升了操作效率和泛化能力，为自动化推理提供新思路。
方法详解
- �� 定义Minilang的抽象语法树（AST）结构，采用JSON Schema描述，确保模型能以JSON格式操作。• 构建树编辑模型，将证明目标、操作和状态融合在一棵证明树中，每个节点代表一个证明操作或目标。• 设计树操作指令（填充、插入、修改、删除），通过节点ID定位树中的位置，实现对证明树的动态编辑。• 利用LLMs生成证明操作的JSON表达，模型在每次编辑后，自动更新证明树的状态，避免反复定位错误。• 结合READ和EDIT工具，实时同步证明状态，减少API调用次数。• 实验中，将AoA应用于miniF2F和NTP4VC-Pearl验证任务，评估成本、速度和成功率。• 通过对比传统源文本方法，验证AoA在效率和效果上的优势。
实验设计
采用miniF2F和NTP4VC-Pearl两个公开验证基准，比较AoA与Amazon Isabelle Agent的性能。指标包括API调用次数、令牌消耗、验证速度和成功率。设置不同验证难度场景，分析系统在高复杂度任务中的表现。通过消耗分析，验证成本节约的有效性。还进行不同树结构规模的消融实验，评估树编辑模型的效率。最后，统计成功率和平均验证时间，验证系统的实用性和鲁棒性。
结果分析
AoA在所有基准测试中均显著优于传统方法，API成本降低2.3-4.7倍，令牌消耗减少2.9-6.9倍，工具调用次数减少3.9-8.9倍，验证速度提升1.4-2.0倍。成功率方面，AoA在复杂验证任务中达89.2%，在miniF2F中达99.6%，均优于对比系统。树编辑模型的引入有效减少了状态恢复和错误定位的开销，验证了其在实际场景中的应用潜力。整体结果表明，系统设计的创新极大提升了自动证明的效率和可扩展性。
应用场景
该系统适用于大规模程序验证、硬件设计验证和数学定理证明等场景。尤其在工业界，能显著降低验证成本，提升验证效率。未来，结合自动化推理和多模态交互，有望实现全自动化的验证流程，推动软件安全和硬件可靠性保障的产业升级。
局限与展望
目前系统在处理极复杂、多分支的证明中，树结构可能变得庞大，影响性能。模型对某些特定证明策略的适应性有限，需进一步优化树操作算法。此外，系统在极端资源受限环境下的表现尚未充分验证，未来需提升其计算效率和鲁棒性。还需扩展支持更多证明语言和场景，以实现更广泛的应用。
通俗解读 非专业人士也能看懂
想象你在做一道复杂的菜谱，每次你需要添加或调整某个步骤，传统方法就像是用一张纸写着菜谱，然后每次修改都要找出对应的那一行，反复查找很麻烦。而这篇研究提出的方法，就像把菜谱变成一棵树，每个步骤都是树上的一个节点，你可以直接在树上添加、修改或删除步骤，不用担心位置变乱。这样做不仅快，还能让厨师（模型）更聪明地理解整个菜谱，做出更好、更快的菜。这种方法让复杂的菜谱变得像搭积木一样简单，节省时间和精力，也更容易改良和创新。
简单解释 像给14岁少年讲一样
你知道写作业时，有时候要改答案，光用纸写很麻烦，因为每次改都得找出原来写错的地方，然后重新写一遍。这个研究就像把答案写在一棵树上，每个答案都是树上的一个点，你可以直接在树上改，不用一遍遍找错的地方。这样，改答案就变得很快，也不会搞错。科学家们用这个方法，让电脑像人一样聪明，能自己在树上改写证明，省了很多时间，也能处理更复杂的问题。未来，这种树结构还能帮我们做更聪明的学习和工作，让电脑帮我们解决更难的任务！
原文摘要
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.