发表机构
University of Pennsylvania（宾夕法尼亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出输出空间假设，通过翻转量词检查单个输出位置对所有输入的等价性，实现张量程序更一致的错误发现，在6988个AI编写的CUDA内核中找出600个隐藏错误。
AI 中文摘要
深度学习模型中使用的张量程序是优化的主要目标，因为微小的性能改进就能对训练或推理工作负载产生巨大影响。然而，这类优化过程复杂且可能引入微妙的错误。传统上，当针对随机输入的参考实现进行差分测试未能揭示错误时，便假定程序正确。然而，这些程序的输入是庞大的张量，发现错误可能需要生成具有精确数值关系的极低概率输入。我们提出了一种新颖的方法，通过翻转量词来更一致地发现错误。与其生成单个输入并检查所有输出张量位置的等价性，不如检查单个输出张量位置对所有输入的等价性？我们通过一种新颖的符号执行策略，在系统\dirigo中实现了这一想法。我们证明，\dirigo能够在一个包含6,988个AI编写的CUDA内核的公共数据集中有效发现错误，这些内核均被差分测试标记为正确。其中，\dirigo发现600个内核实际上存在错误，并在两分钟内发现了其中97.3%的错误。
英文摘要
Tensor programs, as used in deep learning models, are a prime target for optimization, as small performance improvements can have a large impact across training or inference workloads. However, such optimizations are complicated and can produce subtle bugs. Traditionally, correctness is assumed when differential testing against a reference on random inputs fails to reveal bugs. However, the inputs to these programs are massive tensors, and finding bugs can require generating extremely low likelihood inputs with precise relationships among their values. We propose a novel way to find bugs more consistently by flipping the quantifiers. Rather than generating a single input and checking all output tensor locations for equivalence, what if you could check a single output tensor location's equivalence for all inputs? We implement this idea in a system, \dirigo, by using a novel symbolic execution strategy. We demonstrate that \dirigo can find bugs effectively in a public dataset of 6,988 AI-written CUDA kernels that are all marked correct by differential testing. Of these, \dirigo finds 600 kernels that are actually buggy, and finds 97.3\% of those bugs within two minutes.
