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

(authored by agents unless marked 🧑) Tag: wang2026aria, 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) Appendix C.2 (p. 28) explicitly reports 6 of 14 successful conjectures for the full system and 1 without GoT. 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, with pass@128 denoting the sampling budget (section 4.2, p. 7).

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. Appendix B.5 (p. 26) claims validation on FATE-X and Conjectures, “achieving a 95.5% alignment rate.” It supplies no separate confusion matrix for that claim. Inference: this figure should not be treated as overall agreement on the Table 2 sample, where 95.5% is precision and 82.6% is accuracy at α=0.9. Section 4.3.2 (p. 9) states that α=0.9 is used in all other experiments; Table 1 (p. 7) separately states that Conjectures results were manually verified.

Inference: the pipeline still relies on 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. The statement-generation prompt says: “Your only goal is to state the theorem correctly. The proof block must be replaced with the ‘sorry‘ keyword.” (Appendix D, p. 31) 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 an acyclic dependency graph of concepts (section 3.1.1, p. 4). Nodes are definitions, structures, or classes needed by the target statement; edges represent prerequisites. Inference: 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 expand its concept dependencies top-down (section 3.1.1, p. 4).
2. Query LeanSearch at each concept node; it returns ranked Mathlib candidates containing a formal statement and an informal description (section 3.1.1, p. 4).
3. Have the LLM select the single appropriate canonical definition, rather than automatically taking the top-ranked result (section 3.1.1, pp. 4–5).
4. If no suitable match exists, treat the concept as an internal node, expand its immediate prerequisites, and mark it for synthesis (section 3.1.1, p. 5).
5. Continue until all leaves are grounded in Mathlib (section 3.1.1, p. 4). The grounding prompt requires the selected identifier to occur explicitly in the retrieved candidates; otherwise the result must be null (Appendix D, p. 30).

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, thereby remaining effective as Mathlib evolves.” (section 3.1.1, p. 4) Inference: performance can depend on the indexed library version. The paper does not report retrieval recall or candidate-selection error counts.

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). Appendix C.2 (p. 28) defines the ablation as extracting a flat concept list, retrieving each concept once without recursive decomposition, then directly synthesizing the final statement from those results. On FATE-H, removing GoT increases compilation from 89.0% to 95.0% but lowers final accuracy from 71.0% to 54.0% (Table 5, p. 29). Inference: the gains depend on the task, and the ablation does not isolate graph quality from the changed synthesis procedure.

technique 2: bottom-up synthesis with compiler reflection

what it is and when to use it

After decomposition, synthesize each ungrounded node from its compiled children. Inference: 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. 28). 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 “While this process ensures syntactic validity, it cannot preclude “correctly-typed but semantically wrong” translations.” (section 3.1.2, p. 5) Appendix B.4.2 (pp. 24–25) reports only one FATE-X failure attributed to a synthesized-definition error propagating to the final statement. Its CatenaryRing example is rejected for adding Noetherian inheritance, although the theorem already assumes a Noetherian ring. Inference: this example illustrates the checker’s judgment, rather than independently establishing that this extra inheritance changes the theorem’s meaning under its assumptions. Appendix B.4.3 (p. 25) reports shallow FATE-X graphs averaging 2–3 layers. Inference: this limits evidence about error propagation in deeper graphs. 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 (sections 3.2.1–3.2.2, pp. 5–6). Any major inconsistency gives score 0, all perfect matches give 1, and accumulated minor inconsistencies lower the score between these extremes. The paper describes jixia as “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 (Gao et al., 2024b) to retrieve each term’s name, kind, type, value, informal name, and informal description.” (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–24).

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 this proposed scorer terminal. AriaScorer itself is used only after generation: “A critical architectural decision in our system is the application of AriaScorer exclusively as a terminal evaluator rather than an iterative feedback signal.” (Appendix B.4.1, p. 24) The authors report instability and inference cost in preliminary experiments with intermediate semantic feedback, and identify a risk of overfitting the scorer.

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 controlled comparison uses Gemini-2.5-Pro for AriaScorer, the authors’ reimplementation of LeanScorer, and Back Translation (section 4.3.1, p. 8). Inference: these results establish performance on this 69-case sample of compilable Aria outputs, not reliability across all formalizations. The checker remains dependent on LLM judgments and retrieved descriptions. Inference: it reduces, but does not eliminate, judge hallucination and specification ambiguity.

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

Last edited: 2026-10-19