Aria通过依赖图迭代重构定理，提升大模型数学形式化准确率。
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
- 构建依赖图递归分解定理，基于Mathlib定义进行语义对齐
- 在ProofNet上编译成功率91.6%，最终准确率68.5%，超越前人方法
- 擅长处理高阶代数与同调猜想，适合数学研究自动化场景
精确的定理陈述自动形式化对推进研究级数学的自动化发现与验证至关重要，但大模型因幻觉、语义错配及无法合成新定义而面临瓶颈。为此，我们提出Aria（检索与迭代形式化的智能体），一种在Lean环境下实现猜想级形式化的系统，通过双阶段思维图过程模拟人类专家推理：递归分解命题为依赖图，并从基础概念构建形式化表达。为确保语义正确性，引入AriaScorer检查器，从Mathlib检索定义实现术语级对齐，支持严格验证。在多个基准测试中评估Aria：在ProofNet上达到91.6%编译成功率和68.5%最终准确率，优于现有方法；在FATE-X（来自研究文献的挑战性代数问题集）上，以44.0%对比基线24.0%的最终准确率领先；在同调猜想数据集上，达成42.9%的最终准确率，而其他模型均为0%。
原文摘要 · Abstract (English)
Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for LLMs due to hallucinations, semantic mismatches, and their inability to synthesize new definitions. To tackle these issues, we present Aria (Agent for Retrieval and Iterative Autoformalization), a system for conjecture-level formalization in Lean that emulates human expert reasoning via a two-phase Graph-of-Thought process: recursively decomposing statements into a dependency graph and then constructing formalizations from grounded concepts. To ensure semantic correctness, we introduce AriaScorer, a checker that retrieves definitions from Mathlib for term-level grounding, enabling rigorous and reliable verification. We evaluate Aria on diverse benchmarks. On ProofNet, it achieves 91.6% compilation success rate and 68.5% final accuracy, surpassing previous methods. On FATE-X, a suite of challenging algebra problems from research literature, it outperforms the best baseline with 44.0% vs. 24.0% final accuracy. On a dataset of homological conjectures, Aria reaches 42.9% final accuracy while all other models score 0%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。