Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.28429

Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking

Tuan Truong Vu·Cheng Tan
View original source ↗Read source document ↗Export metadata ↓

Abstract

GPU kernels are critical to the performance of today's AI services, yet the same operators are rewritten repeatedly: for each GPU generation, numeric format, serving regime, and kernel language. Every rewrite must preserve the function computed by the implementation it replaces. Today, this obligation depends almost entirely on differential testing: run the new kernel and a trusted reference on randomly sampled tensors, then compare their outputs within a tolerance. This approach has blind spots that additional test cases cannot eliminate. For example, a logical bug may produce an error smaller than the tolerance required to accommodate a correct optimized kernel. We propose symbolic equivalence checking, which executes a kernel and its reference on symbolic inputs, turning each output cell into an exact algebraic expression, and then checks whether the paired expressions agree for all inputs. Because these expressions are exact, symbolic equivalence checking distinguishes floating-point error from logical bugs, while a single check covers the entire input space. We implement Racer, a PTX-level symbolic equivalence checking engine, with three techniques that make this approach practical for production kernels: (1) Shape Reduction to control checking cost, (2) a lockstep CTA scheduler to handle concurrency, and (3) idiom templates with exact numeric refutation for otherwise inconclusive results. Across 2,408 production kernels from 41 collection targets, Racer found 82 real bugs in 23 libraries, including 76 previously unknown bugs and 41 confirmed so far.

Explore related subjects

cs.SCcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Tuan Truong Vu, Cheng Tan. 2026-10-20. Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking. https://arxiv.org/abs/2610.28429

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Indefinite Summation Problem for the Laurent Ring

This article solves the Indefinite Summation Problem (ISP) for the difference ring $(A, α)$, where $A$ is the Laurent ring of shift operators on the lattice $\Z^n$, and $α$ is any ring automorphism of $A$ of finite order. The space of summable elements in $(A, α)$ is infinite dimensional, and it is possible to write down an explicit basis for it. The solution translates to a finite procedure involving a matrix multiplication, where the size of the matrix can be estimated. It follows that the arithmetic complexity of the solution can also be determined. These results extend to a solution of the ISP for the ring of functions on $\Z^n$, on which $α$ acts by duality. The article also points out that the solution to the ISP amounts to calculating the group cohomologies $H^i([α], A), i = 0, 1$, where $[α]$ is the cyclic group generated by $α$.

cs.SC↗
arXiv2026

Sparse Polynomial GCD Cannot Be Computed in Fixed-output Polynomial Time

This paper shows that, assuming $\mathsf{P}\ne\mathsf{NP}$, sparse univariate polynomial GCD cannot be computed in fixed-output polynomial time over any fixed computable field. Precisely, there is no deterministic algorithm that can compute the GCD of sparse univariate polynomials over any fixed computable field with total bit complexity polynomial in the input size, with the output size as a fixed parameter. In particular, there is no deterministic algorithm for sparse polynomial GCD that runs in polynomial time with respect to both the input and the output sizes. This settles the open problem posed as Challenge 5 in the sparsity challenges. Furthermore, we show that the Roots of Unity Detection problem over finite fields is NP-hard under random reductions; that is, determining whether the GCD of a sparse univariate polynomial and $x^n - 1$ has nonzero degree is NP-hard.

cs.SC↗
arXiv2026

Diverse Reasoning Paths Matter: Symbolic Equivalence Augmentation for Enhancing RL Exploration

Reinforcement learning with verifiable rewards (RLVR) has emerged as a powerful paradigm for improving the reasoning capabilities of LLMs. However, the role of supervised fine-tuning (SFT) data in enabling effective downstream RL remains underexplored. In this paper, we investigate a key hypothesis: the diversity of reasoning steps in chain-of-thought (CoT) during SFT is a critical enabler of RLVR performance. To test this hypothesis, we introduce EquivAug, a data augmentation framework that uses symbolic equivalence transformations to generate diverse yet provably correct reasoning paths. By converting CoT solutions into formal symbolic representations, applying equivalence transformations, and reconstructing natural-language explanations, EquivAug produces training data that differs in reasoning steps rather than surface-level lexical variation. Experiments on GSM8K and FOLIO across model scales demonstrate that EquivAug consistently achieves the highest reasoning path diversity after SFT and the strongest accuracy after GRPO. Our results establish that CoT diversity during SFT is positively correlated with downstream RLVR performance.

cs.SC↗