【第三周】论文精读：Aria: An Agent for Retrieval and Iterative Auto-Formalization via Dependency Graph

前言自动形式化Auto-formalization是将自然语言数学定理转化为形式化证明语言如 Lean 4的关键步骤也是实现自动化数学发现与验证的基石。然而现有大语言模型LLM在处理研究级数学猜想时常因幻觉Hallucination、语义失配以及无法合成新定义而失败。来自北京大学与 IQuest Research 的团队提出了Aria一个模拟人类专家推理过程的智能体系统。Aria 创新性地采用两阶段思维图Graph-of-Thought, GoT流程首先递归分解陈述构建依赖图然后自底向上合成形式化代码。为确保语义正确性作者还推出了AriaScorer一个基于检索的项级语义检查器。实验显示Aria 在 ProofNet 上达到68.5%的最终准确率在极具挑战性的同调猜想数据集上更是取得了42.9%的突破性成绩其他模型均为 0%确立了该领域的 SOTA 地位。 论文基本信息项目内容论文标题Aria: An Agent for Retrieval and Iterative Auto-Formalization via Dependency Graph核心方法名Aria (GoT-based Auto-Formalization Agent)作者Hanyu Wang, Ruohan Xie, Yutong Wang, et al.所属机构Peking University, IQuest Research, Renmin University of China发表年份2026 (ICLR Conference Paper)核心领域Auto-formalization, Graph-of-Thought, Retrieval-Augmented Generation (RAG), Semantic Verification关键数据集ProofNet, FATE-H/X, Homological Conjectures (14 real-world conjectures)代码开源GitHub - frenzymath/jixia (相关工具) 研究背景与痛点1. 现有方法的三大致命缺陷静态知识局限LLM 的训练数据是静态的无法跟上 Mathlib 库的快速迭代常生成不存在或已过时的 API幻觉。缺乏合成能力研究级数学常涉及库中未定义的新概念。现有“一步生成”方法无法自发合成这些缺失的定义导致任务直接失败。语义检查失效现有的语义检查器如 LeanScorer过度依赖文本相似度难以检测深层的语义偏差如参数顺序错误、隐含前提遗漏。2. Aria 的核心洞察模仿专家思维人类数学家不会一次性写出复杂定理而是先拆解概念依赖再逐个定义最后组装。Aria 通过GoT模拟这一过程。检索增强合成对于库中存在的概念通过 RAG 精准定位对于不存在的概念利用已定义的子概念进行自底向上的合成。项级语义锚定语义检查必须基于 Mathlib 中术语的真实定义而非表面文本。️ 核心方法Aria 架构详解Aria 系统由两个主要部分组成GoT 自动形式化流水线和AriaScorer 语义检查器。1. 思维图GoT自动形式化流水线该流程分为两个阶段形成一个闭环的推理结构阶段一GoT 分解Top-Down Decomposition依赖图构建将输入的自然语言陈述拆解为概念节点如“Noetherian Ring”, “Cohen-Macaulay Module”构建有向无环图DAG。检索与锚定Grounding对每个节点调用LeanSearch实时更新的 Mathlib 搜索引擎检索候选定义。LLM 作为推理器从候选列表中选择最匹配的规范定义。若找不到匹配项该节点被标记为“待合成”并触发对其子节点的递归分解直到所有叶子节点都能在 Mathlib 中找到。阶段二GoT 合成Bottom-Up Synthesis自底向上生成从依赖图的叶子节点开始利用已检索或已合成的子节点代码作为上下文生成当前节点的 Lean 定义。编译器在环反思Compiler-in-the-Loop Reflection生成的代码立即送入 Lean 编译器检查。若编译失败将错误信息反馈给 LLM 进行修正最多尝试 16 次。只有编译通过的代码才会被用于父节点的合成。新定义合成对于标记为“待合成”的节点LLM 基于其子节点的定义创造性地编写新的 Lean 结构或类。2. 语义正确性模块AriaScorer为解决“编译通过但语义错误”的问题作者设计了 AriaScorer子任务分解将非形式化陈述和形式化陈述都分解为原子假设和结论。项级语义锚定Term-Level Grounding使用静态分析工具jixia提取形式化代码中的所有 Lean 术语。从 Mathlib 数据集中检索这些术语的权威定义、类型和非形式化描述。将这些真实定义注入到 LLM 的提示词中强制模型基于真实语义而非表面文本进行评估。模糊积分评分综合各子任务的匹配度完美匹配/轻微不一致/严重不一致输出 0-1 的分数超过阈值则判定为正确。 实验结果与分析作者在多个基准测试中评估了 Aria涵盖了从本科数学到前沿研究猜想的广泛难度。1. 全面超越 SOTA (End-to-End Performance)ProofNet(本科级): Aria 取得68.5%的最终准确率编译语义远超 Goedel-V2 (32.0%) 和 Gemini-2.5-Pro (27.8%)。FATE-X(博士/研究级): Aria 达到44.0%而最强基线 Goedel-V2 (pass128) 仅为 24.0%。同调猜想(Conjectures): 这是最具挑战性的测试集14 个真实的交换代数猜想。Aria:42.9%(成功形式化 6 个)。其他所有模型:0%。意义证明了 Aria 是唯一能处理未知概念合成与研究级逻辑依赖的系统。2. AriaScorer 的有效性验证在 FATE-X 数据集上的语义检查对比准确率: AriaScorer 达到89.9%(α0)显著高于 LeanScorer (71.0%) 和回译法 (33.3%)。查全率(Recall): AriaScorer 高达96.2%能有效识别出那些“编译通过但语义错误”的隐蔽案例。关键发现项级锚定能检测出参数顺序颠倒、隐含前提遗漏如 UFD 必须是整环以及术语定义偏差等深层错误。3. 消融实验关键发现反射机制(Reflection): 移除后FATE-X 最终准确率从 44% 暴跌至14%证明多轮自我修正是 syntactic correct 的关键。GoT 规划器: 移除后Conjectures 成功率从 42.9% 降至7.1%证明结构化分解对于处理新概念至关重要。RAG 模块: 移除后Conjectures 成功率直接归零 (0%)说明没有实时检索LLM 的静态知识完全无法应对研究级数学。 主要创新点总结思维图驱动的形式化范式首次将Graph-of-Thought应用于自动形式化通过“分解 - 检索 - 合成”的闭环成功解决了研究级数学中新概念合成的难题。项级语义锚定检查器 (AriaScorer)突破了传统基于文本相似度的检查局限通过检索 Mathlib 权威定义注入上下文实现了对深层语义一致性的精准验证。编译器在环的深度反思将 Lean 编译器作为实时反馈信号结合多轮迭代修正大幅提升了代码的语法鲁棒性即使在复杂依赖下也能保证编译通过。研究级数学的突破在真实数学猜想如同调猜想上实现了从 0 到 1 的突破证明了 AI 辅助前沿数学研究的可行性。⚠️ 局限性与挑战计算成本高GoT 流程和多次反射导致每个问题平均需要17.7 次LLM 调用推理延迟较高。依赖外部工具系统强依赖 LeanSearch 和 jixia 等外部工具的稳定性与更新频率。错误传播风险虽然罕见但如果中间层定义出现语义错误且未被检查器发现可能会传播到最终定理论文中提到仅发现 1 例此类情况。领域泛化虽然在代数和拓扑上表现良好但在极度依赖特定领域公理系统的分支中仍需进一步验证。 总结与工程建议《Aria》展示了将结构化推理GoT、实时检索RAG与严格验证Compiler Semantic Scorer相结合的巨大威力。它不仅是自动形式化的 SOTA也为构建高可靠性 AI 科学助手提供了蓝图。 对开发者的实战建议引入依赖图规划处理复杂任务时不要试图一步生成。先让 LLM 画出概念依赖图识别哪些是已知库函数哪些需要自定义再按顺序生成。实施项级语义检查在验证环节不要只靠 LLM“凭感觉”判断。务必检索权威定义如文档、API 说明并注入 Prompt让 LLM 基于事实进行比对这能大幅减少幻觉漏检。编译器/解释器在环对于代码生成任务必须建立生成 - 编译/运行 - 报错反馈 - 修正的闭环。单次生成的成功率远不如带反馈的迭代。动态检索增强对于快速迭代的知识库如代码库、法律条文、数学库必须接入实时检索引擎不能仅依赖模型的预训练知识。容忍冗余以换取正确性在研究级任务中显式地定义中间引理和结构即使库中可能有隐含定义往往比隐式引用更稳健有助于类型检查和后续证明。一句话总结Aria 通过“思维图拆解依赖、检索增强填补知识、项级锚定确保语义”的三位一体策略攻克了研究级数学自动形式化的堡垒是构建高可信科学 AI 的里程碑式工作。参考文献[1] Wang H, Xie R, Wang Y, et al. Aria: An Agent for Retrieval and Iterative Auto-Formalization via Dependency Graph[C]//The Thirteenth International Conference on Learning Representations (ICLR). 2026.