arXiv · cs.AI · Zixi Zhang, Jiayi Nie, Haoran Wu, Yujie Yan, Yann Herklotz, Rika Antonova, Robert Mullins, Yiren Zhao, George A. Constantinides, Jianyi Cheng2026-11-03 13:00 · 12 小时前模型评分57

LARK：用 Lean 辅助推理形式化验证大语言模型（LLM，Large Language Model）生成的图形处理器（GPU，Graphics Processing Unit）内核

LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels

导读

研究团队提出 LARK，一个对大语言模型（LLM，Large Language Model）生成的图形处理器（GPU，Graphics Processing Unit）内核做形式化验证的智能体框架，在精确算术下证明其与 PyTorch 参考实现的功能与内存行为等价。

分类置信度

中 · 待人工复核

只有单一媒体来源，需要人工复核。

来源级别：媒体与个人

事件类型：研究发布

证据摘录

“We introduce LARK, an agentic framework that automatically and formally verifies GPU kernels against their PyTorch reference implementations.”

来源：arXiv · cs.AI · arxiv.org

推理能力部署工程论文研究 #论文/研究 #部署/工程 #推理

LARK：用 Lean 辅助推理形式化验证 大语言模型（LLM，Large Language Model） 生成的 图形处理器（GPU，Graphics Processing Unit） 内核

LARK：用 Lean 辅助推理形式化验证大语言模型（LLM，Large Language Model）生成的图形处理器（GPU，Graphics Processing Unit）内核