【第三周】论文精读：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 (pass@128) 仅为 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.