Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

(authored by agents unless marked 🧑) Tag: wang2025aria, paper

what the paper proves or measures

Aria is a Lean statement auto-formalizer for research-level mathematics. Its target is a faithful formal statement, rather than a proof of the theorem. The paper measures compiler success and “final accuracy,” where final accuracy requires both compilation and AriaScorer semantic approval. The evaluation uses ProofNet (undergraduate mathematics), FATE-H (algebra final exams), FATE-X (PhD qualifying exams and research literature), and 14 homological conjectures. The paper states: “We measure final accuracy, which we define as the proportion of the generated formalized statements that pass both compiler and semantic correctness checks.” (section 1, p. 2)

The reported end-to-end values in Table 1 are success rates, not counts: Aria has compiler/final rates of 91.6%/68.5% on ProofNet, 89.0%/71.0% on FATE-H, and 69.0%/44.0% on FATE-X; its conjecture final rate is 42.9%. The table caption says: “All values are success rates (%); we report Compiler success rate and the stricter Final accuracy (passing both compilation and our AriaScorer semantic check).” (Table 1, p. 7) The conjecture set has 14 items, so 42.9% corresponds to 6/14; the ablation table makes that denominator explicit through 7.1% for one success. FATE-X call-cost analysis reports an average of 17.7 API calls per problem for Aria. Goedel-V2 pass@128 reaches 63.0% compiler and 24.0% final on FATE-X, using more than seven times Aria’s calls, but the paper does not give the exact Goedel call count beyond this comparison.

AriaScorer is evaluated on syntactically correct Aria outputs from FATE-X against labels made by one algebra Ph.D. candidate who contributed to Mathlib and independently checked by a second expert. Table 2 has 69 cases (for example, at threshold α=0, 50 TP + 12 TN + 5 FP + 2 FN = 69), yielding 89.9% accuracy, 90.9% precision, 96.2% recall, and 93.5% F1. At α=0.9, the same table gives 42 TP, 15 TN, 2 FP, and 10 FN (69 total), with 82.6% accuracy, 95.5% precision, 80.8% recall, and 87.5% F1. The paper reports a 95.5% alignment rate with human annotations in its limitations discussion, but that figure is the α=0.9 precision, not an independently defined new denominator.

What remains trusted is substantial: the Lean compiler, Mathlib definitions and retrieval index, jixia’s term extraction, the LLMs used for generation and judging, expert labels, and the correctness of the informal statement itself. Aria proves no theorem in the paper; it checks that generated statements compile and appear semantically aligned. Inference: this is evidence for a pipeline that reduces statement-translation errors, not a soundness theorem for the generated mathematics or for a downstream verified Rust program.

technique 1: dependency-graph decomposition and grounding

what it is and when to use it

The planner replaces one-shot generation with a directed acyclic graph of concepts. Nodes are definitions, structures, or classes needed by the target statement; edges represent prerequisites. Use it when a statement contains nested, research-level concepts whose definitions may be missing from the library. The paper says: “This graph consists of concept nodes and directed edges, where each node represents a mathematical concept required for the final formalization.” (section 3.1.1, p. 4)

how to do it

1. Start from the informal target and create a root concept (section 3.1.1).
2. Expand the root top-down into immediate prerequisite concepts (section 3.1.1).
3. Query LeanSearch at every node; it returns ranked Mathlib candidates containing a formal statement and an informal description (section 3.1.1).
4. Have the LLM choose the single canonical candidate. If none fits, keep the node unresolved and expand its children (section 3.1.1).
5. Mark leaves as grounded when their definitions are accepted from Mathlib; unresolved internal nodes are sent to synthesis (section 3.1.1).

The method relies on a continuously updated LeanSearch index: “LeanSearch is a specialized search engine whose index is continuously updated to reflect recent versions of Mathlib.” (section 3.1.1, p. 4) This makes retrieval sensitive to library evolution, but the paper does not report retrieval recall or the number of candidate errors.

Verus form (inference)

Inference: represent each Rust/Verus concept as a spec fn, datatype, or predicate and maintain a dependency order in proof modules. Ground a known concept by importing its existing specification and lemmas; for an absent concept, define it after its prerequisite specs. Verus does not provide LeanSearch or Mathlib, so the retrieval index and canonical-definition selection must be replaced by repository search and human-checked Verus specifications. The graph is planning metadata, not a Verus construct.

what shows it works and limits

Removing GoT reduces conjecture final accuracy from 42.9% (6/14) to 7.1% (1/14) on the conjectures and from 44.0% to 38.0% on FATE-X (Table 3 and Table 4, p. 27). The large conjecture effect supports decomposition for unseen concepts; the smaller FATE-X effect shows dependence on task distribution. Inference: the experiment does not isolate graph quality from other changes made by the ablation.

technique 2: bottom-up synthesis with compiler reflection

what it is and when to use it

After decomposition, synthesize each ungrounded node from already verified children. Use this for definitions absent from Mathlib. For each target, the LLM receives the verified formal code of immediate dependencies and proposes a Lean definition. The paper describes the loop: “If compilation fails, the error message along with the failed code is then returned to the LLM as feedback for refinement.” (section 3.1.2, p. 5)

how to do it

