LARK：LLM生成GPU内核的Lean辅助自动形式化验证框架

LARK是一个能自动对LLM生成的GPU内核进行形式化等价性验证的智能体框架。 它通过Lean 4将内核拆解为可证明片段，并与PyTorch参考实现逐段比对以验证正确性。 在KernelCraft任务中，LARK配合ReAct智能体，使GLM 5.3成功验证了12个Level-1内核中的10个，并在生产级内核中发现了1个新的数据竞争漏洞。