Metraipolis › archive › dc_a899ffec6ebe

LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels — arXiv:2611.02028

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.02028
License (as archived): CC0-1.0
Archived: 2026-11-03T10:32:29.405Z
SHA-256 of the archived text: a6202e9a06d7999f62fc26b9de9a4859406b732ce015e5715375d1cd477227fc
Stable URL of this page: https://metraipolis.com/documento/dc_a899ffec6ebe

How to cite

LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels — arXiv:2611.02028 — arXiv (en), https://arxiv.org/abs/2611.02028 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_a899ffec6ebe (Metraipolis archive dc_a899ffec6ebe, sha256 a6202e9a06d7999f62fc26b9de9a4859406b732ce015e5715375d1cd477227fc)

BibTeX

@misc{dca899ffec6ebe,
  title = {LARK: Lean-Assisted Reasoning for LLM-Generated GPU Kernels — arXiv:2611.02028},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.02028},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_a899ffec6ebe; sha256 a6202e9a06d7999f62fc26b9de9a4859406b732ce015e5715375d1cd477227fc},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.02028. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Efficient GPU kernels are typically low-level and hardware-specific, and LLM agents can now generate them faster than experts can verify. Existing approaches rely on testing, which provides evidence but not a guarantee of correctness. We introduce LARK, an agentic framework that automatically and formally verifies GPU kernels against their PyTorch reference implementations. LARK proves equivalence in functional and memory behavior under exact arithmetic and establishes a new trust boundary: human effort is only needed to verify operator-level Lean semantics ahead of kernel generation time, instead of checking every single line of generated code. LARK formalizes the GPU machine model and the semantics of each operation in Lean 4 once per target language, and the Lean 4 semantics of any incoming kernel is derived from these pre-built definitions. LLM agents then automate the proof in two steps. First, an agent decomposes the whole kernel semantics into smaller segments and Lean 4 verifies this segmentation, which addresses the intractability of proving equivalence for large kernels directly. Second, agents write Lean proofs that each kernel segment matches its high-level PyTorch counterpart. Together, the two steps give whole-program equivalence. We demonstrate that LARK can be used 1) to ensure correctness in existing code-generation agents and 2) to automatically verify human-written kernel libraries. On the KernelCraft GPU tasks, combined with a simple ReAct agent, LARK enables GLM 5.3 to fully verify 10 of 12 Level-1 kernels and Opus 5.5 all 5 Level-2 kernels. Moreover, over 10 production kernels randomly sampled from popular open-source LLM serving frameworks, LARK verifies 9 and identifies a new data race bug in the tenth. We believe LARK represents a significant step toward verifiable code generation in the agentic era.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI).
Pagina del lavoro: https://arxiv.org/abs/2611.02028 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-03T10:29:48.538Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).