Equivalence Checking of ML GPU Kernels
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911273258582016 |
|---|---|
| author | Dubey, Kshitij Driscoll, Benjamin Wei, Anjiang Kayal, Neeraj Sharma, Rahul Aiken, Alex |
| author_facet | Dubey, Kshitij Driscoll, Benjamin Wei, Anjiang Kayal, Neeraj Sharma, Rahul Aiken, Alex |
| contents | With the rapid progress of deep learning and large language models (LLMs), companies now spend enormous sums executing GPU kernels. These kernels have, therefore, 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 LLMs, and by compilers. We show that our equivalence checker is sound and, for a well-defined class of GPU kernels which includes the programs of interest, complete. Our implementation, VOLTA, can verify ML computations such as convolutions, matrix multiplications, and various attention mechanisms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_12638 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Equivalence Checking of ML GPU Kernels Dubey, Kshitij Driscoll, Benjamin Wei, Anjiang Kayal, Neeraj Sharma, Rahul Aiken, Alex Programming Languages With the rapid progress of deep learning and large language models (LLMs), companies now spend enormous sums executing GPU kernels. These kernels have, therefore, 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 LLMs, and by compilers. We show that our equivalence checker is sound and, for a well-defined class of GPU kernels which includes the programs of interest, complete. Our implementation, VOLTA, can verify ML computations such as convolutions, matrix multiplications, and various attention mechanisms. |
| title | Equivalence Checking of ML GPU Kernels |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2511.12638 |