LARK 发布：验证 LLM 生成 GPU 内核
热点事件持续更新
LARK 发布：验证 LLM 生成 GPU 内核
1 篇报道1 个报道来源7 小时前更新
先了解这件事
AI 综述
2026 年 11 月 3 日，研究团队在 arXiv 发布 LARK 框架，并首次实现了对 LLM 生成 GPU 内核的自动化形式验证。该框架借助 Lean 4 将内核拆解为可证明片段，再与 PyTorch 参考实现逐段比对，以验证内核正确性。 在 KernelCraft 任务中，LARK 配合 ReAct 智能体使 GLM 5.3 成功验证了 12 个 Level-1 内核中的 10 个，并在生产级内核中发现了 1 个新的数据竞争漏洞。研究团队还包括 Zixi Zhang 等研究者。
AI 根据报道生成 · 1 小时前更新
最新进展11月3日 13:00
LARK：LLM生成GPU内核的Lean辅助自动形式化验证框架报道时间线
沿着报道，了解事件的不同侧面。
11月3日
- arXiv · AILARK：LLM生成GPU内核的Lean辅助自动形式化验证框架
LARK是一个能自动对LLM生成的GPU内核进行形式化等价性验证的智能体框架。 它通过Lean 4将内核拆解为可证明片段，并与PyTorch参考实现逐段比对以验证正确性。 在KernelCraft任务中，LARK配合ReAct智能体，使GLM 5.3成功验证了12个Level-1内核中的10个，并在生产级内核中发现了1个新的数据竞争漏洞。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。