RESOLVE: Language-Agnostic Validation of GPU Kernels Through Testing, Reduction, and Proof
Authors: Ashkan Vedadi Gargary, Guido Martínez, Sebastian Burckhardt, Gabriel Ebner, Abhinav Jangda, Madan Musuvathi, Tyler Sorensen
Organizations: University of California, Riverside Riverside, California, USA · Math, Inc. New York City, New York, USA · Microsoft Research Redmond, Washington, USA
AI systems can now write and optimize production GPU kernels, but validating them remains an important challenge. Evaluating the kernel on a few random inputs and checking that its outputs match a trusted reference kernel within numeric tolerances is not sufficient: races can cause nondeterministic behavior that fails to manifest in tests, and numeric tolerances can hide bugs and cause false positives even after extensive calibration. To address this challenge, we present RESOLVE, which combines testing and formal verification to build a comprehensive kernel validation pipeline. It operates in three steps: First, it tests for nondeterminism using binary instrumentation that perturbs execution timing to expose races. Second, an agent rewrites the candidate and reference kernels to obtain "reduced-concurrency" versions that are simpler to analyze but still produce bitwise-identical outputs in all tests. Third, the reduced kernels are formally analyzed in the F*/Pulse framework and prove that they perform the same computation on real numbers. This sidesteps the need for numeric tolerances. We show that RESOLVE can validate a broad selection of kernels using KernelBench, and prove equivalence across fused GEMMs in three state-of-the-art frameworks and languages: CUTLASS, Triton, and Gluon. It also analyzes mega-kernels, notoriously difficult to validate, and finds four previously unreported issues, including two clear bugs. We show that agents can use RESOLVE to repair the issues, with minimal performance impact, highlighting that agents can optimize aggressively when they can rigorously check their results.
Figures & tables
Figure 1. The three passes RESOLVE makes over the binary, and the question each one answers.
Figure 2. Memory-reference operand events per problem across RKB, measured by the counting pass on H100. Activity spans roughly four orders of magnitude, from under 108 to beyond 1011 . Histogram over the 98 RKB problems with a nonzero count, on a logarithmic axis of memory-reference operand events per problem. Bar heights from left to right are 2, 2, 4, 27, 22, 16, 14, 6, and 5 problems, peaking just below ten to the ninth and tailing off past ten to the eleventh.
Figure 3. Where potential conflicts occur across RKB, by memory region and by thread hierarchy level. Counts are out of 100 and the categories overlap, since a kernel can have conflicts at several levels. Horizontal bar chart over 100 kernels. 41 have no potential conflict. By memory region: shared 59, global 8. By thread hierarchy level: within a warp 49, within a CTA 59, across CTAs 8.
Figure 4. Both Kuiper programs provably satisfy S . Vertical links test bitwise equality, using extracted CUDA for Kuiper. The dashed conclusion for the originals relies on those tests. Two columns, reference and candidate, each contain an original kernel, a reduced kernel, and a Kuiper program, from top to bottom. Adjacent versions in each column are linked by tested bitwise equality. Solid proof arrows connect both Kuiper programs to one shared algebraic specification. A dashed connection between the originals denotes the inferred shared specification, conditional on the tested links.
Outcome
Kernels
Classified after first phase
Pass: Deterministic and bitwise identical
15
Fail: Empty kernel, no memory accesses
2
Differ bitwise, require full RESOLVE workflow
Pass: Reduced and formally verified
11
Inconclusive: Missing Kuiper feature
2
Table 1. Outcomes over the RKB candidates (§ 6.2 ).
Time (min)
Median tokens
Stage
Med.
Min
Max
In
Out
D. testing
1.47
1.05
19.20
—
—
Reduction
29.31
12.56
74.40
39.1K
8.1K
Spec. & proof
112.18
44.55
250.20
5.54M
65.6K
Total
142.96
58.16
343.80
5.72M
73.4K
Table 2. Cost per kernel over the 14 RKB kernels carried through the full workflow. Times are wall clock. Medians do not sum, so the total row is the median over per-kernel totals. Determinism testing (D. testing) is the only stage that uses no agent.
Figure 5. Choosing the trace record budget. (a) Potential conflicts found, by memory region and by thread hierarchy level. The inventory is complete at 100 million records and unchanged at 200 and 400 million. (b) Mean, minimum and maximum time to trace and analyze one kernel, which keeps rising past that point. By default we trace 200 million records. Two line charts against trace record budget from one million to four hundred million on a logarithmic axis. The left chart plots six conflict indicator counts, which rise and then flatten from one hundred million onward. The right chart plots mean, minimum and maximum time to configure a kernel, which continues to rise across the same range.
Stage
CUTLASS
Gluon
Triton
D. testing
9.73
8.18
10.40
Reduction
17.17
15.56
10.92
Spec. & proof
∼60∗
∼60∗
—
Table 3. Time to validate each variant of the fused MLP kernel, in minutes. Gluon and Triton are bitwise identical, so only Gluon was specified and proved. Starred entries are estimates at about an hour each, since a logging fault on those runs lost the exact time.
Root cause
Repair
Latency
LUCE (barrier)
Order the counter reset against arriving blocks
−1.4%
LUCE (scratch)
Give the scratch address a block and head offset
−1.6%
FlashMoE
Reserve slots independently of arrival order
+0.8%
FastMoE
Prune capacity independently of arrival order
+10.5%
Table 4. What each repair changed, and what it cost. Latency is the change in warmed call latency after the repair, so a negative number is faster. The two LUCE rows compare each original variant against the combined repair.
GPU kernel optimization is increasingly critical for efficient deep learning systems, but writing high-performance kernels still requires substantial low-level expertise. Recent AI coding agents can iteratively read code, invoke compilers and profilers, and refine implementations, yet existing kernel benchmarks evaluate single LLM calls rather than full agent workflows, and none include both kernel-to-kernel optimization and unseen-configuration generalization testing. We present AgentKernelArena, an open-source benchmark for measuring AI coding agents on GPU kernel optimization. The benchmark contains 196 tasks spanning HIP-to-HIP optimization, Triton-to-Triton optimization, and PyTorch-to-HIP translation, and evaluates complete agent workflows in isolated workspaces using gated compilation, correctness, and performance checks, centralized scoring and an unseen-configuration generalization protocol that tests whether optimizations transfer to input configurations the agent never observed. Across production agents including Cursor Agent, Claude Code, and Codex Agent, we find near-perfect compilation and high correctness rates on most task categories, with the strongest configurations achieving mean speedups of up to 6.89x on PyTorch-to-HIP, 6.69x on HIP-to-HIP, and 2.13x on Triton-to-Triton tasks. Our unseen-configuration evaluation shows that HIP-to-HIP and Triton-to-Triton optimizations largely transfer to unseen input shapes, while PyTorch-to-HIP exhibits substantial correctness drops, indicating that agents generating kernels from scratch frequently hardcode shape-specific assumptions. AgentKernelArena is designed as a modular, extensible framework for rigorous evaluation of agentic GPU kernel optimization across agents, tasks, and hardware targets.
Sharareh Younesian, Wenwen Ouyang, Sina Rafati +11
Deep learning inference and training performance depends critically on GPU kernel efficiency. Modern compilers such as PyTorch Inductor automatically generate GPU kernels from high-level model code, but frequently underperform expert-written implementations by wide margins. Recent LLM-assisted kernel optimizers can close this gap for standalone kernels, yet treat compiled models as black boxes, generally optimizing individual standalone kernels without respecting the compiler's structural decisions or verifying the model end-to-end. We present KernelOPT, a multi-agent system that treats compiled models as structured artifacts. It preserves vendor library calls (cuBLAS, cuDNN) and exclusively targets generated Triton sub-kernels using five profiling-guided LLM agents. A four-gate verification cascade applies static validation, multi-seed correctness checking, model-level float64-fallback verification, and performance gating (γ=1.03) to filter candidates and verify the re-stitched model end-to-end. When candidates fail verification, the system preserves the compiler baseline. The system accepts PyTorch nn Modules, standalone Triton kernels, and Helion kernels. Evaluated on 250 KernelBench problems (100 Level 1, 100 Level 2 and 50 Level 3) on NVIDIA H200, KernelOPT achieves geometric mean speedups over torch compile of 1.40× (L1), 1.15× (L2), and 1.07× (L3) across all kernels, including fallback cases. Optimized-only geomeans (excluding cases where verification gates preserve the compiler baseline) are substantially higher: 2.54× (L1: 36/100), 1.84× (L2: 23/100), and 1.37× (L3: 11/50), reflecting where the optimizer achieves meaningful leverage.
Systems that generate GPU kernels with language models report high correctness rates. Those rates come from a single loose test: run the kernel on a few random inputs at one fixed shape and accept it if the output is close to a reference. A kernel can pass that test and still be silently wrong. It can return an ordinary number where the true answer is a NaN or an infinity, differ from run to run, break when the shape changes, or accumulate in fp16 where the reference keeps an fp32 total. We build the instrument that checks correctness properly: a contract-grade verifier of twelve adversarial gates, each a property a correct kernel must satisfy, several of them tolerance-free, so no choice of threshold can explain a failure away. Aimed outward, the verifier audits 2,638 machine-generated kernels that a public system's own harness had already accepted as correct. It finds 39.5% broken beyond any tolerance argument and 62.1% carrying at least one violation. The field's standard test accepts 1,487 kernels the verifier rejects, against only 14 the other way. We defend the finding four independent ways: a 7/7 positive control, a threshold-calibration sweep, 98.5% agreement with the reference benchmark's own correctness code, and a stratified hand-audit. Aimed inward, the verifier judges a kernel of our own: the first native Blackwell tcgen05 training backward for the gated-linear-recurrence (GDN) family, including the reverse-state stage the field still runs on a fallback. We establish its correctness independently, against a double-precision oracle, and train five family members through it. The correctness signal behind reported progress in kernel generation is far weaker than the numbers suggest, and a set of tolerance-free contracts would close most of the gap.