# The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 31 references that are in the map.
- First posted on arXiv 17 Sep 2026.

## Builds on (most cited first, 7 of 7)

- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [KernelBench: Can LLMs Write Efficient GPU Kernels?](https://mlsanity.com/paper/2502.10517/) (2025)
- [Kevin: Multi-Turn RL for Generating CUDA Kernels](https://mlsanity.com/paper/2507.11948/) (2025)
- [Towards Robust Agentic CUDA Kernel Benchmarking, Verification, and Optimization](https://mlsanity.com/paper/2509.14279/) (2025)
- [Autocomp: A Powerful and Portable Code Optimizer for Tensor Accelerators](https://mlsanity.com/paper/2505.18574/) (2025)
- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)
- [Equivalence Checking of ML GPU Kernels](https://mlsanity.com/paper/2511.12638/) (2025)

## Abstract (arXiv)

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.