Tensor Algebra Equivalence Checker
summary
A semantic equivalence checker formally verifies whether an optimized PyTorch or Triton kernel computes the same function as its baseline for all inputs, lowering programs through FX graph extraction, TTIR expansion, decomposition, scalarization and feeding scalar formulas to the Z3 SMT solver. On KernelBench Level1 it proves 16 kernels equivalent and finds two real bugs, including a float32 constant-truncation error two orders of magnitude below typical tolerance, and it scales to straight-line, loop-free LLM-generated kernels.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:45AI-generated GPU kernels rise
- 2:52Need for auto kernel generation
- 4:15Correctness challenges in AI kernels
- 5:40Testing with fixed configs
- 8:04Testing with sample configs
- 9:52Testing with input distributions
- 12:22Testing with fuzzing
- 14:52Trust in kernels beyond testing
- 15:34TAEC tool overview
- 19:28Future of AI kernels
- 20:09Closing remarks
related talks
20mUnlocking Performance: Harnessing LLMs To Streamline GPU Kernel Development in...
32mPanel Discussion: The AI Kernel...
10mMaximizing Kernel Development Productivity Under Performance Constraints
18mA Verified Compiler for a Functional Tensor Language
08mGPU Programming with Triton Kernels
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
19mPolyJuice: Detecting Mis-Compilation Bugs in Tensor Compilers with Equality Saturation(…)
15mHEC: Equivalence Verification Checking for Code Transformation via Equality...