New AoA theorem prover cuts API costs 4.7x using AST over source code

LLM-based proof agents promise to automate interactive theorem proving (ITP) for program verification and formalized mathematics, but their heavy token consumption and API costs remain a major bottleneck. Current agents operate on serialized concrete syntax, emitting proofs as source text and recovering proof states through separate, line-number-based queries. Every edit shifts later lines, forcing repeated relocation of errors and states. Additionally, this dependence on concrete syntax blocks adoption of Minilang, a recent proof language that achieves SOTA on LLM-based proving but is too new for LLMs' training corpora.

AoA (Agent over AST) lifts the agent off source text and onto the abstract syntax tree. 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. Each operation carries its own subgoal's state, readable directly off the tree. Against Amazon's Isabelle Agent on miniF2F and NTP4VC-Pearl common success sets, AoA cuts API cost by 2.3–4.7x, uses 2.9–6.9x fewer tokens and 3.9–8.9x fewer tool calls, and finishes 1.4–2.0x faster, while solving far more problems on the harder verification benchmark.