013 · 告诉 Agent 错在哪里，比只说“结果错了”更有用吗？

核心问题：当高性能 GPU 优化必须同时保持跨线程、跨内存层级的数据关系时，把这些关系写成编译期不变量并返回具体反例，是否比单纯的测试成败与性能数字更能引导 Agent？

论文卡片

• 原题： Ave: Guiding Agentic GPU Optimization Using Data-Flow Invariants
• 作者： Haohui Mai、Xiaoyan Guo、Xiangyun Ding、Daifeng Li、Qiuchu Yu、Chenzhun Guo、Cong Wang、Jiacheng Zhao、Christos Kozyrakis、Binhang Yuan。
• 机构： CausalFlow、香港科技大学、清华大学、斯坦福大学、中国科学院大学、加州大学河滨分校。
• 版本： 2026-04-16 首次提交；2026-09-14 更新至 arXiv v2，并由 v1 的 ARGUS 更名为 Ave；15 页；分类为 cs.DC、cs.AI、cs.PL；SOSP 2026。
• 定位： 用领域专用语言、静态分析和数据流不变量约束 LLM Agent 优化 GPU kernel 的实证系统论文。
• 阅读入口： alphaXiv · arXiv · PDF 全文

论文讲了什么

高性能 kernel 不是把几个局部技巧独立叠加起来。共享内存暂存、软件流水线、矩阵指令的数据布局、wavefront 分工和指令调度彼此耦合；某次变换即使能编译，也可能让错误的数据元素在线程或内存层级之间配对。单元测试只能在末端说“结果错了”，性能测量只能说“变慢了”，都不直接指出哪条跨层关系被破坏。

Ave 为此设计了一种面向 tile 的 Python DSL。开发者或知识库用 tag function 给数据附上由逻辑坐标推导的符号标签；编译器让标签随数据流和控制流传播；在矩阵指令等使用点，tag assertion 再声明哪些标签必须相等或满足指定关系。分析器采用流敏感、路径不敏感的抽象解释，并把约束交给 SMT 求解器。若断言失败，它返回线程、数据元素和程序位置的具体赋值，而不是只返回布尔失败。

Agent 工作流也被拆成两层。ICRL planner 从人工整理的优化知识库中选择和排序策略；lowering agent 把策略落实为 DSL 代码，并实例化与该策略配套的不变量。编译期检查、单元测试和实测性能共同形成反馈。论文中的 attention 例子里，反例直接指出某个 MFMA 使用点的 K、Q 标签不一致；下一轮据此修改共享内存读取布局后才进入性能评测。

主要结果

论文首先在 AMD MI300X 上评价五组 GEMM、五组 grouped-query flash attention 和五组 fused MoE 配置，起点都是朴素实现。专家基线包括 hipBLASLt、AITER、HipKittens 和 Triton；Agent 基线包括 Atrex、KernelFalcon、KSearch 与 CUDAForge。除成本较高的 Atrex 最多运行五轮外，其余系统最多运行十轮，并报告最佳有效结果；“有效”要求编译、通过不变量检查与正确性测试，并通过人工 reward-hacking 审查。

使用 GPT-5.6 Sol 时，Ave 在三类工作负载上的几何平均吞吐分别达到专家参考的 0.89×、0.99× 和 0.94×。相对于未直接取用参考实现的 Agent 基线，论文报告 1.62–1176× 的几何平均吞吐提升；这个跨度很大，部分原因是较弱基线没有使用矩阵核或漏掉关键低层优化，不能理解为 Ave 在所有任务上都稳定提升三个数量级。

更直接支持核心主张的是消融实验。五组 attention 配置中，仅有运行时反馈时，Agent 尝试的异步加载和 bank-conflict 优化没有奏效，最终约为 190 TFLOPS；加入知识库和不变量、但不使用 ICRL 时达到 255 TFLOPS；保留知识库与 ICRL、移除不变量时，Agent 无法修复转置布局的配对错误，只达到 194 TFLOPS；完整系统依次完成五项优化，达到 588 TFLOPS。这里说明规划顺序与不变量反馈缺一不可，而不是把全部收益单独归因于静态分析。

