一句话：提出首个 GPU 内核等价性检查器，形式化验证手工、LLM 与编译器优化的 ML 内核正确性。
深度学习与大语言模型推动大量 GPU 内核执行，这些内核成为激进优化的目标；近期用 LLM 生成的 GPU 内核缺乏形式化保证。本文提出首个 GPU 内核等价性检查器，用于形式化验证手工、LLM 与编译器优化的机器学习内核的正确性。作者证明该检查器是可靠的（sound），并且对一类定义良好、涵盖许多实际程序的 GPU 内核是完备的（complete）。其实现 VOLTA 能够验证卷积、矩阵乘法以及多种注意力机制等 ML 计算。
With the rapid progress of deep learning and large language models (LLMs), companies spend enormous sums executing GPU kernels. These kernels have become prime targets for aggressive optimization. Recent efforts increasingly leverage LLMs to generate GPU kernels, but make no formal guarantees about the generated kernels. We present the first equivalence checker for GPU kernels and use it to formally verify the correctness of machine learning (ML) kernels optimized by hand, by LLM, and by compiler. We show that our equivalence checker is sound and, for a well-defined class of GPU kernels which includes many programs of interest, complete. Our implementation, VOLTA, can verify ML computations such as convolutions, matrix multiplications, and various attention mechanisms.
@article{paperbot12095,
title = {Equivalence Checking of ML GPU Kernels},
author = {Benjamin Driscoll and Kshitij Dubey and Anjiang Wei and Neeraj Kayal and Rahul Sharma and Alex Aiken},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839470}
}