Functorial Lowering for Verifiable Cross-Platform Code Generation with Large Language Models: A Position Paper

Abstract

Large language models (LLMs) generate plausible code but offer no guarantee that it is correct or that it exploits the target hardware well. Compilers offer the opposite trade-off: rigorous, structure-preserving translation, but only along optimizations their authors anticipated. We argue that category theory provides a precise interface between the two. Computations are modeled as morphisms in a symmetric monoidal category, each hardware target as a category of implementable programs, and lowering to a target as a functor. The LLM proposes candidate implementations of individual morphisms, while functoriality turns the correctness of the composed program into local proof obligations checkable by testing, equivalence checking, or formal verification. We illustrate the formulation on blocked matrix multiplication, operator fusion, and convolution lowered to CPU and GPU targets, clarify the scope of quantum targets, and close with a research agenda and evaluation plan.