arXiv · cs.AI 人工智能· Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, Conrad Watt·2026-11-13 13:00· 5 小时前AI 评分68

AoA：在抽象语法树上运行的定理证明智能体，API 成本降低 2.3–4.7 倍

Theorem-Proving Agent over Abstract Syntax Tree

AI 导读

作者提出 Agent over AST（AoA），让模型以 Minilang AST 的 JSON 表示输出证明，并通过树编辑模型把证明操作与状态融合成一棵证明树，从而摆脱对序列化具体语法和行号查询的依赖。