张量代数属性骨架：增强 AI 编译器的基于属性的测试

TVM 和 ONNX-MLIR 等深度学习 (DL) 编译器将张量计算图转化为目标后端的优化可执行文件。测试这些编译器在模糊测试环境中生成格式良好的输入方面取得了实质性进展。然而，仅靠这样的生成并不能捕获图转换和优化所期望保留的代数不变量的语义漂移。虽然张量代数已经研究了几十年，但它还没有转化为深度学习编译器可执行的基于属性的测试（PBT），因为这样做需要联合构建算子、张量和预言机的耗时且容易出错的任务。核心挑战不再是为模糊深度学习编译器生成格式良好的输入，而是使用此类输入和基于张量代数的正确预言来引导可执行 PBT。我们在 Propilot 中实现了这一愿景，Propilot 是一个 LLM 驱动的基于代理属性的 DL 编译器测试框架。首先，Propilot 将张量代数知识表示为可重用的属性骨架，每个属性骨架都与算子约束和预言模板相结合。其次，给定目标编译器，Propilot 通过生成成对的张量计算图、张量输入和预期语义关系作为预言机，将这些骨架实例化为可执行的 PBT。第三，为了防止生成的测试退化为无效或无信息的 PBT，Propilot 在执行之前验证每个 PBT 候选者的适用性和安全性。验证反馈、执行结果和覆盖信号指导后续生成。我们使用 212 个运营商和 20 个财产骨架在 TVM 上评估 Propilot，生成 4,579 个 PBT。与直接基于 LLM 的 PBT 生成相比，Propilot 减少了 49% 的冗余，并通过显式属性骨架消除了无效测试。这种有效性转化为发现语义错误和数字差异。