Metraipolis › archive › dc_ee49c85ceefa

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-03T18:13:48.662Z
SHA-256 of the archived text: 22e25a1a452678349c5f5a3dedeef23cbb06e5b598fa017fbccca3dde54d10c4
Stable URL of this page: https://metraipolis.com/documento/dc_ee49c85ceefa

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_ee49c85ceefa (Metraipolis archive dc_ee49c85ceefa, sha256 22e25a1a452678349c5f5a3dedeef23cbb06e5b598fa017fbccca3dde54d10c4)

BibTeX

@misc{dcee49c85ceefa,
  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_ee49c85ceefa; sha256 22e25a1a452678349c5f5a3dedeef23cbb06e5b598fa017fbccca3dde54d10c4},
  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-03T18:09:53.368Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).