用 Lean 形式化 PTX 以证明 GPU 内核正确性

论文在 Lean 中形式化 PTX，并证明若干 GPU 内核实现的正确性。

资讯摘要

论文提出一种对 PTX 进行数学形式化的方法，可对深度学习 GPU 内核中的常见模式建模与推理，包括 acquire-release、tensor cores、proxies、异步操作、多内核流水线和数据相关控制流。作者在 Lean 中实现该方法，并用它证明 WGMMA GEMM 内核、FlashAttention 及三内核 MoE 流水线的简单实现是正确的。

要点速读

1. 论文提出在 Lean 中形式化 PTX，以建模和推理 GPU 内核中的常见模式。
2. 覆盖 acquire-release、tensor cores、proxies、异步操作、多内核流水线与数据相关控制流。
3. 作者报告已用该形式化证明 WGMMA GEMM、FlashAttention 和三内核 MoE 流水线简单实现的正确性。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/5 08:00:38（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。