AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Technical Summary: Theorem-Proving Agent over Abstract Syntax Tree of Redesigned Language

Problem Statement
Interactive Theorem Proving (ITP) is essential for program verification and formalized mathematics but suffers from high manual labor costs and limited scalability. While Large Language Model (LLM) agents promise to automate this process, current implementations face prohibitive API costs and token consumption. The paper identifies two root causes for this inefficiency:

1. Reliance on Concrete Syntax: Current agents operate on serialized source text. They emit proofs as plain text and recover proof states through separate, line-number-based queries. This forces repeated relocation of errors and states whenever edits shift line numbers, leading to excessive tool calls and token usage.
2. Incompatibility with New Languages: A recent proof language, Minilang, is designed to improve LLM efficiency by delegating fine-grained reasoning to classical Automated Theorem Provers (ATPs) and aligning syntax with natural-language reasoning. However, because Minilang is new (corpus released late 2025), general-purpose LLMs lack the training data to master its concrete syntax, and fine-tuning is often impractical due to data scarcity and cost.

Methodology: Agent over AST (AoA)
The authors propose Agent over AST (AoA), a proof agent that lifts the interaction layer from source text to the Abstract Syntax Tree (AST) of Minilang. The methodology consists of three core components:

1. AST-Centric Representation:

   • Instead of generating source code, the LLM outputs proofs as JSON representations of Minilang's AST. This format is native to tool-calling LLMs and removes dependence on specific concrete syntax.
   • The AST is formalized using JSON Schema, allowing LLMs to focus on the semantic construction of proofs rather than syntactic spelling.

2. Tree-Edit Proof Model:

   • The agent interacts with the prover via a tree-edit model that fuses proof operations and proof states into a single, evolving proof tree.
   • State Fusion: Unlike conventional agents where state is retrieved separately, every node in the proof tree carries the state of its subgoal. When an operation is applied, the prover computes the resulting state (goals, hypotheses, errors) and attaches it directly to the operation node.
   • Edit Operations: The agent uses tools (READ, EDIT, QUERY, SUBAGENT) to manipulate the tree. The EDIT tool supports filling slots, inserting nodes, amending operations, or deleting subtrees.
   • Incremental Synchronization: Upon an edit, the system returns a compressed view of the tree, showing only changed states and messages, rather than the entire tree. This eliminates the need for the LLM to re-read the entire context or navigate via brittle line numbers.

3. System Design without Model Modification:

   • AoA enables general-purpose LLMs to construct proofs in Minilang without fine-tuning. By abstracting away concrete syntax and exposing semantic structure via JSON, the system allows models with no prior exposure to Minilang's corpus to perform effectively.

Key Contributions

• Tree-Edit Proof Model: A novel interaction model that replaces source-file patching with proof-tree editing, eliminating the need for separate line-number-based proof-state queries.
• AoA Agent: A concrete implementation demonstrating that general-purpose LLMs can construct formal proofs in a new language (Minilang) purely through system design, without corpus-scale exposure or model fine-tuning.
• Empirical Evaluation: A comprehensive evaluation against Amazon's Isabelle Agent on the miniF2F (mathematical) and NTP4VC-Pearl (program verification) benchmarks.

Results
Evaluated on the common success sets of miniF2F and NTP4VC-Pearl, AoA demonstrates significant efficiency gains over Amazon's Isabelle Agent:

• Cost Reduction: Achieves 2.3–4.7× lower API costs (normalized for input-cache reuse).
• Token Efficiency: Uses 2.9–6.9× fewer total tokens and 3.9–8.9× fewer tool calls.
• Speed: Completes cases 1.4–2.0× faster.
• Performance:
  • miniF2F: Achieves a 99.6% pass rate (matching the state-of-the-art SeedProver).
  • NTP4VC-Pearl: Achieves an 89.2% pass rate, setting a new state-of-the-art for verification-condition proving.
• Generalization: When tested on Claude Opus 4.5 (released before the public Minilang corpus), AoA maintained a 98.6% pass rate, confirming that the approach works without prior corpus-scale exposure to the language.

Significance and Claims
The paper claims that the high cost of current proof agents stems from operating on serialized concrete syntax. By redesigning the proof language (Minilang) and exposing its AST within a tree-edit model, it is possible to:

1. Drastically reduce the API cost and token consumption of proof agents.
2. Enable general-purpose LLMs to operate in new formal languages without the need for expensive fine-tuning or massive training corpora.

The authors emphasize that this approach abstracts the semantic information of the proof language and re-expresses it in a format native to LLMs (JSON/AST), allowing the agent to focus on proof construction logic rather than syntactic navigation. The paper concludes that this methodology offers a scalable path for integrating LLMs into formal verification and suggests that similar AST-based approaches could benefit coding agents for newly designed programming languages.