← 研踪 PaperTrailarXiv:2611.04447 · v1
Formalizing PTX in Lean to Prove GPU Kernel Correctness
首次提交 2026-11-03 15:37
版本更新 2026-11-03 15:37
雷达观测 2026-11-04 23:40
摘要
We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async operations, multi-kernel pipelines and data-dependent control flow. We implement it in Lean and use it to prove the correctness of simple implementations of a WGMMA GEMM kernel, FlashAttention, and a 3-kernel MoE pipeline.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-03 15:37 · 最新观测版本
Formalizing PTX in Lean to Prove GPU Kernel Correctness
We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async operations, multi-kernel pipelines and data-dependent control flow. We implement it in Lean and use it to prove the correctness of simple implementations of a WGMMA GEMM kernel, FlashAttention, and a 3-kernel MoE pipeline.
查看此版本解读 →查看此版本原文 ↗