AoA：在重设计语言抽象语法树上运行的定理证明智能体

论文提出 AoA，将交互式定理证明智能体从具体源代码提升到 Minilang 的抽象语法树（AST）上。模型以 JSON 输出证明树并通过树编辑操作驱动证明器，使操作与子目标状态绑定。摘要称，在 miniF2F 与 NTP4VC-Pearl 公共成功集上，API 成本降低 2.3–4.7 倍，Token 减少 2.9–6.9 倍，工具调用减少 3.9–8.9 倍，速度提升 1.4–2.0 倍。