AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language
Proposes AoA, a proof agent over AST, reducing API costs 2.3-4.7x and improving speed and success rates significantly.
Key Findings
Methodology
This work shifts proof interactions from source code to abstract syntax trees (AST), defining Minilang’s AST via JSON Schema for native LLM manipulation. The proof process is modeled as a unified tree where proof operations and states are intertwined, enabling direct editing of proof goals and subgoals. The system employs tools like READ and EDIT to synchronize proof states efficiently, avoiding line-based error localization. Extensive experiments on miniF2F and NTP4VC-Pearl benchmarks demonstrate that AoA reduces API costs by 2.3-4.7 times, token usage by 2.9-6.9 times, tool calls by 3.9-8.9 times, and accelerates proof completion by 1.4-2.0 times, outperforming traditional source-based agents.
Key Results
- On benchmark datasets, AoA achieves API cost savings of 2.3-4.7x, token reduction of 2.9-6.9x, and speedup of 1.4-2.0x compared to Amazon’s Isabelle Agent. Success rates reach 89.2% on NTP4VC-Pearl and 99.6% on miniF2F, surpassing existing methods.
- The proof tree model effectively captures proof states and operations, enabling the model to construct proofs in new languages like Minilang without fine-tuning, demonstrating strong generalization.
- Cost and efficiency improvements are consistent across various proof complexities, indicating robustness and scalability of the approach.
Significance
This research addresses the critical bottleneck of high API costs and inefficiencies in automated theorem proving with LLMs. By abstracting proof interactions into a tree structure over ASTs, it enables large models to perform formal reasoning in new languages without extensive training data. The approach significantly reduces operational costs, making large-scale verification feasible for industrial applications. It also opens avenues for integrating formal proof systems with general-purpose LLMs, fostering broader adoption of formal methods in software engineering and mathematics.
Technical Contribution
The core innovation lies in the tree-edit proof model that interleaves proof states and operations within a single structure, eliminating the need for brittle line-based navigation. Defining proof language ASTs via JSON Schema allows models to manipulate proofs semantically rather than syntactically. The implementation of AoA demonstrates that such a system can operate efficiently without fine-tuning, achieving state-of-the-art results while drastically reducing API costs. This bridges the gap between formal proof systems and large language models, offering a scalable, generalizable framework.
Novelty
This is the first work to replace source code-based proof interactions with a tree-edit model over ASTs, enabling proof construction in languages with limited training data. The use of JSON Schema for defining proof language ASTs allows models to operate semantically, overcoming the dependency on concrete syntax. This paradigm shift significantly enhances the generalization and efficiency of LLM-based proof agents, representing a major step forward in automated formal reasoning.
Limitations
- Handling highly complex, multi-branch proofs may lead to large, unwieldy trees that impact performance. Optimization of tree operations is needed.
- The system's effectiveness in resource-constrained environments remains untested; computational overhead of tree manipulations could be a concern.
- Support for additional proof languages and diverse proof styles requires further validation and extension.
Future Work
Future efforts include integrating multimodal interfaces for more intuitive proof editing, developing smarter tree manipulation strategies, and applying transfer learning to adapt the system to other formal languages. Extending the framework to handle more complex proofs and exploring industrial-scale deployments will further demonstrate its practical value.
AI Executive Summary
Interactive theorem proving (ITP) has long been a cornerstone of formal verification and mathematical formalization, offering expressive power beyond automated theorem provers. However, its reliance on manual effort and source code manipulation has hindered large-scale adoption. Recent advances leverage large language models (LLMs) to automate proof construction, but these systems face significant challenges: high API costs, inefficiencies in error localization, and limited generalization to new proof languages.
This paper introduces AoA, a novel proof agent built upon an abstract syntax tree (AST) framework. By transforming proof interactions from source code to a structured tree model, AoA enables LLMs to manipulate proofs directly at the semantic level. The core idea involves defining Minilang’s proof language as a JSON Schema-based AST, allowing models to generate and edit proofs via JSON representations. The proof process is modeled as a tree where nodes represent proof goals, operations, and subgoals, with proof states embedded within nodes. This design eliminates the need for brittle line-based error localization and reduces API calls by enabling direct tree editing and state synchronization.
Extensive experiments on benchmark datasets demonstrate that AoA reduces API costs by over 2.3 times, cuts token consumption by nearly 7 times, and accelerates proof completion by up to 2 times compared to traditional source-based agents. Notably, AoA achieves a success rate of 89.2% on complex verification tasks, surpassing existing state-of-the-art methods. These results highlight the effectiveness of the tree-edit model in enabling large models to construct proofs in languages with limited training data, such as Minilang.
The broader impact of this work lies in making formal verification more scalable and accessible. By reducing operational costs and improving generalization, AoA paves the way for industrial adoption of automated theorem proving. Future directions include enhancing the system’s ability to handle complex proofs, integrating multimodal interfaces, and extending support to diverse proof languages. Overall, this research marks a significant step toward fully automated, cost-effective formal reasoning systems driven by large language models.
Deep Dive
Abstract
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.