Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, Bin Dong
cs.AI
Oct 6, 2025 · v2
TL;DR
Agent autoformalizes research-level conjectures into Lean, retrieving Mathlib definitions for grounding and checking semantic correctness of formalized statements.
Abstract
Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for LLMs due to hallucinations, semantic mismatches, and their inability to synthesize new definitions. To tackle these issues, we present Aria (Agent for Retrieval and Iterative Autoformalization), a system for conjecture-level formalization in Lean that emulates human expert reasoning via a two-phase Graph-of-Thought process: recursively decomposing statements into a dependency graph and then constructing formalizations from grounded concepts. To ensure semantic correctness, we introduce AriaScorer, a checker that retrieves definitions from Mathlib for term-level grounding, enabling rigorous and reliable verification. We evaluate Aria on diverse benchmarks. On ProofNet, it achieves 91.6% compilation success rate and 68.5% final accuracy, surpassing previous methods. On FATE-X, a suite of challenging algebra problems from research literature, it outperforms the best baseline with 44.0% vs. 24.0% final accuracy. On a dataset of homological conjectures, Aria reaches 42.9% final accuracy while all other models score 0%.
Problem
LLM-based autoformalization of research-level theorem statements is unreliable. Models hallucinate, produce semantic mismatches, and cannot synthesize new definitions that the statements require.
Approach
Aria uses a two-phase Graph-of-Thought process. It first recursively decomposes a statement into a dependency graph of concepts, then builds the Lean formalization bottom-up from grounded concepts. A checker called AriaScorer retrieves Mathlib definitions for term-level grounding, so the semantic correctness of the formalizations can be verified.
Results
On ProofNet, Aria reaches 91.6% compilation success and 68.5% final accuracy, surpassing previous methods. On FATE-X it reaches 44.0% final accuracy versus 24.0% for the best baseline. On a dataset of homological conjectures it reaches 42.9% while all other models score 0%.
