Aria: an Agent for Retrieval and Iterative Auto-Formalization via Dependency Graph
Authors: Hanyu Wang
Ruohan Xie
Yutong Wang
Guoxiong Gao
XintaoYu
Bin Dong
Venue: ICLR 2026 Poster (2026)
Keywords: Lean 4
Autoformalization
LLM
Graph-of-Thought
Retrieval Augmented Generation
Primary area: foundation or frontier models, including LLMs

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 (**A**gent for **R**etrieval and **I**terative **A**utoformalization), 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\%.

Published as a conference paper at ICLR 2026
ARIA: AN AGENT FOR RETRIEVAL AND ITERATIVE  FOTTALLORMALINNTIONN VIA DEPENDENCY GRAPH
Hanyu Wang
Ruohan Xie
Yutong Wang" 1.2+
Guoxiong Gao 1.2
Xintao Yu
Bin Dong*.5.6f
Peeiing University "IQuest Research RRemmin University of China
'Beijing International Center for Mathematical Research and the New Comnerttnne Science
Laboratory, Peking University
"Center for Machine Learning Research, Peking University
"Center for Intelligent Computing, Great Bay Institute for Advanced Study, Great Bay University wanghanyu2004@stuu pku.edu. edu. cn, xieruohan@stu. www.esstuuuuuuu...... pkk.puuuuuuu edu.cn cn wangyuteeng2esstu. pku edu, en, samggxestu. pku. puu.edu.u......e....... cn
RUCxintaoyuBoutllokk com, dongbin@math..ku..du.
ABSTRACT
Accurate cottaloomaliztiion of theorem statements is essential for advancing au- tomated discovery and verification of research-level mathematics, yet remains 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) 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 depen- dency 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, suite of challenging algebra problems from research lit- erature, outperforms the best baseline with 44.0% vs. 24.0% final accuracy. On dataset of homological conjectures, Aria reaches 42.9% final accuracy while all other models score 0%%
INTRODUCTION
In recent years, Interactive Theorem Provers (ITPs) such as Coq (Barras al. 1999), Isabelle (Paul- son 1994) and Lean (Moura & Ullrich 202T) have become crucial ecosystems for formalized math- ematics. Among these, Lean 4, together with its comprehensive library Mathlib (mathlib Commu- nity 2020 is pioneering new paradigm for formalization. However, the continuous growth of this ecosystem is always constrained by the immense manual effort and the deep expertise that formal- ization demands. To address this, the research community has turned to Large Language Models (LLMss for auto-formalization the process of translating informal (or natural language) mathemat- ical statements and proofs into their formal counterparts. While these two processes are intercon- nected, the accurate formalization of statements is the foundational first step. A correctly formalized statement is prerequisite for any valid proof and, on its own, valuable asset to the mathemati- cal ecosystem, enabling better search, integration, and verification. Thus, despite progress in proof automation (Ren et al. 2025; Chen al.) 2025). the fidelity of this initial statement translation re- mains a critical bottleneck. LLMs frequently generate formal statements that suffer not only from compilation errors but also from more insidious semantic flaws, challenge that intensifies when formalizing more complex research conjecture-level statements.
"Equal contribution. Corresponning author.

---

Published as a conference paper at ICLR 2026
These foundational shortcomings manifest in several critical downstream failures. An unfaithful translation can derail large-scale data generation pipelines, wasting significant computational bud- gets attempts to prove an incorrect premise. For instance, modern provers often decompose complex proofs into smaller, informal lemmas, which are then individually translated and proven. In this workflow, single flawed translation of lemma not only invalidates the entire proof structure but can also contaminate the datasets generated during this process, which are crucial for fine-tuning future models. Furthermore, as the research community pushes towards formal models that can au- tonomously explore conjecture-level problems, the inability to create and utilize the necessary, often unseen, premises (i.e. definitions, lemmas, theorems, etc.) becomes critical roadblock. Any sys- tem lacking this capability is bound to fail at the outset of such ambitious tasks. In this work, we address these challenges by introducing a robust methodology to generate, iterate, and verify formal statements, tackling these foundational bottlenecks through automated structural reasoning.
One primary challenge stems from the static nature and inherent fallibility of an LLM's pre-trained knowledge. While foundational work has demonstrated the potential of LLMs up to undergraduate mathematics (Gao et al. 2024b Wang et al. 2025), these methods exhibit critical failure modes when confronted with research-level statements, where LLMs are prone to hallucination and out- dated pre- pre-trained knowledge. They generate invalid codes with functions either non-existem in Mathlib, or incompatible with rapidly evolving library toolchains. To address this, we integrate Setrieval-Augmentee Generation (RAG) framework, grounding the formalization process by dy- namically querying the most current version of the Mathlib library, mitigating the model's depen- dence on static knowledge and ensuring compatibility with the evolving toolchain.
Beyond the issue of knowledge retrieval, a more profound challenge lies in synthesis. Research- level mathematics fundamentally involves creating new mathematical objects and definitions, one- pass generation methods, even when augmented with retrieval, fail at this task because they cannot spontaneously synthesize definitions for concepts absent from existing libraries. To address this, we develop an agentic pipeline driven by Graph-of-Thouge (GoT) formalizing process. This approach emulates an expert mathematician's 's workflow by recursively decomposing dependencies of definitions until they are well gollngrounded, then synthesizes their formal statements a bottom-up order until the primary target is formalized. To ensure the robustness of this process, compiler-in- the-loop reflection mechanism employed at each node.
Once a statement is generated and pass the compiler check, the ultimate challenge is to ensure its semantic correctness. While existing methods like LeanScorer (Xuejun et al.) 2025) have advanced semantic checking by performing fine-grained comparisons, they fail detect subtle definitive dis- crepancies between formal and informal terms due to reliance on superficial textual similarity. To overcome this limitation, a term-level grounding step. AriaScorer retrieves the authoritative definitions of all Lean terms from Mathlib and injects this formal context into the comparison process, enabling a more rigorous and accurate evaluation.
introduce AriaScorer,
enhanced semantic checker that incorporates
Equipped with this validated checker, we evaluated Aria's end-to-end performance on suite of research- datasets. We measure final accuracy, which we define as the proportion of the gen- erated formalized statements that pass both compiler and semantic correctness checks. The results demonstrate a significant leap over prior work, with Aria achieving 68.5% on the ProofNet bench- mark while also surpassing previous state-of-the-ar models on others, including FATE-H (71.0% challenging set of real-world
vs. 43.0%) and FATE-X (44.0% vs. 24.0%). Most notably, mathematical conjectures where all baseline models score 0%, Aria achieves 42.9% success rate, demonstrating unique capability for research-level formalization.
The main contributions of this paper are as follows:
We introduce Aria, statement auto-formalizer agent that emulates the human formaliza- tion process by integrating aatrivval-aummente generation, ofuh-oof-thought planning, and a compiler-guide self-reflection mechanism that is especially effective on conjecture-level problems.
We develop term-level grounded semantic scorer, AriaScorer, to detect subtle discrepan- cies between informal statements and Lean terms, and to accurately verify the mathematical correctness of formalizations.
2

---

Published as a conference paper at ICLR 2026
We achieve sfate-of-the-art performance with substantial improvements over previous methods, reaching 68.5% on ProofNet, 71.0% on FATE-H, 44.0% on FATE-X, and 42.9% real-world conjectures proposed by mathemattciins.
The remainder of this paper is structured as follows. Section 2 reviews related work. Section details our proposed methodology, including Aria's architecture and its core components. Section presents our experimental results and their analysis. Finally, Section concludes the paper.
RELATED WORK
Auto-formalization The rapid advancement of Large Language Models (LLMs) has catalyzed significant progress in auto-formalizatio. Early efforts demonstrated success by leveraging few- shot in-context learning (ICL) (Wu et al. 2022 Patel et al. 2024 Zhou et al. 2024). As the Lean community grew and its Mathlib library became more comprehensive, the availability of large- scale datasets enabled the development of specialized models through supervised fine-tuning (SFT) Azerbayev et al., 2023] Jiang et al.) 2023) Gao et al. 2024bb Wang et al.) 2025). More recently, Reinforcement Learning (RL) has shown potential mathematics and inference, and several works have leveraged RL training to enhance the quality of auto- cotto-fommaliattoon (Xuejun et al. [2025] Huang et al. 2025). In parallel, other methods have focused on enhancing the quality and reliabiiit of the generation process itself. With the increasingly powerful search capabilities within the Lean ecosys- tem, Retrieval- Augmenttd Generation (RAG) has proven effective at providing models with relevant definitions and theorems from the extensive Mathlib library (Lu et al. 2025) Concurrently, novel methodologies like Process-Superviieed Verification (PSV) leverage direct feedback from compilers to guide the model's 's learning process, significantly improving the correctness and reliability of the generated formalizations (Lu et al. 2024). Similarly, in the adjacent field of automated theorem proving, recent works (Thakur al.) 2024 Zhou al., 2025 Chen et al. 2025) have demonstrated the efficacy of reflection mechanisms, enabling systems to iteratively critique and refine their rea- soning strategies.
Semantic Check As methods for statement auto-formalization have become more sophisticated and diverse, it is crucial to establish a credible way evaluate the extent which the formal state- ment preserves the mathematical meaning of its informal counterpart. Human experts can certainly provide reliable evaluations of consistency (Azerbayev al., 2023). but as statements grow more complex, such evaluations become increasingly demanding. Consequently, perplexity (Wang et al., 2018) and BLEU (Wang et al., 2018 Azerbayev et al., 2023) have been used as proxy metrics. also common to use an L.LM to back-translate valid formal statements into informal statements, and then employ another L.LM to assess semantic preservation (Ying et al.] 2024, Gao et al. 2024bb
Liu et al. 2025b). Additionally, a combined structure of unanimous voting among LLM judges and validation by Lean experts has been introduced, serving as a reward signal during training (Wang al. 2025). Moreover, subtask decomposition of informal statements has been considered, sulting in a more fine-grained filtering of incorrect formalizations (Xuejun et al.) (023). Recently, an automated neuro-symbolic method for determining the mathematical equivalence of formal statements has been widely adopted. This approach establishes equivalence and only if a formal proof can connect the two statements, by using semantic- preseervip tacties (Liu et al. 2025a Wu et al. 2025).
METHODOLOGY
This section details methodology, which is comprised of two primary components. The overall pipeline is shown in Figure [] Section 3.1 describes Aria's architecture, a structured pipeline de- signed to navigate the deep conceptual dependencies in conjecture-level mathematical statements. Then Section presents our integrated semantic checker, which verifies whether the agent's output faithful to the original mathematical intent.
3.1 THE GRAPH-OF-THOUGHT (GoT) AUTO- FORMALIZRR PIPELINE
In this section, we detail the architecture of our agent, Aria. This architecture moves beyond the conventional approach of direct, single-step generation. These methods often fail when applied to
3

---

