paperbot · PL 论文追踪

全部论文 待读 收藏

P1 GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM Testing

GenCoG:一种基于 DSL 的 TVM 测试计算图生成方法
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 5/10 · 论文将DSL、类型约束求解和混合执行用于TVM计算图生成测试,属于PL技术在机器学习系统中的邻接应用,可能与PL→AI/ML系统测试相关;但它不涉及静态分析、Agentic程序、LLM,也不涉及浮点或贝叶斯程序分析,因此与核心研究方向匹配度中等。引用 23 inbox
Zihan Wang, Pengbo Nie, Xinyuan Miao, Yuting Chen, Chengcheng Wan, Lei Bu, Jianjun Zhao
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出 GenCoG,用 DSL 描述算子类型约束并通过混合执行求解,增量生成有效且高表达力的计算图以测试 TVM。

现有 Muffin、NNSmith 等深度学习编译器测试方法生成的计算图要么类型不合法,要么表达力不足,难以覆盖 TVM 的核心功能。GenCoG 由两部分组成:GenCoGL,一种用于描述算子类型约束的领域特定语言;以及基于混合执行(concolic)求解类型约束并增量生成高表达力计算图的方法。作者在多个 TVM 版本上评估:GenCoG 生成的计算图全部通过类型检查,顶点和边多样性分别达到现有方法的 1.65~6.93 倍和 1.06~7.08 倍,并在 TVM v0.8/v0.9 中发现 16 个缺陷,其中 14 个确认、12 个修复。

问题
现有计算图生成方法(如 Muffin、NNSmith)生成的图常类型不合法或表达力不足,无法有效测试 TVM 等深度学习编译器的核心功能。
方法
提出 GenCoG:用 DSL(GenCoGL)声明算子类型约束,并通过混合执行(concolic)求解约束、增量生成高表达力计算图。
评估
在 TVM 多个版本上评估,所有生成图通过类型检查,顶点/边多样性显著优于现有方法,并在 v0.8/v0.9 发现 16 个缺陷(14 确认、12 修复)。
原文摘要(Abstract)

TVM is a popular deep learning (DL) compiler. It is designed for compiling DL models, which are naturally computation graphs, and as well promoting the efficiency of DL computation. State-of-the-art methods, such as Muffin and NNSmith, allow developers to generate computation graphs for testing DL compilers. However, these techniques are inefficient — their generated computation graphs are either type-invalid or inexpressive, and hence not able to test the core functionalities of a DL compiler. To tackle this problem, we propose GenCoG, a DSL-based approach to generating computation graphs for TVM testing. GenCoG is composed of (1) GenCoGL, a domain-specific language for specifying type constraints of operators, and (2) an approach that concolically solves type constraints and incrementally generates computation graphs of high expressivity. We implement and evaluate GenCoG on TVM releases. Our results show that GenCoG is effective in generating valid and expressive computation graphs — all of the GenCoG-generated graphs pass type checking, a critical graph validation stage; letting the graphs’ expressivity be measured by their vertex and edge diversities, GenCoG outperforms state-of-the-arts by achieving 1.65~6.93× in vertex diversity and 1.06~7.08× in edge diversity, respectively. Furthermore, GenCoG has detected 16 bugs in TVM v0.8 and v0.9, with 14 confirmed and 12 fixed.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{WangNMCWB023,
  title = {GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM Testing},
  author = {Zihan Wang and Pengbo Nie and Xinyuan Miao and Yuting Chen and Chengcheng Wan and Lei Bu and Jianjun Zhao},
  booktitle = {ISSTA},
  year = {2023},
  doi = {10.1145/3597926.3598105}
}