作者还在 60 个选定的 KernelBench GEMM／卷积任务上移除不变量模板，要求 Agent 同时完成 MFMA、软件流水线和硬件越界保护加载。六个“数据集层级 × 模型”组合中，加入不变量后成功数都增加：例如 L1 上 GPT 从 8 增至 18，DeepSeek V4 Pro 从 1 增至 16；L2 上分别从 12 增至 25、从 7 增至 26。轮数、token 和 API 成本通常下降，但墙钟时间并非一致改善。

在更宽的生成评测中，Ave 使用 DSL 示例后，GPT 在 100 个 KernelBench L1 与 100 个 L2 任务上的 Pass@3 为 100% 和 88%。作者把直接调用 PyTorch、针对特定输入走捷径等输出人工判为失败。在 NVIDIA H200 上，三类生产 kernel 相对各自专家参考的几何平均吞吐为 0.98×、1.00× 和 0.99×，但移植仍需专家加入硬件 intrinsic 与架构专属知识。

证据边界

数据流不变量不是完整的功能正确性证明。Ave 主要检查共享内存布局、元素配对以及优化步骤声明的关系；分析是路径不敏感的，涉及全局内存写入的 MoE 路由、多 GPU 通信，以及一个字节内两个 FP4 nibble 的置换，都超出当前表达或追踪范围。通过检查只说明已声明的不变量成立，没有声明的错误仍可能存在。

不变量也不会提出新算法或自动选择 tile size、wavefront specialization。论文明确把算法选择与初始生成留给 planner 和知识库，再用不变量保护低层变换。因此实验测到的是 DSL、编译器分析、人工知识、ICRL 规划和 lowering agent 组成的系统能力；虽然消融削弱了其中若干部件，但不能把接近专家库的性能归结为“反例反馈”单一因素。

基线比较也受预算与接口能力影响。Ave 的 DSL 显式暴露寄存器类别、硬件指令和调度屏障，一些基线所用语言无法表达相同控制；各系统只运行有限轮数并取最佳有效结果。跨架构结果证明了同一思路可以移植，却没有证明无需专家：论文报告为新架构补充工具链、intrinsic 和知识条目，初始支持约需一人周。

最后，reward-hacking 审查针对已知捷径且带有定性人工判断。作者承认人工可能漏掉更隐蔽的取巧，不变量也只能发现落入其词汇表的行为。因此 KernelBench 通过率比只看测试更严格，但仍不是穷尽性的语义保证。

重点读哪里

先读 §2–§3，理解高性能 attention 中跨层数据关系为什么会成为 Agent 的难点；再读 §4–§5，看 tag、assertion、抽象解释和 SMT 反例分别承担什么角色；随后读 §6 的 ICRL 工作流。实验部分重点看 §9.2 的系统消融和 §9.4 的不变量消融；§8 集中列出了保证边界与跨架构代价。

思考启发

以下是导读者由论文引出的理解角度，不是作者额外验证过的结论。

Ave 把反馈从结果层推进到了结构层。测试失败只表明至少有一个输入产生错误，而不变量反例把失败投影到“哪个线程、哪个元素、在哪个使用点破坏了什么关系”。这不是让模型凭空获得更多推理能力，而是改变它面对的搜索空间：许多错误候选在运行前就被排除，剩下的修改也有更具体的局部目标。

但结构化反馈的有效性来自预先定义的概念边界。知识库不仅记录“做软件流水线”，还要附上这项优化必须保持的关系模板。系统因而把一部分专家判断从每次手工调试，转移到可复用的不变量词汇中。它减少的是重复推理，并没有消除决定“什么必须保持不变”的知识工作。

三个思考问题

1. 不变量提高成功率，证明的是反馈更好，还是搜索空间更窄？

当 Agent 只能在受限 DSL 和预设关系中修改程序时，成功率提高应如何在“获得有效指导”和“失去部分探索自由”之间解释？

2. 具体反例在什么意义上是“解释”？

SMT 返回线程、坐标和程序位置后，它说明了约束如何被违反，是否也说明了该怎样修复、以及哪项优化决策本身有误？

3. 谁来验证不变量本身？

若知识库为一种优化绑定了遗漏或写错的关系模板，编译器成功证明这些断言时，系统获得了什么保证，又可能产生怎样的虚假安全感？