Published as a conference paper at ICLR 2026
Decompostion
Synthesi
rocutt
Mabiib prouddded Net prounded Decondencyy
ClArk grounder ferailaation Systeaee
divaniiion
Nrull dir anstion
capp
roatheran
FC mermial ring
Cotter Mancautyy
Touths
Cohan Macemaay
Nr Naki by Midee Thstinal
The giots
Palfactio
AiiaScoror
Pecept
Reject
Mamia
man, Let Cohan Macaulay module over Then M a Rl ih is Cohen- Maraulay module over Re (f
Park Matce
recus
Paricty
Informal Statement
Judgo
Formalized Statement
Figure I: The overall pipeline of Aria system. (A) Graph-of-Thought Decomposition: Aria ex- pands the informal statement into dependency graph of concepts and grounds them in Mathlib. (B) Graph-of- Graph-of-Thought Synthesis: The system executes bottom-up synthesis procedure guided by the graph, incorporating a self-reflection loop. (C) AriaScorer: A dedicated module that verifies the semantic correctness between the generated formal statement and the original informal statement.
complex, conjecture-level statements. As illustrated in Figure 1 our agent operates through struc- tured pipeline that systematically deconstructs, resolves, synthesizes and verifies formalization, mirroring the methodical process of a human mathematician.
This pipeline uses a graph-of-Thoughee (GoT) planner to deconstruct an informal statement into a conceptual graph, where each concept node represents definition, structure or class, as illustrated in Figure [ (A). Each concept node in the graph is then processed by a grounding module, which Generation (RAG) framework powered by LeanSearch (Gao al.) 2024ap to anchor known concepts to the Mathlib library. For ungrounded concepts, a synthesis mod- ule generates new definitions bottom-up, as depicted in Figure (B). ). All outputs are validated and refined by compiler-ing -aapiile--i-tte-loyee reflection module. Finally, we employ a retrieval -based checker to verify semantic correctness.
employs a Retrieval-Augmente
3.1.1 GoT DECOMPOSITION PHASE
To manage the complex, acyclic dependency graph of definitions and lemmas required to formalize a high difficulty-level statement, our agent's architecture centered around Planning Module based on the GoT paradigm. This module transforms the monolithic task of formalization into a structured, manageable workflow by modeling it the construction and resolution of a conceptual dependency graph, as shown in Figure (A). This approach is founded on key principle of mathematical abstraction, which our agent leverages directly: any concept, no matter how complex, can be defined solely in terms of its immediate prerequisite concepts.
The core of our planning module is conceptual dependency graph, a dynamic data structure that serves as the agent's 's working memory. This graph consists of concept nodes and directed edges, where each node represents mathematical concept required for the final formalization.
For given statement, Aria initiates full formalization routine: it performs top-down dependency expansion of the concept graph until all leaf nodes can be grounded in Mathlib. To achieve this grounding, the agent queries LeanSearch at each node. LeanSearch is specialized search engine whose index is continuously updated to reflect recent versions of Mathlib, thereby remaining ef- fective Mathlib evolves. This retrieval process returns ranked list of candidates from Mathlib, where each candidate consists of a formal statement and its corresponding informal description, ordered by their semantic relevance the input concept name.
Since the top ranked search result is not always the canonical definition required for formalization, the agent employs an LLM sophisticated reasoner analyze the retrieved candidates, identify-
4

---

Published as a conference paper at ICLR 2026
ing the single best appropriate canonical definition for the concept. If the reasoner concludes that no suitable match exists among the candidates (i.e., the concept is not grounded in Mathlib), the node is treated status triggers the planner to continue the top-down expansion of its children, after which the node is marked for synthesis.
internal node in the dependency graph (as depicted in Figure I (A). Its unresolved
3.1.2 GOT SYNTHESIZING PHASE
Immediately upon completing all expansions, the agent transitions to a bottom-up synthesis phase for the whole graph, which is shown in Figure[[( The synthesis module is invoked for any con- cept that could not be grounded in the Mathlib library (for instance, the concept "Conen-Macaulay Module" in Figure [ (B)). This module is responsible for generating verifiable formal definitions from the ground up, guided by robust compiler-in-the-llop reflection process that ensures syntac- tic correctness.
For a given target concept, the agent first collects the verified formal code of all its immediate dependencies (i.e. its children in the dependency graph) use as context for the LLM to generate formal Lean definition for the target. The generated code is immediately sent to the Lean compiler for a syntactic check. If compilation fails, the error message along with the failed code then returned to the L.M as feedback for refinement. If it succeeds, the code is marked as synthesized and used for the synthesis of parent node.
While this process ensures syntactic validity, it cannot preclude "correctly-type but semantically wrong" translations. check the semantic correctness our code with a more flexible approach, our methodology incorporates an enhanced retrieval-based semantic consistency checker, which is detailed in Section
3.2 SEMANTIC CORRECTNESS MODULE: ARTASCORER
Decompoeed nabtasics
ceakation
Original infermal utatmmnnt
Acseppiom:
Math Axch4 (l... ay K.
Score coloriatio
incernsterry
Let for caloreiaii cadess Pove
Leart:
Bi V. Sishaiion
2 the octle gron srarder
Galdk: 12/0R0
Mate: any (h.....)) EC Leon
Uioigromia Intetten
hertis resective
Incoralcencsp (0.1)
Farmal statement check
aSced aune Canuraupehaccaa
Math
C( 10
aSeed Bustais Tharracs Meed (kteake)
Leen in
Made Nivor incossntency.
I Acreet
x Rojoc
Retieand Loan beice
The overall pipeline of AriaScorer: informal statements are decomposed into subtasks, grounded with retrieved Lean terms, and their evaluations are aggregated into final score, which is compared against threshold a E [0, 1] to yield binary decision.
Figure 2:
3.2.1 GROUNDWORK: LEANSCORER
We propose a semantic correctness checker for toroofooaal Lean statements aimed at mitigating hallucinations and reducing the false positives inherent in LLM- -egerreedttedd outputs. To address the densely packed, cenuntiion-sesiiivee nature of high difficult-Ievell statements (such as conjectures), we adopt the subtask decomposition strategy of LeanScorer (Xuejun et al. 2025), which evaluates the semantic correctness through sebtask-level comparisons.
Given an original informal statement, it is decomposed into atomic assumptions and conclusions by an LLM, and each resulting subtask is then evaluated to determine how well its formal clause matches the corresponding informal one. Subtasks are labeled as Perfectly Match, Minor Inconsis- tency, or Major Inconsistency, and these labels are aggregated via a fuzzy integral into final score between 0 and 1, where 0 indicates the presence of major error and reflects perfect alignment across all subtasks. Besides these two cases, the score decays gradually from 1 with accumulating minor inconsistencies, capturing the cumulative effect of subtle deviations. A tunable threshold is
5

---

Published as a conference paper at ICLR 2026
applied to make binary decisions, balancing tolerance for small deviations against the need ject semantically incorrect formalizations. Nonetheless, because this method still relies heavily on surface-level textual similarity, it remains vulnerable to semantic mismatches hidden beneath super- ficially close expressions, which motivates our introduction of a term-grounded evaluation module.
3.2.2 TERM-LEVEL SEMANTIC GROUNDING
To ensure alignment between the evaluation process and the true semantics of formal Lean state- ments, we introduce new step: term-level retrieval and interpretation. In this step, we use jixię [ 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. 2022bb to retrieve each term's name, kind, type, value, informal name, and informal deseription. The retrieved term information, together with the original informal and formal statements, the decomposed subtask list, and few-shot examples, then provided as context to the LLM during the subtask evaluation stage.
This process serves as the foundation for semantic grounding, enabling AriaScorer to reason over the true meanings of formal components rather than their surface syntax. As a result, AriaScorer can identify subtle inconsistencies, such reversed parameter order unintended type coercions, all of which are easily missed by purely textual comparison. This step helps prevent common LLM failure modes, including: (i) overlooking implicit preconditions constraints embedded in Lean term definitions; (ii) misinterpreting Lean definitions by defaulting to their more familiar mathematical counterparts when the diverge; and (iii) hallucinating incorrect explanations of Lean ferms. These error types and how AriaScorer addresses them are discussed in Section 4.3.3 with detailed illustrations provided in the case studies.
By grounding evaluation in the actual semantics of Lean terms, AriaScorer provides more reli- able and fine-grained assessments, particularly in cases involving newly introduced user-defined structures. To validate the impact of this semantic grounding step, we present an ablation study in Section 4.3 showing clear gains in error detection and reductions in false positives.
EXPERIMENTS
We conduct extensive experiments to evaluate the performance of Aria and AriaScorer. In Section we describe the experimental setup of Aria, while Section 4.2 presents the main results. Section demonstrates the comprehensive experiment to validate AriaScorer Finally, we analyze the contributions of key components through ablation studies in Section
4.1
EXPERIMENTAL SETUP ARIA
This section outlines the experimental framework for rigorously evaluating Aria's performance, in- cluding the datasets used and the baselines for comparison.
4.1.1 BENCHMARKS
To rigorously assess our agent across diverse difficulty levels and problem types, we evaluate it on a suite of benchmarks. Specifically, we use the widely adopted ProofNet (Azerbayev et al., 2023) to ensure generalizability and comparability with existing work, and the FATE (liang et al., 2025)
(Formal Algebra Theorem Evaluation) collection together with dataset of 14 real conjectures to test performance complex, rescarch-level problems.
ProofNet To assess generalizability, we use ProofNet, widely-adopted benchmark of undergraduate-leve mathematics. This ensures our agent's 's sophisticated architecture is not only effective for complex conjectures but also robust and competitive on standard problems.
FATE-H & FATE-X The FATE collection tests our agent on advanced mathematics. FATE-H
comprises problems from algebra final exams, while FATE-X contains more difficult problems from PhD qualifying exams and research literature. These benchmarks were specifically chosen to evalu- ate our agent's capabilities on complex, research-level mathematics.

---

Published as a conference paper at ICLR 2026
Table 1: End-to-end auto-formalization results comparing Aria against specialized models. All values are success rates (%); we report Compiler success rate and the stricter Final accuracy (passing both compilation and our AriaScorer semantic check). Results for the Conjectures dataset were manually verified. Kimina's score on ProofNet is marked due to potential data contamination".
ProofNet
FATE-H
FATE-X
Method
Conjectures
Compiler Final acc. Compiler Final acc. Compiler Final acc.
Aria
91.6
68.5
89.0
71.0
69.0
44.0
42.9
Goedel-V (pass@ 16)
77.0
37.0
Goedel-Ve V2 (pass @2)
82.0
49.0
0
Goedel V2 (4ass@64)
88.0
58.0
0
Gocdel V2 (pass@ 128)
91.0
43.0
63.0
24.0
0
Gemini 2.5 Pro-Pro (pass@1) 1)
55,8
27.8
35.0
31.0
27.0
21.0
0
Goedel- V2 (pass@1 @ I)
59.6
32.0
35.0
27.0
27.0
16.0
Kimina (pass @ I)
70.4'
24.7'
10.0
0.0
5.0
1.0
Herald (pass @ 1)
48.5
18.3
24.0
12.0
8.0
5.0
0
Kimina was trained on the ProofNet dataset, so its reported score may not reflect true generalization capabilities.
Homological Conjectures in Commutative Algebra (Conjectures) Finally, we test Aria on set of 14 real-world Homological Conjectures (Wikipedia contributors (225) in Commutative Algebra, compiled by Melvin Hochster. These conjectures probe deep connections between the homological properties of commutative Noetherian ring and its structural characteristics. This serves as direct and challenging testbed of Aria's ability to formalize active mathematical research problems.
4.1.2 BASELINE MODELS
To evaluate the efficacy of our agent's architecture, we compare it against several leading state- ment auto-formalization models, including a powerful reasoning model Gemini-2.5-Pro (Google DeepMind) and specialized fotmalermsss including Goedel-Formalizer--22222 (Lin et al., 2023), Kimina-Autoformalizer (Kimina) (Wang et al. 2025) and Herald-translator
(Goedel-V2)
(Herald) (Gao al. 2024b).
4.2 MAIN RESULTS AND ANALYSIS
To evaluate the performance of model, we conducted comprehensive tests comparing Aria with the baselines on benchmarks detailed in Section 4.1 As shown in Table T our agent demonstrates outstanding performance across all evaluations.
As shown in Table [ Aria demonstrates a significant advantage over all baselines on each bench- mark. However, Our GoT and reflection mechanisms require multiple LLM calls for each translation task within Aria. To ensure a fair comparison of efficiency, it is crucial to consider not only the suc- cess rate but also the computational cost, for which use the number of API calls per problem as the primary metric. As Goedel-V2 is the top-performing specialized model at a single pass, with results comparable to the Gemini-2.5-P baseline, we select it for a direct comparison of compu- tational budget against Aria. We first determined that Aria requires an average of 17.7 calls per problem on the FATE-X benchmark.
Based on this, we designed a series of experiments for Goedel-V2, ranging from pass@ 16 to @ 128. As shown in Table [ while Goedel-V2's compilation rate scales with the number of calls, its final accuracy remains lower than Aria's. s. Aria maintains higher final accuracy even when compared to Goedel-Vi V2 pass@ 128 (using more than 7x calls).
Most importantly, comparative analysis the Conjectures dataset reveals why Aria achieves its breakthrough performance. Through comprehensive case study of the generated codes, We identify distinct shortcomings in baseline models: large reasoning models tend to hallucinate incorrect inter- faces due to insufficient expert knowledge of Mathlib, while specialized formaizzessssss lack the mathematical reasoning power manage conjecture-level conceptual dependencies, as evidenced

---

Published as a conference paper at ICLR 2026
by their tendeney to simply replicate training data formats without true understanding of the un- derlying mathematical logic. Aria's architecture, integrating GoT and retrieval module on top of a strong reasoning model, successfully addresses both limitations. We provide case studies of formal- ized conjectures in Appendix for further illustration.
4.3
VALIDATION OF ARIASCORER
4.3.1
EXPERIMENTAL SETUP
We validated our semantic correctness checker against leading alternatives on the FATE-X bench- mark. The evaluation used the Aria agent's 's syntactically correct, nuto-formalized outputs. This benchmark contains complex mathematical statements and advanced definitions, providing rigor- ous test of semantic precision.
Ground truth dataset construction We create an expert-validated ground truth dataset by label- ing each formalization as "True" or "False" based on its mathematical fidelity. The annotations provided by an algebra Ph.D. candidate in pure mathematics and has also contributed to Mathlib, then independently verified by second expert with the same credentials. We then used this dataset to benchmark the performance of several semantic correctness checkers.
Baselines We benchmark AriaScorer against several established methods for checking semantic correctness. The first is LeanScorer (Xuejun et al., (202).. a method using decomposition and match- ing, which we re-implemented as its original version LeanScorer also serves as a critical ablation study for AriaScorer, representing our full pipeline but without the term-level grounding step. The second is Back Translation (Ying et al., 2024 Gao et al., 2024b), a widely-used pipeline that translates formal statement back to an informal one and uses an I.I. to judge the similarity. For a controlled comparison, AriaScorer, LeanScorer, and Back Transsaaaatioon are all built upon the same base model: Gemini-2.5-Prro. We also evaluate Gemini- 2.5-Pro's performance on this task directly. This comparison framework ensures that AriaScorer's accuracy improvements be attributed specifically to novel term-level analysis, rather than the underlying language model.
open-source. Our re-implementation of
Evaluation Metrics We evaluate performance using binary classification, where formalizations are labeled positive (correct) or negative (flawed). Performance is based on the counts of True Posi- tives (TP), True Negatives (TN), False Negatives (FN), and False Positives (FP). A False Positive, for instance, occurs when checker incorrectly approves a flawed formalization. These four outcomes then used calculate and report accuracy, precision, recall, and Fl score.
4.3.2 PERFORMANCE OF ARIASCORER
Table 2: Performance comparison of distinct semantic correctness checkers. It is carried out on the auto-formalized output of Aria FATE-X. The score threshold for binary decision is denoted a.
AriaScorer AriaScorer LeanScorer LeanScorer
Back
Gemini
(a = 0)
(o 0.9)
(a = 0)
(a 0.9)
Translation
50
42
44
TN
12
15
7
16
8
FP
5
2
14
10
1
9
FN
2
10
8
45
Accuracy
89.9%
82.6%
71.0%
73.9%
33.3%
76.8%
Precision
90.9%
95.5%
77.6%
81.5%
87.5%
83.3%
Recall 96.2%
80.8%
88.5%
84.6%
13.5%
86.5%
F1 93.5%
87.5%
82.1%
83.0%
23.3%
84.9%
AriaScorer is the porferrfnnnng model for semantic correctness checking on Aria's output from FATE-X. At threshold of it achieves the highest accuracy (89.9%), recall (96.2%), and Fl score (93,5%), significantly outperforming all baselines. Its superior precision and recall compared LeanScorer underscore the benefits of term-level grounding. Increasing the threshold to
8

---

Published as a conference paper at ICLR 2026
0.9 boosts AriaScorer's precision to peak of 95.5%. This demonstrates key trade-off: lower threshold more tolerant of mathematically equivalent forms, maximizing recall, while a higher threshold imposes stricter criteria, minimizing false positives for real-world deployment. In contrast, the Back Translation baseline, which demands an exact textual match, achieves very high precision but suffers from low overall recall. While we adopt the high-precision setting of a 0.9 in all other experiments, the results at a = 0 best demonstrate the fundamental advantage of our term-grounded approach.
4.3.3 KEY FINDINGS OF ARIASCORER
By incorporating term-level grounding, AriaScorer addresses common failure modes in semantic correctness checking. Our ablation study highlights three of its key strengths:
Implicit Semantic Inclusion By retrieving a formal term's 's full definition from Mathlib, AriaS- corer identifies any implicit preconditions or constraints contains. This uncovers crucial depen- dencies for accurate evaluation that purely textual comparisons would overlook. (See Appendix B.I..
Definition Discrepancy Detection AriaScorer detects subtle discrepancies between formal term's precise definition and the informal concept's intended meaning. By comparing the retrieved Mathlib definition against the original problem's 's context, it identifies when a Lean term, though textually similar, carries a different mathematical interpretation. (See Appendix B.2).
Hallucination Suppression via Grounding AriaScorer suppresses LLM hallucinations by grounding the evaluation process. Before invoking the LLM, it injects the authoritative Mathlib definitions of all formal terms into the prompt. This constrains the model reason based on verified ground truths, ensuring its output reflects the actual semantics of the formal code. (See Appendix
B.3
4.4 SUMMARY OF ABLATION STUDIES
We conduct a series of comprehensive ablation studies to quantify the unique contributions of Aria's core components: the Reflection mechanism, the Sruph-of-Thougee (GoT) planner, and the Setrieval-Augmentte Generation (RAG) module. Our findings, particularly on the challenging Con- jectures dataset, demonstrate that all three are indispensable.
Ablating the Reflection module, caused performance to collapse on both FATE-X and Con- jectures, proving its necessity for achieving correct codes.
Removing the GoT planner cripped the agent's 's ability to formalize novel concepts, reduc- ing successful conjectures from to 1. This highlights its critical role in imposing logical structure. Moreover, nounced on more challenging datasets.
found that the impact of ablating the GoT module is more pro-
Disabling the RAG module results in a complete 0% success rate on Conjectures, confirm- ing its crucial function in grounding the agent and preventing foundational hallucinations of non-existent concepts.
Detailed procedures and analysis are provided in Appendix
5 CONCLUSION
In this paper, we present Aria, statement auto-oormaiization agent integrating reureeedl-augmeenedd generation, graph-of-thought planning, and self-reflection mechanism. This integrated approach makes Aria the first agent capable of autonomously synthesizing the complex novel definitions re- quired to formalize high difficulty-evel mathematical statements such as conjectures. This capabil- ity directly addresses a core limitation of prior methods, which fail due to hallucination and logical errors when encountering unseen concepts. Moreover, presented novel semantic correctness checker, AriaScorer, that retrieves definitions from Mathlib for term-level grounding, enabling rig- orous and reliable verification.

---

Published as a conference paper at ICLR 2026
Our comprehensive experimental results demonstrate that agent achieves leading final accuracy on benchmarks of varying difficulty, from the undergraduate level to conjectures. This success is particularly pronounced the highly challenging Homological Conjectures dataset, where our agent achieves breakthrough performance.
Given that statement formalization is critical prerequisite for theorem proving, successful formalization of conjecture-level statements established a solid foundation for future work on auto- mated mathematical proof at this frontier of research.
ACKNOWLEDGEMENTS
This work is supported in part by National Key R&D Program of China grant 2024YFA1014000 Fundamental and Interdisciplinary Disciplines Breakthrough Plan of the Ministry of Education of China (UV22025XDXM1 13), the New Cornerstone Investigator Program, and Ubiquant.
Xintao Yu is supported by the "Qiushi Academic-Donglinge Project of Renmin University of China (No. RUC240SDL0155.
REFERENCES
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathemat- ics. arXiv preprint arXiv:2302.12233,, 2023.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre. Jean-Chin -hrristoie Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, 1999.
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang. Zhihong Wang. Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang. Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, and Thomas Hanwen Zhu. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving, August 2025. URL htth:://p/axiii org/ abs /205 23726 LrXiv:2507.23722 [cs].
Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4, 2024a.
wbw./osr///aaaaaaoooooo....sssea abs/24bs.3 113300131
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. arXiv preprint arXiv:2410.10875 2024b.
Google DeepMind. Gemini 2.5 pro. gemini/pro/] 2025.
Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, and Yang Liu. Formarl: Enhancing autoformal- ization with no labeled data. arXiv preprint trXiv:2508.1891 2025.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023.
Jiedong Jiang, Wanyi He, Yuefeng Wang. Guoxiong Gao, Peihao Wu, Bryan Dai, and Bin Dong. Introducing fate: A multi-level formal benchmark for frontier algebraic problems. https:// Frenzymath wttp//ooooo/aateeeeeeooeoeeooaee fate/ Aug 2025.
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge. Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goevel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025. URL https:
//w.xiv.org/aas////// 2508 03613
10

---

Published as a conference paper at ICLR 2026
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalizaton: Towards a faithful metric and a dependency retrieval based approach. In The Thirteenth International Conference Learning Representations, 2025a. URL https:
7 //openreviex ewweew.www........ net. formm??mm? hett:Foorrmmm10hhbb222222222
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. arXiv preprint arXiv:2502.055677 2025b.
Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. Process-driven autoformalization in lean 4. arXiv preprint ar arxiv:2406. 04440000444 01940, 2024.
Wangyue Lu, Lun Du, Sirui Li, Ke Weng, Haozhe Sun, Hengyu Liu, Minghe Yu, Tiancheng Zhang, and Ge Yu. Automated formalization via conceptual retrieval-augmented llms. arXiv preprint arXiv:2508. 06931, 2025.
The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference Certified Programs and Proofs, 2020.
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction - CADE 28, pp. 625-635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5.
Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization, 2024.
httthttss///zxiiia org/ Abs//310. 07957
Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-provers Advancing formal mathematical rea- soning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An context learning agent for formal theorem-proving. 2024.
2310.04353.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504. 11354, 2025.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of in- formal to formal mathematics. International Conference on Intelligent Computer Mathematics, pp. 255-270. Springer, 2018.
Wikipedia contributors. Homological conjectures in commutative algebra Wikipedia, the free encyclopedia.
http://ewwwwiiiiiieee..e ptt. cessed 22-5e).
logi 1_ conjectures in commutative alggbraaooldiie-122999122233333 2025. [Online; ac-
Yuhuai Wu, Albert Q Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformaliztionn with large language models, 2022. URL https:
12615
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi. Rui Zhang, Zidong Du, Jie Yan, and Xing Hu. CeepFun-Formalizee Unlocking the Autoformalization Potential of LLMs through Knowledge-Reessning Fusion, August 2025. URL lttp::t/axixi......// abs/2508. 04440 2XXv:2558.004400 [cs].
Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haox- iong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, et al. Mathesis: Towards formal theorem proving from natural languages. arXiv preprint arXiv:2506.070477 2025.
2025.

---

Published as a conference paper at ICLR 2026
Huaiyuan Ying, Zijian Wu, Yihan Geng. Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in 2024.
Neural Information Processing Systems,
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don't trust: Verify grounding Ilm quantitative reasoning with autoformalization, 2024. URL
https://arxiv org/ hwwgg/bb//2400 18120
Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang. Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang. Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, and Hang Li. Solving formal math problems by decomposi- tion and iterative reflection, 2025.
BRLhttps:: / /awxivv.vvv////////////a/////xi/ orq/ h/sp/ab////a / 2502.15255
12

---

Published as a conference paper at ICLR 2026
A CASE STUDY FOR ARIA'S GENERATED STATEMENTS
In this section, we present a qualitative analysis of Aria's generated statements through several representative case studies illustrate its strengths and limitations. For each case, we visualize the agent's 's conceptual dependency graph as a "blueprint"-a -a visualization style standard in the Lean community for representing dependencies-to illustrate its planning process. We then present the final formalization and compare against the outputs generated by the Goedel- 122-Formalizer-3 and Gemini-2.5-PP model for the same problem.
A.1 EXAMPLE 1: KOETHE'S CONJECTURE
INFORMAL STATEMENT
Let R be a ring. R has no non-zero nil ideal (two-sided), then it has no non-zero nil one-sided ideal (neither left right).
ideal
nilpotent elements
ring
one-sided ideal
nil ideal
koethe's_conjeee conjecture
Figure 3: Dependency Graph of Koethe's Conjecture
ARIA GENERATED STATEMENT
import Mathlib
universe u
/-- An ideal '1" is nil ideal if every element of "1" is nilpotent. -/ def ISNil {R Type u} [Semiring R] (I Ideal R) Prop
Y E I, IsNilpotent
/--
IE ring "R" has no nen-zero nil two-sided ideals, then it has no non-2ero nil
onc-sided idcals (neither left nor right).
-/
theorem ___ni__idell__imlles_eeo sol_lss____nnl_ee__seeeeee didd_eeeddddddlls {R Type u}
[Ring R]
V Ideal R), I8Ns1 -1-1-
(L Submodule RJ, x E L, IsNilpotent x) + ^
(J : Submodule (Mul0pposite B) R), (V x E J, IsNilpotent x) 4 J
1 :=
sorry
GOEDEL GENERATED STATEMENT
import Mathlib
import Aesop
set_option maxHeartbeats 0
13

---

Published as a conference paper at ICLR 2026
open BigOperators Real Nat Topology Rat
theorem statement (R : Type*) [Ring R]
(A I Ideal R, I * 1 + 3
E I, ~IsNilpotent x) 4
(A Ideal R, 1 * 1 +
E L, -IaNilpotent x) A
(V R Ideal R
E R, -IaNilpotent x) :- by sorry
GEMINI GENERATED STATEMENT
import Mathlib
variable (R Type*) [Ring R]
des noethe_conjectunee
Prop := (V (I Ideal R), IsNil - 1) -
(v (J Submodule R R) IsNil
J =) Av (K Submodule R R), IsNil K +
ANALYSIS
This example clearly reflects the architectural advantages of Aria both the specialized formal- ization model like Goedel and a powerful general reasoning model like Gemini.
Among the three outputs, Gemini's results successfully preserves the original mathematical intent, correctly identifying the need to distinguish between two-sided and one-sided ideals. However, fails to compile because it hallucinates a non-existent API (IsNi reflecting a disconnect between its strong high-level reasoning and its knowledge of the library's API.
In contrast, while Goedel's output compilable, is semantically incorrect. fails to cap- ture the non-trivial knowledge that one-sided ideals are represented by Submodule R R and Submodule (Mul0ppos iitssiteee ite R) R, and instead formalizes all ideals as Ideal R, which stands only for two-sided ideals, causing the formalization to deviate entirely from the original mathematical intent.
Aria's formalization is both syntactically and semantically correct. It uses the proper Mathlib types for the different ideals but also achieves good readability and modularity with a prerequisite formal definition for nilpotent ideals (def IsNil), This success highlights the core advantage of Aria" s GoT architecture. Its ability to perform high-level conceptual planning, while strictly grounding the formalization process in Mathlib, allows it to avoid both the API hallucinations of Gemini and the semantic errors Goedel.
A.2 EXAMPLE 2: EXISTENCE OF BALANCED BIG CONJECTURE
MODULES
INFORMAL STATEMENT
Let R be Noetherian commutative local ring with maximal ideal ma. There exists R-module W such that mgW # W and every system of parameters for R is regular sequence on W.
ARIA GENERATED STATEMENT
import Mathlib
/-- A ring "R" is a Noetherian local ring if it is both Noetherian and a local ring. -/ class IsNottherianniccllinng (R Type*) [CemrRing R]
extends IsNoetherianRing R, IsLocalRing Prop
Note: 'ringKrullDim" is already defined in Mathlib.
Note: 'Ideal. f is standard in Mathlib and its definition matches the one provided in the context.
14

---

Published as a conference paper at ICLR 2026
nocthrian_ring ring
krull dimension of a _a_ring
local ring
commutativve ring
neotherinn_ r_in
primary_ide ideal
regular soquence
system of parameters
nectherian commutative local ring
r-module
maximal idcal
rooL conjecture
Figure 4: Dependency Graph of Existence of Balanced Big Cohen-Macaulay Modules Conjecture
/--
In Noetherian local ring "R" of Krull dimensicn "d", "system of parameters" a sequence of "d" elements "X1, Xn in the maximal ideal "m" such that the ideal
-I- <X1x .... X,>" generated by these elements is "m'-maiaary (f.e., it is a primary ideal
whose radical the maximal ideal "m").
-/
de IsSystemOffarameters IR Type*) [CommRing R] [IsNottherlanLooalRingg R]
N) (x Fin R) Prop : ringKrullDim
fd (V 1, x i E www.lliiin.maxmmaal...
R) A
(let I : Ideal. span (Set. range x);
I. IsPrimiyyy I.radical LocalRing maximalldesl
/--
Let R be Noetherian commutative local zing with maximal ideal ma. There exists R-module W such that mnW o W and every system of parameters
for R is regular ar sequence on W.
-/
theorem exists exists_module where where_systen of parameters is regular reqular_sequence sequence
Type*) [CommRing [ISlettheriannocelRing R] :
(W : Type*) (_ AddCommGzoup W) (_ Module R W),
R) (T Submodulc R W) # T A
A (d N) (x Fin d + R), IssystemofParameters d RingtheerrySequencce IsRegular (List.ofFn := by sorry
GOEDEL GENERATED STATEMENT
import Mathlib
import Aesop
set_option maxleaarbbaats 0
open Big0perators Real Nat Topology Rat theorem statement (R : Type*) [CommRing R] [IsLocalRing R]
[IsNostherianRing R]
3 (M Type*) [AddComnGroup W] [Module R W),
(maximalIdeal R Ideal R) * w
(s R), s.Finite Ideal.span s maximalIdeal R + A (f + W), (V E s, # 0) + Linear Independent
f = by sorry
GEMINI GENERATED STATEMENT
15

---

Published as a conference paper at ICLR 2026
import Mathlib
open Localking
The proposition defined within "variable" block, which sets the context for the ring R. variable (R Type*) [ComnRing R] [INNoetherianRing R] [LocalRing R]
/--
Formalization the statement:
"There exists an R-module such that MLR W o W and every system of parameters for is a regular sequence en W."
-/
def module_with setprch__egaaaap_eeeeeee sop_spissssssssooeeeee Prop "There exists an R-module W..."
3 (w Type*) [AddCommGroup W] [Module R W), -- such that R_ R * W..."
(maximalIdeal R) (T SubmaduleRW) Atop A
and every system of parameters for R..."
{s : Fin (Ring. R) + (maximalIdea) R) }
[IsSystemOfParameten s) +
.s..is regular sequence on R. (IsRegularSequenc) (fun (s i R))
ANALYSIS
This is more complex conjecture, and the three generated examples once again highlight the poor performance of a specialized model like Goedel in capturing complex mathematical semantics, as well as the knowledge gaps of general reasoning model like Gemini regarding the Mathlib library.
In this instance, Gemini uses a definition LsSystemofParaaae exist in the library. And for concept of regular sequence, which avail- Seeerhhorr..equueeeeee
which does not
able in Mathlib (IsRegu sequencc)). Goedel, on the other hand, failed entirely to grasp the concepts of "regular sequence" and "system of parameters", producing completely erroneous statement.
Tsregular), it used an incorrect interface
contrast, Aria's Graph-of-Thought (GoT) architecture helped correctly identify the key con- cepts. It successfully searched within Mathlib to find SiinTheeory.Seeuencee IsRegul ar. By leveraging the deconstruct capabilities GoT, Aria successfully formalize the definition for system of parameters, and ultimately succeeded in formalizing the entire conjecture.
B DISCUSSION AND CASE STUDY FOR ARIASCORER
By grounding evaluation in retrieved Lean term information, our checker captures the precise seman- ties of formal statements with greater accuracy. improving both matching and evaluation quality. In the following section, we present examples showing how three key innovations contribute the enhanced performance of AriaScorer.
B. IMPLICIT SEMANTIC INCLUSION
INFORMAL STATEMENT
y, 2/r.y,2//2²² + n² + +27 is UFD.
CONDITIONS AND CONCLUSIONS
Condition:
1. Let R be the ring R = Clæ, v. 2l/2222 + + +2²).
Conclusion:
16

---

Published as a conference paper at ICLR 2026
R is Unique Factorization Domain (UFD). This means:
1. R is integral domain (a commutative ring with 1 & 0 and zero divisors).
2. For every non-zero, non non-umit element E R, there exist irreducible elements
P1. ....P-..-PP R such that P1P2 :. Pk-
3. This factorization unique: if 9142 ... Jm another factorization into irreducibles, then m and there exists permutation of [1, 2. k) and units U U2 E R such that p. = ux)o(1) for all i E (1,2,.., k).
FORMAL STATEMENT TRANSLATED BY ARIA
import Mathlib
state that the quotient ring is UFD, Lean must first know it's an integral doma in.
This requires the ideal to prime. The error lunknown constant indicates that the
function name
iff isDomain iesteaiin.uuoieentt used in the previous attempt does not exist.
The correct mathiib theorem 'Ideal. Quotient. ietiiinnttsDominnn isDomain iff prime", which states
"IsDomain (R / I) + I. I.IsPrime', To prove the 'IsDomain' instance from the primality of the ideal, we need the reverse direction of this equivalence, which is accessed with '.mpr".
The 'noncomputable" keyword is required because types like "MvPolynomial" over 'C' are defined using classical logic and do not have an executable implementation.
noncomputable def kleinianSingulariinn
Ideal (MuPolynomial (Pin
C) :-
span {
(MsPolynomial.X 0 NvPolynomial (Fin 3) C)
(MrPolynomial.X 1)^3 +
(NrPolynomial.X 2)*7
Ne define an abbreviation for the quotient zing type for clarity, abbrev CxyzMocKleinian MrPolynomial (Fin C
KleimianSingularityyldell
We manually provide the 'IsDomain' instance for our quotient ring. Its proof follows from the fact that the ideal is prime, non-trivial result which we assume with "sorry". local instance Islemmain cxyzModkleinian :-
(Ideal.Quotien iuuotient....... awtomain_iff_oriiiie kleinians, hwwniinnulrityydeee. .pr sorry
xyd_mod theorem isUFD C xyz mod x2 y3_z7
www.uuaaactoiiiaiioooooo.o CxyzMoaKleinian := by sorry
RETRIEVED LEAN TERMS
('name': ('MrPolyncmial)) ], 'kind'; 'definition', 'value': "Type u_l + (R Type 2_2) [inst : Commsemiring R] + Type (max u_l u_2)', 'informal_name" 'Multivariate polynomials over R with variables in a', nnnformal_deerippiion
'The type of multivariate polynomials over a commutative semiring R with variables indexed by a type d. Each polynemial is a finite fornal linear combination of mononials, where monomial is product of variables X, for iEa a raised to non-negative integer powers, with coefficients R.
17

---

Published as a conference paper at ICLR 2026
I'name:: I'Ideal', 'span'l, 'kind': 'definition', 'value': '[a Type + linst Semiring al + set Ideal a', 'informal_name' Iddall generated by a subset', "informa__dscriptioot subset 8 of semiring a, the ideal span(s) is the smallest ideal of containing 8, defined as the intersection of all ideals containing 8.
'Given
MATCHING AND ASSESSMENT BY ARTASCORER
LLM Full Output: Let's compare the mathematical conditions and conclusions with the Lean 4 formal statement one by one:
1. Let be the ring C(z, y, 2)= yy² +
Math: The object of study is a quotient ring- The base ring is the ring of polynomi- als three variables 2, y, 2 with complex coefficients, C(z, y, 2]. The ideal the principal ideal generated by the polynomial x² + +
MvPolynomial (Fin C Lean: abbrev CxyzModKleinian This defines the ring as a quotient / kleinianSingun hegiirianSggullaittyydeea
The base ring MvPolynomial (Fin 3) C, which represents multivari- ate polynomials with coefficients in C (complex numbers) and variables in- dexed by Fin 3 (a type with elements, corresponding to T, T, =). The ideal Aeeiiianniinulaiityyy..
is defined Ideal.apor of the set con- taining the polynomial (MvPolynomial X 0) 2 [NvPolynomis 1. 1)^3 CivPolynomial. 2) ^7, which corresponds exactly to x² +2? Match: Perfectly match.
2. R is Unique Factorization Domain (UFD):
Math: The ring R is an integral domain, and every non-zero, non-unit element has unique factorization into irreducible elements (up to order and multiplication by units).
Lean: The conclusion formalized in two parts. First, local inst ance IsDomain CxyzModKleinial asserts that the ring is integral domain. Second, the main theorem theorem onmonoid Un Uni queFactorizattttt inn.ooroiooooooooioid CxyzModKlei in asserts the property
of unique factorization. In Mathlib, a ring is UFD if and only if it satisfies both
IsDomain and Uni wuw.aaattorizaaiinooo..... Match: Perfectly match.
Check for missing conditions/ / implicit conditions:
The mathematical statement "R is UFD" contains the implicit condition that R must be an integral domain. The Lean code makes this explicit with the local i instance : IsDomain CxyzModK wenini an. This is missing condi- tion but a correct formalization of an implicit part of the mathematical definition.
Match: Perfectly match.
ANALYSIS
In this case, the informal statement asserts that the quotient ring R = C[r,, 2// + + + 27) Unique Factorization Domain (UFD), which requires R to be an integral domain by def- inition. AriaScorer, empowered by term-level retrieval, correctly accesses the definitions of relevant Lean terms and tracks newly written local instances. This allows it to recognize that the concept of UFD is semantically realized through the combination of IsDomain and UniqueTactorizatioo innMonnoii even though they appear separately the formal code.
Without this term-level semantic grounding, checker may mistakenly treat the newly defined local instance as a nontrivial addition to the conclusion, rather than recognizing as a prerequisite im- plicitly embedded in the definition of uniqeFactorri aattoiiitttiiiiiccaacciicaiaaaat inntoonoooi By contrast, AriaScorer uncovers this internal dependency and correctly matches the formalization. This case illustrates the strength of semantic grounding: it enables the checker move beyond surface forms and reason
18

---

Published as a conference paper at ICLR 2026
about the structural meaning and interrelation of formal terms something that purely textual com- parison would fail to capture.
B.2 DEFINITION DISCREPANCY DETECTION
INFORMAL STATEMENT
Let A, B E QK be rational numbers. Consider the quaternion ring DA.B.E = {a bi + oj + dk a, b, e, d E ] which the multiplication satisfies relations: 1² A, "² B, and ij = jj k. Show that DAB either isomorphic H. (Hamilton quaternion) isomorphic to Matex2 (R) as R-algebras.
CONDITIONS AND CONCLUSIONS
Conditions:
1. A, B QK (i.e., A and B are non-zero rational numbers).
2. DA.B. an R-algebra defined on the set {a bi + cj + dk a, a.b, e R}.
3. The multiplication in DA, is defined by the relations:
22
j = B
ij --
ji
Conclusion:
DA, is isomorphic to H. (the Hamilton quaternions) or isomorphic to M1(2x2(1R) (the algebra of 2 real matrices) as R-algebras. This can be stated as: (Da,B.R H) V (DA,B.R (R)) where _ denotes an isomorphism of R-algebras.
FORMAL STATEMENT TRANSLATED BY ARIA
import Mathlib
theorem
(A : Q) (hA A # 0) (hB B * 0) :
Nonempty (QuaternicnAlgeber (quaternionAleebr)
R (A : R) (B R) [RR]
R (-1) (-1) 1)) V
Nonempty (QuatermionAlgebra R (A R)
=x [R] Matrix (Fin
2) (Fin 2) R) := by sorry
RETRIEVED LEAN TERMS
I'name:: ['Matrix'), 'kind'; 'definition', 'value': "Type Type u' Type Type (max u² v)", "informal_namee 'Matrix', "The type of matrices with rows indexed by a type m, columns indexed by a type n, and entries in type a. A matrix M can be represented as a function M n a, where M(i.)) gives the entry in row i and column j.') d'name': ['Ouatermionnlgebaa]]]
"informal_description
'kind'; 'structure', 'value': '(R Type u_l, 'informal_name' 'Quaternion 'The structure representing a
Type u_l) + - Algebra', Inforral_descrippt quaternion algebra over connutative ring R with fixed coefficients a, where the elements are of the form + + + + wk
with 2,V,2,W and the multiplication rules are determined by == bi and =c The structure has four components: the real part "re" and three imaginary parts "imI', "imJ', "inK"."
MATCHING AND ASSESSMENT BY ARIA'S SEMANCTIC CHECKER
19

---

Published as a conference paper at ICLR 2026
Let's compare the mathematical conditions and conclusions with the Lean 4 formal statement one by one:
1. A, B E Q (i.e., and B are non-zero rational numbers).:
Math: A, A
Lean: (A B Q) (hA A x (hB + 0).
Match: Perfectly match.
2. DA, is an R-algebra defined on the set {a + bē + cj + dk a, ba,,,,,d R).
Math: The algebra is defined on the set of elements of the form + bi cj + dk with real coefficients.
Lean: Quater
onAlgebra R : R) According to the provided Mathlib entry for Quaterni onA wawooonnllslsa.. gebra, the elements
R) 1.
are of the form x + yi 2 wk where x, y, 2, are from the base ring R. which is R in this case. This matches the form of the elements.
Match: Perfectly match.
3. The multiplication DA,B. is defined by the relations: 8² = =A = and
ij --j-- k.:
Math: The multiplication rules are 1² = A j B.
Lean: The multiplication is determined by QuatermionAlgebra R (A RR (B R) 1.
R a b c has multiplication rules 1 a bi and j c. For the Lean statement, is R, is (A R). b is (B IR), and c is 1. This implies the rules are i A + Bi and j 1. These rules do not match the mathematical rules. Match: Major inconsistency.
According to the provided Mathlib entry, QuaternionAlgebr
4. DA,B,R is isomorphic to H (the Hamilton quaternions) isomorphic to Mat2x2 (R) (the algebra of 2x2 real matrices) as R-algebras.:
Math: (DA,BR = HI) V (DA,BR Matex2 (R)).
Lean: Nonempty @QuaternionAlgebra E (A : R) (B R)
=a [RR] (QuaternionAleebrr. R (-1) (-1)
1)) V Nonempty
CobaternicnAlgenen
(A R) ( R) =a [R] Matrix
(Fin 2) (Fin 2) R)
The conclusion in Lean concerns the algebra QuaternionAlgete
R (A
R) (B R) 1. which, as established in point 3, is not the same DA,BR- Furthermore, the Hamilton quaternions (HH), defined by 12 -1, -1, are rep- resented in Lean as Quaterni eeteiiinnnggbbrrr the provided documentation, this corresponds and j = 1. which is not H. While the representation of Matex2 (R) as Mat rix (Fin 2) (Fin 2) F is correct, the overall statement is about different alge- braic structures than those the mathematical problem. Match: Major inconsistency.
(-1) (-1) 1. According to algebra with rules i -
Check for missing conditions /implicit conditions:
No missing conditions / implicit conditions
Match: Perfectly match.
ANALYSIS
In this case, the informal statement introduces DA,B.R with multiplication rules: 12 = A, and ij = -ji k. However, the corresponding Lean term actually has completely different rules:i² A Bi = 1. These differences are not perceptible by surface text comparison, Both the informal and formal version use A and B, and have similar algebra structure. By term- level grounding, AriaChecker gets the explicit retrieval of the definition of QuaternionAle gebra, making the semantic incorrectness obvious to AriaScorer. While LeanScorer is deceived by apparent textual similarity and misjudges this case, AriaScorer correctly flags as "Major Inconsistency". This demonstrates that Defintion Discrepancy Detection enables AriaScorer to distinguish semantic
20

---

Published as a conference paper at ICLR 2026
incorrectness, ensuring that the formal statement aligns with the formal statement in mathematical intent.
B.3 HALLUCINATION SUPPRESSION VIA GROUNDING
INFORMAL STATEMENT
Let (2 v (2 v3) and consider the extension E (a)). Show that Gal(E/Q) Qs, the quaternion group of order 8.
CONDITIONS AND CONCLUSIONS
Conditions:
1. a V (2 (3) v3)
2. E = (a) (E is the smallest field containing both Q and ox)
Conclusion:
The Galois group of the extension E over Q is isomorphic the quaternion group
Qs. In mathematical notation: Gal(E/Qu Qs. where:
Gal(E/QQ :o: E is field automorphism and Va Qz)(z)=
x} Qs (, x² 1, ry x 11 is the quaternion group of order 8.
FORMAL STATEMENT TRANSLATED BY ARTA
import Mathlib
open Polynomial
/--
Let a= -2+ (2) (3+ V3). The field == Q(a) is Galois
extension of Q, and its Galois group is isomorphic to the quaternion group Qs. Nonempty (P.Gal ex QuaternionGroup 1) :
sorry
RETRIEVED LEAN TERMS
('name': I'IntermediateFieldd 'adjoin'), 'kind'; 'definition',
'value': (F Type u_l) +\n [inst Field F] (E Type u_2) + [inst_1 Field E] [inst_2 Algebra El Set IntermediateFleld F E', innforma_aamee 'Field adjunction of set S to F', 'informal_descrreeee and subset $ SÇE, the structure attermediateFFeelddaaaa represents the intermediate field obtained by adjoining the elements hedral group; when n= it iscrorphic a cyclic group of order 4.')
'Given a field extension E of F
s'
''name:: ('Polynomial'), 'kind': 'structure', 'value': '( : Type u_l) [inst : Semiring R] + Type u_l', 'informal name": 'Univariste polynomials over semiring', "informal infformal_descrpptionn structure "Polynomial
'The
represents the type univariate polynomials over a semiring 'R", denoted as "R[X]", Polynomials are constructed using the variabie "x" and constant embedding "c" from "R", forming a semiring structure.";
MATCHING AND ASSESSMENT ARIA'S SEMANCTIC CHECKER
21

---

Published as a conference paper at ICLR 2026
Let's compare the mathematical conditions and conclusions with the Lean 4 formal statement one by one:
1. Condition:
V +2)+++++++
Math: a is defined constructively by the given formula, which specifies a par- ticular (positive real) number.
Lean: let P [X] :- x 24 * X 144 X
rootSet P.splittingFiele This does not define using the sgrt formula. Instead, it posits the existence an element that is a root of specific polynomial P. While the minimal polynomial of the mathematical
288 * X 144 and
the formal statement is about any root of P, not the specific one in the math problem.
Match: Minor Inconsistency.
2. Condition: E = Q(a) (E is the smallest field containing both Q and a)::
Math: E is defined as the field extension Q(a). The problem then asks to com- pute the Galois group of this extension, which implicitly assumes or requires that E/Q is a Galois extension.
Lean: Int rentertedeteeedddd adjoin Q {a) T. The Intermediate ee ield. adjoin Q {a} corresponds to Q (a). The term (top) refers to the ambient field, which is P P.splittinggieeee Thus, the statement asserts that Q (a) is the splitting field of P. This makes the implicit mathematical assumption that E/Q Galois into an explicit and strong condi- tion within the theorem.
Match: Minor Inconsistency.
2. Conclusion:
Gal(E/Q) Qs:
The Galois group of the extension E over Q is isomorphic Qs the quaternion group of order 8.
Math:
QuaternionGroup 1). G. cor- responds to Gal (E/Q). Nonempty (G ~* H) means G is isomorphic H. However, QuaternicnGroup
Lean: Nonempty (P. Ga.l
the generalized quaternion group with n-1, which is isomorphic to the cyclic group of order (C_4). The quaternion group order 8, Q_a, corresponds QuaternienGroup 2. Match: Major Inconsistency.
Check for missing conditions/ /mplicii conditions:
The Lean statement introduces the explicit definition of the polynomial P, which is not present in the original mathematical problem statement but is necessary intermediate result for its proof. This is an added condition. No conditions are missing.
Match: Minor Inconsistency.
MISJUDGMENT WHEN TERM-LEVEI GROUNDING IS ELIMINATED
Let's compare the mathematical conditions and conclusions with the Lean formal statement one by one:
1. Definition of a::
Math:
= (2 (2) + v3). This defines a as a specific positive real
number.
LLean:
let P Q[X] := x 24 * x 144 * X rootSet P
288 X 144 and
This implicitly defines a as an arbitrary root of the given polynomial
22

---

Published as a conference paper at ICLR 2026
(which is the minimal polynomial of the mathematical ().. This is shift from a concrete definition an abstract algebraic one.
Match: Minor Inconsistency.
2. Definition of the field E:
Math: = Q(a). The field is defined by adjoining the specific number a to
Q. That this field is Galois extension over is substantial part of the proof.
Lean: The ambient field P P.Sp1 ww..ppittiii. aappittinngiiin iellielld d, the splitting field of the polynomial P. The condition Inte
adjoin Q {a)
states that this splitting field is generated by single root a. This reframes the definition the field: the problem is set in the splitting field of and of the goals is to show it can be generated by single root.
Match: Minor Inconsistency.
3. The groups being compared:
Gal(E/Q) (the Galois group of the extension E over Q) and Qa (the quaternion group).
Math:
Lean: Gal and QuaternionGroup 1. P. Gal is the Galois group of P ..pplittingiie over Q, which corresponds to Gal(E/Q). The doc- string and context imply QuaternionGroup 1 is the name used for Qs. Match: Perfectly match.
4. Conclusion:
Math: Gal(E/Q) = Qs, i.e., the Galois group is isomorphic to the quaternion group.
Lean: Nonempty (P.Gal Gal QuaternionCroup 1). This
states that there exists group isomorphism between G.Gal and QuaternicnGroup
The Nonempty wrapper is standard way in Lean to express existence in proposition.
Match: Perfectly match.
Check for missing conditions/ implicit conditions:
The mathematical problem requires implicitly that one finds the minimal poly- nomial of and proves that the extension Q(a/Q is Galois (i.e., is the split- ting field of this polynomial). The Lean statement makes these aspects ex- plicit by providing the polynomial tion Intermen wntteremdaaeeFie fiedd.ld... adjoin Q {a) T (that Q(a) is the splitting field) as part of the theorem to be proven. The formal statement more explicit, which a feature of formalization, not missing condition.
from the start and including the condi-
Match: Perfectly match.
ANALYSIS
In this case, the Lean statement claims isomorphism Nonempty (P GPl 2= QuaternicnGroup 1), using the key Lean term QuaternionGre assume that QuaternionGrout QuaternicnGroun 1 is isomorphic to the cyclic group Ca, while the actual representation of Qs is Quaterni onGroup 2. This subtle but important distinction overlooked when LLM gives the checking purely on surface texts. In the setting without the information of Lean terms, checker is misled by the hallucination of LLM and gives a wrong judgment. In comparison, AriaScorer grounds the checking pipeline in concrete semantics. With the usage of the definition of Quatern. QuaternionGroup onGroup n, AriaScorer correctly flags the statement as "Major Inconsistency", which is in line with human annotation. It gives example of how the process of hallucination suppression constrains the LLM's s reasoning within Lean terms, guarantces precision in the semantic correctness checking.
1. It is easily to refers the quaternion group of order Qs. Actually,
23

---

Published as a conference paper at ICLR 2026
B.4 VERIFICATION STRATEGY AND ERROR PROPAGATION ANALYSIS
B.4.1 VERIFICATION STRATEGY
A critical architectural decision in our system is the application of AriaScorer exclusively ter- minal evaluator rather than an iterative feedback signal. This design is driven by a strategic trade-off between verification rigor, algorithmic stability, and computational efficiency. AriaScorer is engi- neered to function as a rigorous, independent checker involving multiple LLM calls and database searches. Consequently, it is computationally expensive and best suited for validating the quality of the completed solution.
Our preliminary experiments with iterative semantic feedback revealed two primary challenges:
Correcting semantic issues at intermediate steps frequently disrupted the syn- tactic structure the proof, leading to oscillatory behavior where the system toggled be- tween semantic and syntactic errors.
Instability:
Inference Efficiency:
Given the computational intensity of AriaScorer, applying it every intermediate node would drastically increase the total inference time. This inefficiency is further compounded by the aforementioned oscillatory behavior.
Furthermore, utilizing AriaScorer feedback signal for reflection-in addition to its role as the final checker-introduces a risk of self-referential bias, where the formalizer might learn to overfit the scorer's specific preferences rather than producing universally correct proofs.
B.4.2 ANALYSIS OF SEMANTIC ERROR PROPAGATION
We specifically investigated the risk of semantic error propagation, where an incorrect intermedi- ate definition might lead to a finalized but flawed proof. Our empirical data suggests that errors caused by "correctly typed but semantically wrong" intermediate definitions are statistically rare. A root cause analysis of failure cases in the FATE-X dataset revealed that only single instance of failure was attributable to a flaw in definition synthesis that propagated to cause final semantic inconsistency.
To demonstrate the rigor of AriaScorer in detecting such rare propagation cases, we present detailed analysis of the "Catenary Ring" instance. In this case, the generator synthesized a definition for PatenaryRing that was syntactically valid but mathemati- cally overly restrictive compared the standard definition.
Case Study: The Catenary Ring
import Mathlib
universe u
/--
ring "R" is catenary ring if it commutative Noctherian ring, and for any two prime ideals "p" and "q" with "p C q', all saturated chains of prime ideals between
"p" and have the
length.
The Length of a finite chain of prime ideals "po C Pt C ... C p. is "n", This corresponds
to the chain having "n+1" elements. Thus, two chains have the same length if and only
is they have the same number of elements (cardinality).
-/
class CatenaryRing (R Type u) [CommRing R] extends IsNoetherrianRing R Prop where
/--
For any two prime ideals "p, q" with "p S q", all saturated (i.e. maximal) chains
of prime ideals 1s in the interval Set Icc p q" have the same cardinality.
24

---

Published as a conference paper at ICLR 2026
eq egLsauraatcc_hhhhn_leggggh
(p q arimeSpectrum R), p 1 a
A (C1 02 Set (Sct.Ice Icc q)), IsMaxChain {. S +)
IsMaxChain S +) 02
Set.ncard c1 net.dcard C2
/--
Noetherian Unique Factorization Domain Krull dimension most catenary.
-/
theorem af
(A Type u) [CommRing A] [IsDemain A] [IsNoetherianRing A] wmniipeePttoriiaaiionoooeoe A]
(h_dim Order kruliDim (PrimeSpectrum A) S 3)
CatenaryRing A ==
sorry
Below the analysis of AriaScorer:
is catenary ring+*:
Math: is catenary ring, i.e., for any two prime ideals P;Q of with PCQ, any two saturated chains of prime ideals between and Q have the same length.
Lean: "CatenaryRing A' The provided "class CatenaryRing" definition
extends IsNoetherianRing R', which means that to be "CatenaryRing', a ring must be Noetherian in addition to satisfying the chain condition. The mathenatical definition provided does not require the ring to be Noctherian. This makes the Lean conclusion stronger than the mathematical one.
Match: Major inconsistency.
Even though the specific problem context (Theorem ufd_of I Meatteeeeehreeeeeeeeeeee is i catenary) explicitly included the Noetherian ring condition (IIsostherianninng Al), AriaScorer cor- rectly identified that the definition itself hallucinated an unnecessary inheritance (extends tsNoether rinnning).. This demonstrates that AriaScorer maintains rigorous judgment even when the propagated error is subtle and contextually masked.
B.4.3 FUTURE OUTLOOK
While the current dependency graphs in FATE-X are relatively shallow (averaging 2-3 layers), min- imizing the impact of error propagation, this challenge may become more pronounced in large-scale formalization tasks, such as formalizing entire textbooks. Future work may aim efficiently inte- grate semantic signals into larger systems by adopting strategic checkpointing (e.g., verifying every layers) to balance efficiency and correctness.
B.5 LIMITATIONS OF SYNTACTIC METRICS IN RESEARCH-LEVER MATHEMATICS
potential concern in using a LLM-based evaluator is the risk of self-referential bias. We address this by adhering to a strict architectural decoupling: AriaScorer is utilized solely as post-hoc evaluator and is never exposed to the agent during generation or reflection. This ensures that the observed performance gains reflect genuine capabilities rather than optimization towards the metric. Furthermore, the reliability of AriaScorer has been validated against human expert annotations on the FATE-X and Conjecture datasets, achieving a 95.5% alignment rate.
B.5.1 WHY SYNTACTIC METRICS ARE LIMITED.
While syntactic metries such as BEq simple type-checking standard for simple formaliza- tion tasks, we find them ill-suited for research-level mathematics. At this level, proving logical equivalence between synthesized definition and reference statement is often non-trivial. Stan-
25

---

Published as a conference paper at ICLR 2026
dard syntactic matchers frequently generate false negatives due to several intrinsic complexities of formal libraries:
1. Multiple Mathematical Definitions: A single concept often has multiple equivalent math- ematical definitions. Different contexts (or authors) may prefer different formulations, leading to distinct structures or type classes in Lean.
2. Bundled Type Classes: Structures can be "bundled" differently. For example, wwo-variable polynomial ring be formalized as MvPolynomt (Fin 2) or Polynomial al "Polynomial al R). These are not definitionally equal; proving their equivalence requires constructing complex algebraic isomorphism (= [R)).
3. Inheritance Structures (Diamonds):
Type classes inherit from others. Different inheri- tance paths can lead to "diamond" problems where the formal representations diverge de- spite tepresenting the same object. This issue acute in framework: the Graph of Thoughts (GoT) planner synthesizes deeply structured, multi-layer definition chains. This structured approach naturally induces diamond patterns.
B.5.2 CASE STUDY: THE ES KLEINIAN SINGULARITY.
To illustrate why syntactic metrics fail in this domain, we present specific case from the FATE-X dataset regarding the E8 Kleinian Singularity.
--Aria Generated Code:
import Mathlib
noncomputable def kleinian wttp::inngngaatt___opooooool
KvPolynomial (Fin
3) C :- (MvPolyncmial. 0)
(MvPolynemial. x 1) 3 (MVPolynomial.x 2)
abbrev F8
:-
(MvFolyncmial (Fin 3) C) (Ideal.spar
(kleinian wtt.:/ssuuuarrttt___l.oooom
instance kleinian kleiniannssiguuuiaaaaaeeeae wwwgularityyyee......... ideal isPrime :
(Ideal.span [iceniiiiiiiipllarrrrrgaasoooooo
Isprime by sorry
theorem isUrD_e8_ hetpp_sssaiiuuuuutttoooooooooot. uniqueFactorrkkationnnee B
B__singlaartty_uutteenntt.. : by sorry
--Reference Code:
import Mathlib
/--
The ring R Clæ, u, 2x/(x² y +27). -/
abbrev : Type :- (MvPolynomial (Fin 3) / Ideal.spar (.X 0 .x
1 3 + x 2 7 MvPolynomial (Fin 3) )
/--
Cla,y, 2) + + x is a UFD.
-/
theorem quet puctienn_not__ue
E (h IsDomain R)
(Uniqueractorization inmoonoooi R) by sorry
Both theorems assert the same fact: the coordinate ring of the E8 singularity is Unique Factoriza- tion Domain (UFD).
To formally prove that these two statements are equivalent in Lean (and thus satisfy a strict checker, e.g. BEq), would need to perform three non-trivial steps:
Ring Identification: Prove E8 E8_sit www.innngiiit.... wetitty__ooieett_tteee unfolding the definitions, returning to the quotient construction, and applying rewrite tac- ties.
This requires
Domain Verification: Prove that R is integral domain. This follows from the aesininnnsingulrlle ieeiet______eeeeeeee_e_eeeeeeee_ ideal, isprisii sirrimme instance, but requires a non-trivial proof step.
26

---

Published as a conference paper at ICLR 2026
Logical Elimination:
Prove the lemma ( (n IsDomain R) UniqueFactorl zat ionMonoid R)
Uni.ueeFactorizatiooooooo R.
This involves existential elimination logic.
Bridging this gap requires unfolding 4-5 technical layers and employing intermediate-level Lean tactics. BBq, which operates structural equality, cannot perform this semantic reasoning. Conse- quently, we maintain that AriaScorer represents a necessary, reliable, and unbiased standard for this domain.
C ABLATION STUDIES
To quantify the individual contributions of the core components within our Aria agent, conducted a series of comprehensive ablation studies. We systematically disabled the Reflection, Graph-of- Thought (GoT), and Retrieval- -egmeeval-Augmented Generation (RAG) modules measure their impact on the performance. All experiments were conducted on the challenging henchmarks FATE-X and homological conjectures, with the results presented TableBaand and Table 4
Table 3: Ablation study results on the Conjectures dataset. Performance drops significantly as key components of Aria are removed, highlighting their individual contributions. All values are success rates (%).
Configuration
Final acc.
Aria (Full System)
42.9
Ablations of Aria:
without Reflection
without GoT
without RAG
Baseline (Gemini)
Table 4: Ablation study results the FATE-X benchmark. All values are success rates (%).
Configuration
Compiler
Final acc.
Aria (Full System)
69.0
44.0
Ablations of Aria:
without Reflection
19.0
without GoT
69.0
38.0
without RAG
61.0
43.0
Baseline (Gemini)
27.0
21.0
C.I ABLATING THE REFLECTION MECHANISM
This study designed to quantify the contribution of our agent's core iterative self-correction mech- anism. In the full Aria agent, each generation step (for both prerequisite definitions and the final theorem) is embedded in a refinement loop that allows for 16 reflection attempts. Within this loop, the agent generates candidate formal definition or statement and receives feedback from the com- piler, and uses this feedback to inform the next generation attempt.
For ablation, we disable the refinement loop entirely, restricting the agent to a single generation attempt at each stage.
As shown in Table ablating the reflection module causes the final accuracy FATE-X to drop from 44% to 14% and the compilation success rate from 69% 19%, even lower than that of baseline. This dramatic performance decrease is also observed on the Conjectures dataset, where the success rate plummet from 42.9% to 0%. The result indicates that a single generation is often insufficient for both capturing the semantic nuances and the syntactic rigor of complex mathemat- ical statements. Therefore, we conclude that the Reflection module a crucial part in our agent's architecture.
27

---

71.0 Published as a conference paper at ICLR 2026
C.2 ABLATING THE GOT PLANNER
The experimental setup for this ablation is as follows: first, we extract a flat list of conceptual key- words from the original informal statement. Then, for each concept in this list, use LeanSearch to retrieve it in Mathlib. In contrast to the full system, this process does not perform any further recursive decomposition, regardless of the search outcome. The agent then directly synthesizes the final formal statement only using the results from this search.
Quantitative Analysis. As shown Table 3 the impact of GoT scales with problem difficulty. On the challenging Conjectures dataset, the full Aria system successfully formalized 6 of the 14 conjectures, whereas the version without GoT only managed 1. Similarly, on the FATE-X bench- mark (Table 4. removing GoT causes the final accuracy drop from 44.0% 38.0%, although the compilation success rate remains constant at 69.0%.
However, Table 5 reveals counter- innuutr- phenomenon the simpler FATE-H dataset: the ab- lated agent achieves a higher compilation success rate (95% vs. 89%) but significantly lower final accuracy (54% vs. 71%).
The Trade-off between Syntactic Risk and Semantic Rigor. We attribute the "high compilation, low accuracy" anomaly on FATE-H to a strategic trade-off. The GoT planner prioritizes semantic ex- plicitness by forcing the generation of all necessary intermediate definitions (e.g., explicitly defining extended fields or tensor products as separate structures). While this ensures semantic consistency, it significantly increases the total attack surface for syntactic errors. For instance, the modular style introduces complexities global namespace management and Lean's 's type class resolution where instances of equivalent but distinct definitions often fail to interoperate without explicit equivalence proofs.
On simpler problems like those in FATE-H, which typically require no prerequisite definitions, this structural overhead yields a net negative impact on compilation. The ablated model, which tends generate monolithic statement using local 1et bindings, avoids these interface complexities but fails to capture the correct semantics, leading to lower final accuracy.
Scaling to Complexity This relationship shifts as problem complexity increases. On FATE-X and Conjectures, the "syntactic cost" of longer code is effectively offset by the "structural bene- fit" of decomposition. Without GoT, the agent's attempt to formalize novel, high-level concepts monolithically leads to 2 distinct failure modes: synthesis failure (inability to generate complex and definitions) and interface hallucination.
In summary, GoT acts manded by research-level fonoloormaiizaiin. Unlike prior works that rely solely on static library retrieval, GoT explicitly leverages the reasoning LLM's natural-language mathematical capability to construct dynamic dependency graphs. This enables a modular formalization style that bridges the gap between the model's internal knowledge and the rigorous requirements of the formal system.
indispensable engine for the creative mathematical construction de-
Table 5: Performance comparison between the full Aria agent and its GoT-ablated version on the FATE-H benchmark. All values are success rates (%).
Configuration
Compiler
Final acc.
Aria (Full System)
89.0
Aria (without GoT)
95.0
54.0
C.3 ABLATING THE RAG MODULE
To measure the value of Eetrieval-Augmentn Generation (RAG), we designed this study to contrast live, base- retrieval against reliance on the pretrained, static knowledge of the Large Language Model (LLM).
In the full system, the agent's grounding process is executed by leveraging LeanSearch. The LLM's task confined reasoning over this verified set of options. For the ablated version, we disable the
28

---

Published as a conference paper at ICLR 2026
retrieval tool entirely. Instead, the agent directly queries the LLM, recall the correct formal name for a concept based on its own knowledge.
Our ablation studies, presented in Table 3 and Table 4 reveal the crucial role of the RAG module, particularly as problem complexity increases. While the ablation version resulted in only a moderate drop in final accuracy FATE-X X (from 69% to 61 %),, its effect on the more challenging Conjectures dataset was absolute, with the success rate collapsing from 42.9% to 0%.
This divergence highlights key insight into the agent's capabilities. For moderately complex tasks like those in FATE-X, the agent can partially compensate for the lack of retrieval through its power- ful self-reflection mechanism. By interpreting the compiler's precise feedback "unknown identi- fiers," the agent may iteratively rediscover correct Mathlib definitions. However, this trial-and-erro recovery process is insufficient for complex conjectures. The 0% accuracy reveals that without the contextual grounding from RAG, the LLM's inaccurate internal knowledge of Mathlib leads it to hallucinate non-existent definitions and confidently judge them as grounded. This foundational er- prevents the generation of compilable code, demonstrating that our RAG module is essential for success on challenging mathematical reasoning tasks.
D PROMPTS
For clarity and reproducibility, we present the prompt frameworks used by Aria across various stages.
Prompt for Decomposition Phase
You are an expert mathematician and specialist in formal mathematics, specifically Lean 4 and its library, mathlib4. Your task is to deconstruct a given mathematical concept into its immediate, foundational prerequisite concepts.
The goal is to produce a list of terms that are thenselves canonical, scarchable definitions. will provide you with examples of correct dcconstruction before giving you the final task.
**Example 1:**
**Input Concept:*. "Finitely Generated Prime Ideal"
**Correct Output:*. "dependencies": ("finitely generated ideal", "prime ideal"]
(few shot examples)...
Nooww perform the task for the following concept based its name
Concepp to deconstruct:*4 "node, name"
Prompt for Grounding Phase
You are a meticulous expert in lean 4 and 'mathlib4 ib4", Your task is to act as "grounding" reasoner for formalization agent. Your goal is to determine if given mathematical concept has canonical 'mathlib', based on 1ist search candidates. Concepp to find:** "node. "nmee **Search Candidates from 'mathlib':**
formal definition
(candidatos context)...
*our Task (Follow these steps PRECISELY): :*) **Step 1: Direst Match Analysis**
First, look for esdirect, canonical definitions* among the cancidates. A direct match is typically 'class', 'structure', or
"cet" whose name is very similar to the concept name (e.g., concept local ring' matches 'class 1slocalkingg)..
29

---

Published as a conference paper at ICLR 2026
If you find clear, direct match, use that as your primary answer. Sttep 2: Deduction from Usage Patterns (If no direct match is found)
If direct match found in Step your task is +xdeduce the canonical name by finding **consistent usage pattern** across multiple 'theorem' and 'instance' candidates.
**Analyze the signatures:** Look for a common identificr that is consistently used cancidates,
**type** **typeclass** across multiple
**Fxample:** If you are locking for "Charßere" and the search results include 'instance Charkero N', 'instance : Charkero 2', and 'theorem my_thm [Charkero R]', the identifie 'Charkero' appears repeatedly typeclass. This overwhelming evidence that the canonical definition named 'CharZero'.
**Strict Rule:** The name you select **must** be an identifier that is explicitly present in the candidate list. De **not** invent, combine, guess emerges from
name. If no single, consistent pattern candidates, you must conclude that no confident match can be found.
**Step 3: Final Decisicn**
Based on your analysis from Step 1 and Step 2, determine the single best for the concept.
Your answer MUST de single, valid JSON object with the following keys:
"bbst__atchh" The full formal name of the canonical definition (e.g., "Ringtheory. Seery.Issloce Isloocalkigg") If no confident match can be found through either direct matching inference, the value must be 'null',
""reasoning""; A brief, one-sentence explanation of HOW you found the match. It must be ene of the following strings: "Found direct definition," "Inferred from usage in instances and theorems. "No confident match found." ++JSON Output:*.
Prompt for Definition Synthesis Phase
You meticulous expert in Lean and 'mathlib4', Using the following verified Lean 4 prerequisite definitions as context, write the formal Lean definition for "node.name name".
Your output must be a single, vell-formed Lean 4 code block. Do not add any explanation outside the code block. **Context from Previous Steps:**
(context co.e)...
Informal Definition of
(informal description)... **Your Task: write the lean "def" or 'class':""
Caution:
Do NOT use sorry to skip the value of the definition.
Prompt for Statement Synthesis Phase
You are a meticulous expert in Lean and 'mathlib4', Your primary goal is to translate infermal mathematical statements into .crrrect, idiomatic, and compilablex* Lean code that seamlessly integrates with the existing Mathlib library. Before generating the final code, you MUST follow structured thought process in tive steps: 1. **Deconstrust** Break down the informal statement into its core mathematicas components (e.g., objects, assumpticns, conclusion).
30

---

Published as a conference paper at ICLR 2026
**Identify Mathlib Components**: List the key Kathlib definitions, theorems, and nctations that are necessary to formalize each component, Guessing is not allowed; refer to known Mathlib APIs. For example, "integral domain' correspends to "[IsDomain R] 'finitely generated module' to [Module.Finite R M)
2.
3. **Plan the Formal Statement**: Outline the structure of the final theorea. This includes defining the types (e.g., 'R M Type* typeclasses (e.g., '[CommRing ) variables, hypotheses, and the goad.
4. **Generate Pinal Code+*: Based on the plan, write the compl ete,
compilable Lean 4 code.
5. Do not generate 'variable' declarations that are irrelevant to the final theorem statement. For single thecren, prefer placing all variables and hypotheses directly in the 'thecrem. signature instead of using a global 'variable' block. **Context (Newly Generated Definitions)
(nowly generated definiticns)...
+ Informal Theorem to Formalize:
(informal statement)...
**Final Lean Theorem Statement:**
Caution: Don't generate explicit header like 'import
Use 'import Mathlib'. +*Crucially,
you must NOT write the procš.** Your only goal is to state the theorem correctly. The procf block must be replaced with the 'sorry' keyword.
Prompt for Reflection
You are a leean expert. The following code you previously generated has a compilation error.
Your task is to analyze the error message and provide corrected version of the code.
You MUST follow this two-step process: **Step 1:
Analysis and Correction Plan.
First, provide a brief analysis of the problem in the following format:
message in 1. **Error Analysis: [Summarize the main
sentence]
2. **Root Cause:** (Explain the underlying reasen for the error,
e.g., missing typeclass instance, type mismatch between term and its expected type, incorrect syntax, etc.]
3. *CCorrection Plan:** [Describe the specific code change you will make to fix the issue, e.g., "Change the typeclass constraint. from [Semiring R] to [Ring s]", "Explicitly access the underlying ideal using .oIddeal", etc.
**Step 2: Corrected Lean Code**
Then, provide the complete, corrected code in a single Lean code block. Do not change the original theorem statement, only fix the proof or definition.
* You generate explicit header like 'import Mathlib.Ringhhen Rlgghhooyy........e.llnnnn Nootherian', USE iimorrt Mathlib'.
about the explicit header,
NOT
**Crucially, you must NOT write the proof.** Your only goal is to state the theorem correctly.
**Failed Code:**
(previous code)...
Error Message from Lean Compiler:** (error message)...
31

---

Published as a conference paper at ICLR 2026
Provide the complete, corrected Lean code in a single code block, without any extra explanation. USE 'import Mathlib' as header!
E GENERALIZATION ACROSS MATHEMATICAL DOMAINS
While our primary experimental analysis centers on the FATE algebra datasets, the mechanisms underlying Aria are not intrinsically limited to algebra. In this section, we analyze the system's 's per- formance across diverse mathematical fields and discuss the rationale behind our domain selection.
E. PERFORMANCE ON PROOFNET
To empirically validate domain generalization, we break down the performance the ProofNet benchmark by subfield. As shown in Table [ Aria demonstrates high consistency across undergraduuat-level algebra, analysis, number theory and topology. Furthermore, surpasses the strong baseline (Goedel-Ve V2) in every category. Notably, in number theory and topology, Aria achieves significant margin in final accuracy, suggesting that retrieval and planning capabil- ities are robust to domain shifts.
Table Performance breakdown by domain on the ProofNet benchmark. Aria demonstrates con-
sistent superiority over the Goedel-V2 V2 baseline across all subfields.
Metric
Algebra
Analysis
Number Theory
Topology
Aria (Ours) Compiler
97.4% %
100.0%
100.0%
96.7% 56.7%
Aria (Ours) Final Acc.
64.7%
64.8%
71.4%
Goedel Compiler
54.7%
81.8%
90.5% 47.6%
26.7%
Goedel Final Acc.
28.9%
44.3%
11.7%
E.2 CASE STUDY: BOREL'S CONJECTURE TOPOLOGY
Furthermore, we successfully applied Aria to formalize Borel's Conjecture in topology. This task requires handling distinct mathematical structures (e.g.. Manifold, ChartedSpace, Homotopyyrroup) that differ significantly from algebraic rings and modules.
This successful formalization confirms that Aria's GoT planner can effectively navigate the defini- tion dependencies in non-algebraic domains, provided that the underlying library support exists.
import Mathlib
/-- closed manifold compact manifold with empty boundary. -/ k] {E
class Isll {k Type*) Type*}
[NormedkdCoommroop E] [NormedSpace k E] (H Type*) [Topol ogi ca caace H
(I ModeLWithCorners k H) (n MithTop Noo) Type*) [TopologicalSpacee M]
[ChartedSpace и M] extends IsManifold I n M, CompactSpace M Prop where
/- The boundary of closed manifold is empty. -/
boundaryless (x : M I.IsBoundaryPoin (chartAt x x))
An aspherical topological manifold is topological manifold "M" that path-connected and for which the "k"-th homotopy group "M, is trivial for all "k 2 2" and all basepoints "x M" -/
structure dessphericcatooooooocclaaaaa (k Type*] (Nontriviallyybomeedr Type*) [NormedkddCommGrrop [NormedSpace R]
k]
32

---

Published as a conference paper at ICLR 2026
Type*] [TppaoggicalSpace H] (I Mode_WithCorners E H)
WithTop Noo) (M : Type*) [TopologiialSpace M] [ChartedSpace
M] : Prop where
/-- An aspherical topological manifold is a topological manifold. -/ is_manifcld IsManifold I M
(-- aspherical topological manifold is path-connected. -/
path_connected : PathConnectedSpace
-- The -k"-th homotopy group of an aspherical topological manifold is
trivial for "k 2 2" 22.-. -/
N) (nk 2 Subsingleton (HomotopyGroup (Kin k) x)
petttcpyygrruss_triie
Let M and N be closed and aspherical topelogical manifolds. If
M N is homotopy equivalence, then is homotepic homeomorphism.
thoorem
[k Typo*) MNontiivaalllMoorraFFiiicc k]
[E Type+] [Normedkd&CommGrouu [NormedSpace E]
Type*) [TopologicallSpace H]
{I Mode1Withhorners E H)
{n WithTop Noo)
(M Type*1 [TopologicalSpace M] |ChartedSpace и M]
IsCiosedManioold
MI
(hM aspherical Iikpperriaalggeelgiiiaaaaaaa
a K)
(N Type*) [Topologicalsp]] N] [ChartedBpace H N]
[IsClosedManifole aaAgheericallopooloo...llaaa
N]
thh_aspherical
N)
Cont ContinuousMap. Hom.osppp..ooootyEEuuuuu
(g : = N), ContinuousMap Homotopic f.toFun (g C (M, N) : by
sorry
STATEMENT ON THE USE OF LARGE LANGUAGE MODELS (LLMs)
In accordance with the policy, we disclose that Large Language Models (LLMs) played significant role in the preparation of this manuscript. The authors take full responsibility for all content, includ- ing any text generated by these models, and have meticulously reviewed and edited all outputs for accuracy, originality, and scientific integrity.
We utilized Google's Gemini-2.5-PHr as language editing tool. Its role was strictly limited to improving clarity, correcting grammatical errors, and rephrasing sentences.
33


Reviews:
[{"review_id": "zLsFtcrOTI", "reviewer": "Reviewer_YbKa", "summary": "The authors introduce two contributions, Aria, an autoformalization method/pipeline which decomposes and grounds an informal statement in Mathlib to ensure correctness, and AriaScore, a new metric which improves upon other alignment scorers such as LeanScore and back-translation. The authors conduct experiments to demonstrate the effectiveness of their contributions.", "questions": "How does your system know the **informal** definitions of things it can't find in Mathlib, e.g., Cohen-Macaulay Module? My understanding is that this would be necessary information to be able to continue breaking down the definition into grounded terms, but I'm not clear on how this works.\n\nWhile it's not in autoformalization, a similar technique as your \"reflection\" module has been used in similar fields such as automated theorem proving (see: COPRA from Thakur et al. 2024) among others. Maybe worth mentioning in related works.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "Both AriaScore and Aria are significant contributions to the community. The authors conduct experiments and error analyses to show that AriaScore performs better at measuring alignment than previous metrics. The authors also show that each of their three components in Aria are important to high performance as shown by an ablation study. Overall, the authors do a good job supporting their claims and have a strong contribution.", "weaknesses": "I think it's worth distinguishing this approach from papers such as (Liu et al, 2025), which also do RAG autoformalization.\n\nAn error analysis of the components of Aria would be very useful to understanding how this method improves. The authors make a claim (~L361) that hallucination of incorrect interfaces is the main source of error. However, why does a single-retrieval RAG system not accomplish a similar improvement in that case? Or perhaps it does, but just not to the same degree? Your ablation study answers this to some extent. But I believe an error analysis would be most beneficial.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "VjfafqkG0l", "reviewer": "Reviewer_vbY2", "summary": "The paper proposes **ARIA**, an agent for translating informal mathematical statements into Lean code through **Graph-of-Thought (GoT)** reasoning, **retrieval-augmented generation (RAG)** from Mathlib, and a **compiler-in-the-loop** feedback mechanism. It also introduces **AriaScorer**, a term-grounded semantic checker ensuring meaning consistency between informal and formal statements. Experiments on **ProofNet**, **FATE**, and real conjectures show **state-of-the-art** performance, demonstrating ARIA’s ability to handle complex, research-level formalization tasks.", "questions": "Please refer to Weaknesses.", "limitations": "", "rating": 4, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- Introduces a **dependency-graph (GoT)** framework that mirrors human reasoning, enabling structured decomposition and synthesis of unseen mathematical concepts.\n- Combines **RAG grounding**, **GoT planning**, and **compiler reflection** into a robust, self-correcting pipeline, with solid ablation evidence.\n- Well-structured and clearly illustrated; figures and examples effectively explain the dependency graph process.\n- Achieves **research-level formalization** beyond prior methods and improves semantic reliability through **term-level grounding** (AriaScorer).", "weaknesses": "- The paper does not provide the detailed prompts used in the key stages—decomposition, grounding, synthesis, and reflection. Since the entire pipeline relies on prompt-driven reasoning, the absence of these examples makes it difficult to reproduce the workflow or evaluate design choices. Including representative prompts or templates would significantly improve clarity and reproducibility.  \n\n- All experiments are conducted on datasets from algebra and commutative algebra, limiting the demonstrated generality of ARIA. It remains unclear whether the dependency-graph and grounding strategies would perform equally well in other mathematical domains such as analysis, topology, or geometry. Broader testing or discussion on domain adaptation would strengthen the paper’s scope and impact.\n\n- The LeanSearch component relies on a locally indexed Mathlib database, which introduces significant computational and storage overhead. A discussion of indexing efficiency, caching, or alternative lightweight retrieval strategies would make the system more practical for large-scale or real-time deployment.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ipyjYzPCnw", "reviewer": "Reviewer_ZfvQ", "summary": "The paper presents ARIA, an agent for auto-formalization of mathematical statements in Lean 4. ARIA integrates Retrieval-Augmented Generation (RAG), a Graph-of-Thought (GoT) planning mechanism, and a reflection loop guided by the Lean compiler. It also introduces AriaScorer, a semantic checker that retrieves term definitions from Mathlib for grounding-based verification. Experiments show improvements over prior baselines.", "questions": "Please refer to the Weakness section.", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "1. The paper clearly motivates improving statement-level formalization before theorem proving by introducing ARIA, an agent designed to convert natural language mathematical statements into Lean 4 formalizations.\n\n2. It presents a well-structured and competently engineered system that integrates Retrieval-Augmented Generation (RAG), a Graph-of-Thought (GoT) planning mechanism, and a reflection loop guided by the Lean compiler, alongside AriaScorer, a semantic checker leveraging Mathlib for grounding-based verification.\n\n3.It evaluates the model on various benchmarks, including conjecture-level tasks.", "weaknesses": "1. The paper claims novelty by integrating RAG, GoT, and the reflection loop guided by the Lean compiler. However, each of these components already exists in prior work. ARIA merely combines these elements without introducing a new algorithmic principle or theoretical insight. This makes the paper engineering incremental rather than conceptually innovative\n2. The core metric is defined using AriaScorer, a tool introduced in the same paper, which introduces a potential self-evaluation bias: the observed performance gains may reflect alignment with the metric rather than genuine capability. Furthermore, only the Conjectures dataset has been human-verified, leaving the main benchmarks unchecked. Alternative metrics for autoformalizers, such as typecheck and BEq [1], exist, and reporting results under these metrics would provide a more robust and credible evaluation.\n3. Table 1 compares ARIA with Goedel-V2, although most results reported are for pass@1. However, “pass@k” sampling is not equivalent to multi-stage agentic reasoning. Additionally, regarding the Conjectures dataset, I would like to ask why ARIA exhibits such a significant advantage on this data. It seems likely that other models may not have encountered this type of data during training, resulting in 0% accuracy for those models.\n\n[1] Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, Junchi Yan. Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "nhWmu3I6pF", "reviewer": "Reviewer_Tkra", "summary": "This paper presents Aria, an agent system for auto-formalizing mathematical statements through a two-phase Graph-of-Thought (GoT) process: recursively decomposing statements into conceptual dependency graphs anchored to Mathlib via RAG, then bottom-up construction of formalizations synthesizing new definitions through compiler-in-the-loop reflection. The paper also introduces AriaScorer, a semantic checker achieving term-level grounding by retrieving actual definitions of Lean terms. Experiments demonstrate that Aria achieves 44.0% accuracy on FATE-X (baseline: 24.0%) and 42.9% on Homological Conjectures (all baselines: 0%), significantly outperforming existing methods.", "questions": "1. **Regarding semantic error propagation mechanism**: Is AriaScorer's semantic checking iteratively applied to each newly synthesized node during the GoT synthesis phase (Figure 1(B)), or only performed once at the end? If not iteratively applied, how does the system prevent or recover from compound semantic errors caused by intermediate definitions that are \"correctly-typed but semantically wrong\"? Is there experimental data quantifying the impact and system robustness under such error scenarios?\n\n2. **Regarding the deep mechanism of Table 5's anomaly**: Removing GoT increases compilation rate (89.0%→95.0%) but decreases accuracy (71.0%→54.0%) on FATE-H. Does this suggest that the non-GoT monolithic approach tends to produce syntactically simpler (thus easier to compile) but semantically incorrect formalizations? Can you provide concrete cases for in-depth analysis of the root cause of this \"high compilation, low accuracy\" failure mode? What does this reveal about GoT's core value (enforcing semantic structure vs. syntactic simplification)?\n\n3. **Regarding reliability of critical decision points in GoT decomposition**: This process relies on an LLM reasoner to judge whether retrieved Mathlib candidates are \"suitable matches\" and decide whether to use candidates or trigger synthesis of new concepts. Overall pipeline performance critically depends on this decision's accuracy. How is this LLM reasoner's accuracy evaluated? Is there data showing the specific impact of its erroneous decisions (e.g., deciding to synthesize an existing concept or incorrectly matching an irrelevant concept) on end-to-end performance?\n\n4. **Regarding robustness boundaries of AriaScorer**: This checker's term-level grounding depends on retrieving term information from the Herald dataset. What are AriaScorer's failure modes if Lean terms used in formalized statements are not included in this dataset, or if informal descriptions of terms in the dataset are inaccurate or ambiguous? Does the paper experimentally quantify the checker's robustness to incomplete grounding datasets? How does this affect the method's generalization capability to new domains or rapidly evolving Mathlib versions?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "- **Effective system architecture**: The paper successfully integrates GoT planning, RAG, and compiler-in-the-loop reflection to address the critical failure point of prior models in synthesizing new definitions. Ablation studies in Table 3 validate the necessity of each component: removing RAG or reflection causes accuracy to collapse from 42.9% to 0% on the Conjectures dataset.\n\n- **Innovative contribution of AriaScorer**: This checker transcends text similarity limitations by employing the static analyzer jixia to retrieve actual definitions of Lean terms. Table 2 validates that this term-level grounding step is crucial for improving accuracy.\n\n- **Breakthrough experimental results**: The system achieves 42.9% success rate on the Homological Conjectures benchmark where all baseline models completely fail (scoring 0%), demonstrating the unique capability and practical value of this compound approach for conjecture-level formalization.", "weaknesses": "- **Compound propagation risk of semantic errors**: The paper explicitly states that the GoT synthesis phase ensures only syntactic correctness and \"cannot preclude correctly-typed but semantically wrong translations,\" while AriaScorer's semantic checking is described as a final step (Figure 1(C)). This creates a critical logical gap: if a base concept (e.g., \"Cohen-Macaulay Module\" in Figure 1) is semantically incorrect during synthesis, it will serve as a syntactically valid but semantically flawed premise for synthesizing all dependent parent nodes, invalidating entire dependency branches. The paper lacks crucial discussion or experimental validation on whether AriaScorer should be iteratively applied to each node during the synthesis phase to prevent this issue.\n\n- **Insufficient explanation of contradictory phenomena in GoT ablation**: Table 5 shows that removing GoT paradoxically increases compilation rate (89%→95%) while decreasing final accuracy (71%→54%) on FATE-H. Although Section C.2 mentions this leads to \"synthesis failure\" and \"interface hallucination\" failure modes, it inadequately explains why a simpler monolithic approach systematically produces more syntactically simple (thus easier to compile) but semantically incorrect code. The fundamental mechanism of this \"high compilation, low accuracy\" failure mode remains unclear, weakening understanding of GoT's core value.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "wauGuEbAEY", "reviewer": "Reviewer_tTzy", "summary": "The paper introduces Aria, a system designed to perform autoformalization of high-level mathematical statements into Lean 4 syntax. Aria emulates human reasoning via a two-phase Graph-of-Thought (GoT) process: (1) recursively decomposing a conjecture into a dependency graph of definitions and sub-statements, and (2) constructing Lean-formalized statements using retrieved definitions from Mathlib. To enforce semantic precision, it employs AriaScorer, a retrieval-based verifier that grounds terms and checks logical consistency.\nThe model combines retrieval-augmented generation, graph reasoning, and self-reflection for improved correctness. On three benchmarks (ProofNet, FATE-X, and Homological Conjectures) Aria achieves strong improvements. The paper claims Aria is the first system to synthesize novel definitions during autoformalization, addressing a key bottleneck in automated mathematical reasoning.", "questions": "Addressing the points I mentioned in weakness part should be enough.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The combination of retrieval, graph-of-thought reasoning, and verification is well-motivated and logically coherent. Autoformalization of research-level statements is a frontier problem, and this paper is impactful both for Lean and general symbolic reasoning research.\n\n2. Performance is satisfactory. The system achieves SOTA results across diverse benchmarks, especially on difficult tasks where all prior models can't do well.\n\n3. It tackles hallucination and definition synthesis, the two well-known weaknesses of current formalization LLMs.\n\n4. The use of term-level retrieval (AriaScorer) for semantic grounding is a technically meaningful contribution that enhances reliability.", "weaknesses": "1. More ablation study can make it even better. The contribution of each submodule (retrieval, GoT reasoning, reflection, AriaScorer) is not quantified in detail; ablation or controlled comparison would strengthen claims.\n\n2. Some discussion on Aria's generality to other systems (e.g., Coq, Isabelle, Lean 3) will make it more impactful.\n\n3. While promising, the \"first to synthesize novel definitions\" claim may need stronger empirical evidence (e.g., human evaluation verifying novelty and correctness).\n\n4. More detailed discussion on computational cost or efficiency will be very beneficial for assessing scalability.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "VdhhWq4b0n", "reviewer": "Reviewer_dKZk", "summary": "This paper proposes Aria, a comprehensive agent-based autoformalization pipeline designed to emulate human reasoning for research-level mathematics. The system first performs graph-of-thought decomposition, transforming natural language statements into dependency graphs and grounding the identified concepts in mathlib when possible. For ungrounded concepts, it employs graph-of-thought synthesis to generate Lean representations through a self-reflective loop.\n\nThe authors further introduce AriaScorer, which decomposes informal statements into atomic assumptions and conclusions, then aligns them with formal clauses retrieved from Lean’s library and their corresponding natural language versions to compute an aggregated correctness score.\n\nExperimental results demonstrate that Aria significantly outperforms existing LLM-based autoformalization baselines on the ProofNet, FATE benchmarks, and real-world conjectures. Moreover, AriaScorer achieves more accurate verification of formalization correctness compared to other evaluation methods.", "questions": "* Could you include some manual evaluation on the main experiments to better assess the quality and reliability of the autoformalized results?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "* The paper is well-written and well-motivated. Its focus on research-level mathematical autoformalization is interesting.  \n* The proposed Aria and AriaScorer frameworks are novel, integrating several intuitively and carefully designed components into a cohesive pipeline.  \n* Experimental results demonstrate that both Aria and AriaScorer are effective, outperforming existing methods by a substantial and consistent margin.  \n* The key insights underlying AriaScorer are also inspiring, offering a new perspective on evaluating the correctness of autoformalization.", "weaknesses": "There is no human evaluation in the main results, which makes the reported performance less reliable. Moreover, since AriaScorer uses Gemini for both generation and evaluation, the results may be biased toward its own generated responses, especially when compared to other baselines such as Goedel-Autoformalizer.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)