TLDR: Aria is an AI agent designed for auto-formalization of mathematical statements into Lean code. It employs a two-phase Graph-of-Thought process to decompose complex problems and synthesize formalizations from grounded concepts in Mathlib. With a compiler-in-the-loop for self-reflection and AriaScorer for term-level semantic verification, it achieves state-of-the-art performance, significantly outperforming previous methods on challenging research-level conjectures.
In the complex world of advanced mathematics, translating informal human-written theorems and conjectures into precise, verifiable formal code is a monumental task. This process, known as auto-formalization, is crucial for developing automated systems that can discover and verify new mathematical knowledge. However, it has long been a significant hurdle for artificial intelligence, with large language models often struggling with inaccuracies, misunderstandings, and the inability to create new definitions.
Addressing these challenges head-on, researchers have introduced Aria (Agent for Retrieval and Iterative Auto-formalization), an innovative system designed to formalize complex mathematical statements in Lean, a popular interactive theorem prover. Aria mimics the way human mathematicians approach problems, employing a sophisticated two-phase “Graph-of-Thought” process.
How Aria Works: A Two-Phase Approach
Aria’s methodology is built on breaking down complex problems into manageable parts. The first phase, Graph-of-Thought Decomposition, involves recursively deconstructing a mathematical statement into a dependency graph of concepts. Imagine a complex puzzle being broken down into individual pieces, where each piece represents a definition or a structure. Aria then attempts to “ground” these concepts by searching for existing definitions in Mathlib, Lean’s extensive mathematical library, using a specialized search engine called LeanSearch. This retrieval-augmented generation (RAG) framework ensures that Aria uses the most current and accurate mathematical knowledge, preventing issues like hallucinating non-existent functions or using outdated information.
If a concept cannot be directly found in Mathlib, Aria moves to the second phase: Graph-of-Thought Synthesis. Here, it works bottom-up, generating new formal definitions for these ungrounded concepts. This creative synthesis is guided by a “compiler-in-the-loop reflection” mechanism. After generating a piece of code, Aria sends it to the Lean compiler for a syntactic check. If there are errors, the compiler provides feedback, and Aria uses this information to refine its code, iterating until it achieves a syntactically correct formalization. This iterative self-correction is vital for ensuring the robustness of the generated code.
Ensuring Semantic Accuracy with AriaScorer
Beyond just compiling successfully, a formal statement must also accurately reflect the original mathematical meaning. To tackle this, Aria introduces AriaScorer, an advanced semantic checker. Unlike previous methods that relied on superficial text comparisons, AriaScorer incorporates a “term-level grounding” step. It retrieves the authoritative definitions of all Lean terms from Mathlib and injects this formal context into the comparison process. This allows AriaScorer to detect subtle discrepancies, such as reversed parameter orders or unintended type coercions, which are easily missed by simpler textual analyses. This rigorous verification ensures that Aria’s formalizations are not only syntactically valid but also semantically correct.
Also Read:
- FormalML: A New Benchmark to Bridge AI and Advanced Mathematical Proofs
- Enhancing Mathematical Reasoning in LLMs with Adaptive Learning
Breakthrough Performance
Aria’s effectiveness has been rigorously evaluated on various benchmarks, demonstrating significant advancements over prior methods. On ProofNet, a benchmark for undergraduate-level mathematics, Aria achieved a 91.6% compilation success rate and 68.5% final accuracy. More impressively, on FATE-X, a suite of challenging algebra problems from research literature, Aria outperformed the best baseline with 44.0% versus 24.0% final accuracy. Most notably, on a dataset of homological conjectures—real-world mathematical problems where all other models scored 0%—Aria achieved a remarkable 42.9% final accuracy. This unique capability for formalizing research-level conjectures highlights Aria’s potential to push the boundaries of automated mathematical discovery.
The success of Aria underscores the importance of its integrated approach: combining retrieval-augmented generation for grounding, graph-of-thought planning for structured reasoning, and compiler-guided self-reflection for refinement. This work lays a solid foundation for future advancements in automated mathematical proof at the frontier of research. You can read the full research paper here.