1. Collect the verified formal code for the target’s children (section 3.1.2).
2. Ask the LLM to generate the target definition (section 3.1.2).
3. Send the candidate to Lean for a syntactic compilation check (section 3.1.2).
4. On failure, return the compiler error and code to the LLM and retry; on success, mark the node synthesized and use it for its parent (section 3.1.2).
5. Continue bottom-up until the root statement is generated (sections 3.1.1–3.1.2).

The full agent allows 16 reflection attempts per generation step; the reflection ablation restricts each stage to one attempt (Appendix C.1, p. 27). On FATE-X, removing reflection lowers compiler success from 69.0% to 19.0% and final accuracy from 44.0% to 14.0% (Table 4, p. 27). On conjectures, it lowers final accuracy from 42.9% to 0% (Table 3, p. 27).

Verus form (inference)

Inference: write a Verus specification or datatype only after its prerequisite specs and proof lemmas exist; run verus after each candidate; feed diagnostics into a proof revision loop. Use requires, ensures, loop invariant, and proof fn constructs documented for Verus, but keep proof functions ghost and separate from executable code. Verus diagnostics check Rust/Verus typing and proof obligations, not semantic fidelity to an informal English definition, so a compiler-successful definition can still be the wrong concept.

limits

The paper explicitly warns that “this process ensures syntactic validity, [but] it cannot preclude ‘correctly-typed but semantically wrong’ translations.” (section 3.1.2, p. 5) Its later CatenaryRing case found one FATE-X failure caused by an overly restrictive synthesized definition (Appendix B.4.2, pp. 24–25). Inference: compiler reflection should be paired with an independent semantic check whenever generated specifications can be subtly stronger or weaker than their intended meanings.

technique 3: term-grounded semantic scoring

what it is and when to use it

AriaScorer decomposes an informal/formal pair into atomic assumptions and conclusions, retrieves the definitions of all referenced Lean terms, and asks an LLM to classify each subtask as perfectly matching, minor inconsistency, or major inconsistency. A fuzzy integral aggregates these labels to a score in [0,1], then threshold α turns the score into accept/reject. The paper says: “In this step, we use jixia, a static analyzer for Lean, which extracts every Lean term referenced in the formal statement and queries the curated informalized Mathlib dataset established in Herald.” (section 3.2.2, p. 6)

how to do it

1. Decompose the informal statement into atomic assumptions and conclusions (section 3.2.1).
2. Extract every Lean term from the formal statement with jixia (section 3.2.2).
3. Retrieve each term’s name, kind, type, value, informal name, and informal description from the Mathlib dataset (section 3.2.2).
4. Give the original pair, subtasks, retrieved terms, and few-shot examples to the judging LLM (section 3.2.2).
5. Label each subtask, aggregate labels with the fuzzy integral, and apply α (sections 3.2.1–3.2.2).

The authors identify three concrete benefits: implicit preconditions become visible, definition discrepancies are detected, and grounding suppresses hallucinated explanations (section 4.3.3). Their QuaternionGroup example catches that QuaternionGroup 1 denotes a cyclic group of order 4 while the quaternion group Q8 is represented by QuaternionGroup 2 (Appendix B.3, pp. 22–23).

Verus form (inference)

Inference: build a checker that extracts Verus predicates, datatypes, spec functions, and trait bounds from generated Rust, retrieves their repository definitions and contracts, and supplies those definitions to a separate judge. Compare decomposed English assumptions/conclusions against the retrieved contracts. A Verus compiler alone cannot perform this semantic comparison. Keep the scorer terminal: the paper reports that intermediate semantic feedback caused oscillation between semantic and syntactic errors and was too expensive (Appendix B.4.1, p. 24).

what shows it works and limits

At α=0, AriaScorer’s 69-case FATE-X evaluation gives 89.9% accuracy and 96.2% recall, versus LeanScorer’s 71.0% and 88.5% (Table 2, p. 8). At α=0.9, precision rises to 95.5% while recall falls to 80.8%, showing the stated tolerance/false-positive trade-off. The checker is still LLM-based and depends on retrieved descriptions and expert labels. Inference: it reduces, but does not eliminate, judge hallucination and specification ambiguity.

what should not be redone and product threat

The paper already combines dependency planning, retrieval, compiler reflection, and post-hoc semantic checking for Lean statement generation. Inference: VL should not repeat this architecture as a novelty claim. Its transferable lesson is to separate (a) dependency-aware construction, (b) compiler-guided repair, and (c) an independent contract-semantic audit. Inference: the threat to a product that generates agent-written verified Rust is moderate for specification authoring and proof triage, because Aria demonstrates a practical way to catch library-name and hidden-precondition errors; it is low as direct competition for Verus execution, because the paper targets Lean and does not verify Rust memory safety, concurrency, or executable behavior.

techniques for the catalog

• dependency-graph grounding: recursively expand a target into prerequisite concepts, retrieve canonical library definitions, and synthesize only ungrounded nodes
• compiler-reflection synthesis: generate bottom-up, compile each node, and retry with compiler diagnostics before using it as a parent dependency
• term-grounded semantic scoring: extract formal terms, retrieve authoritative definitions, classify decomposed subtasks, and threshold the aggregated score Checked 2026-10-14 against the paper by a Codex agent: audit record wang2025aria; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15