GPU Kernel Correctness Verification

GPU: Graphics Processing Unit

Follow this topic Ask about this topic

Latest papers

13 papers3 papers in the last four weeks, level with the four weeks before. 0.0% of all new papers.

Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking
Oct 20, 2026Tuan Truong Vu, Cheng TanGPU Kernel Correctness Verification Formal Verification
Northeastern University
RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Oct 5, 2026Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt +4Formal Verification GPU Kernel Correctness Verification
University of California, Riverside Riverside, California, USA · Math, Inc. New York City, New York, USA · Microsoft Research Redmond, Washington, USA
AI as a Compiler: Compiling Triton kernels without the Triton compiler
Sep 29, 2026François Costa, Charly Castes, Thomas Bourgeat +1GPU Kernel Optimization Large Language Model-Guided Optimization
Stanford University · EPFL
Silent Failures Beyond the 32-Bit Index Range: A Differential Characterization of Large-Tensor Matrix Multiplication in PyTorch's MPS Backend
Sep 19, 2026Junichiro NiimiGPU Kernel Correctness Verification
Meijo University
The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs
Sep 17, 2026Paul Biberstein, Joseph Devietti, Mayur NaikDifferential Testing GPU Kernel Correctness Verification
University of Pennsylvania Philadelphia, PA, USA
Measuring the Checker: Mutation Analysis for GPU-Kernel Benchmark Oracles
Sep 2, 2026Mingzhe Du, Anh Tuan Luu, Dong Huang +1GPU Kernel Correctness Verification Benchmark Auditing
National University of Singapore · Nanyang Technological University · CAIR, VinUniversity
Deterministic LLM Inference Across GPU Kernels: Power-of-Two INT8 Quantization Scales and the Limits of Tolerance-Based Conformance
Aug 25, 2026Teng-Ruei ChenLLM Quantization Neural Network Quantization
Krixvon, Taipei 100, Taiwan
The Integer Alibi: Localizing Cross-Kernel Divergence in INT8-Quantized LLM Inference
Aug 13, 2026Teng-Ruei ChenGPU Kernel Correctness Verification LLM Inference
Krixvon, Taipei 100, Taiwan
A Contract-Grade Verifier for LLM-Generated GPU Kernels, and a Native Blackwell Backward for the Gated-Linear-Recurrence Family
Aug 13, 2026Rishi Shah, Rishav ShresthaAutomated Software Testing Formal Verification
E3A Healthcare
Test-Input Generation for Tensor Programs: What Actually Finds Kernel Bugs
Jun 23, 2026Dipankar SarkarAutomated Software Testing Benchmark Design
Arizona State University, USA
The Correctness Illusion in LLM-Generated GPU Kernels
Jun 18, 2026Dipankar SarkarAutomated Software Testing Differential Testing
Arizona State University, USA
Kernel Contracts: A Specification Language for ML Kernel Correctness Across Heterogeneous Silicon
Apr 23, 2026Cooper VeitFormal Verification Heterogeneous Computing
Ashiba Research
M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification
Mar 6, 2026Mengting He, Shihao Xia, Haomin Jia +2GPU Kernel Correctness Verification LLM Inference
Penn State, USA · SKLP, ICT, CAS, China · Peking University, China

Oct 20, 2026J/K move · Enter open · S save

Racer: Hunting GPU Kernel Bugs with Symbolic Equivalence Checking

Tuan Truong Vu, Cheng Tan

Northeastern University

GPU Kernel Correctness Verification Formal Verification

Open paper AskPDF arXiv

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.