# Equivalence Checking of ML GPU Kernels

arXiv: https://arxiv.org/abs/2511.12638 · HTML: https://mlsanity.com/paper/2511.12638/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Nov 2025.

## Built on by (most cited first, 7 of 7)

- [Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon](https://mlsanity.com/paper/2604.22032/) (2026)
- [The Integer Alibi: Localizing Cross-Kernel Divergence in INT8-Quantized LLM Inference](https://mlsanity.com/paper/2608.13756/) (2026)
- [Deterministic LLM Inference Across GPU Kernels: Power-of-Two INT8 Quantization Scales and the Limits of Tolerance-Based Conformance](https://mlsanity.com/paper/2609.00363/) (2026)
- [PTXBench: Benchmarking and Adapting LLMs for GPU Kernel Optimization with Architecture-specific PTX](https://mlsanity.com/paper/2608.17379/) (2026)
- [The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs](https://mlsanity.com/paper/2609.19611/) (2026)
- [Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization](https://mlsanity.com/paper/2609.34069/) (2026)
- [AI as a Compiler: Compiling Triton kernels without the Triton compiler](https://mlsanity.com/paper/2609.36800/) (2026)

## Abstract (arXiv)

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.