CORTEXA
← Browse
arxivcs.PLcs.AIcs.LG2026-07-15

Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code

Niels Mündler-Sasahara, Hristo Venev, Dawn Song, Martin Vechev, Jingxuan He

Languages with rich static semantics, such as Rust, provide stronger guarantees for AI-generated code, but their strictness makes generation more difficult. Off-the-shelf compilers can provide useful feedback post-generation, but does not guide intermediate generation steps, such as those during autoregressive LLM decoding. Constrained decoding intervenes earlier by rejecting invalid tokens during sampling, but requires white-box model access and costly reimplementation for semantic constraints. We introduce generative compilation, the first approach to obtaining compiler feedback on partial programs during generation. The core technical device is a sealor: a lightweight, mostly syntax-guided transformation that converts partial programs into complete ones that standard compilers can diagnose. It is designed such that possible-to-complete partial programs are never rejected, while preserving enough code context to catch genuine dead ends early. We construct such a sealor on a core Rust-like calculus and prove that it satisfies these properties, all mechanized in Lean. We extend it to the first partial-program checker for real Rust. We evaluate our method on challenging repository-level Rust coding tasks, across both frontier black-box and open-weight models. We show that generative compilation reduces non-compiling outputs and improves functional correctness, relative to standard post-generation feedback. It does so by detecting a broad range of errors close to their source and early during generation, thereby reducing errors cascades and enabling focused diagnostics. More broadly, generative compilation is a step toward making compilers a first-class citizen of AI-assisted programming active during generation, rather than a separate post-generation check.

View free PDFSource page

Related papers

arxivcs.PLcs.AIcs.LG2026-07-20

Decode-Time Grammars: Constrained LLM Generation over a Refinement Order of Grammar Fragments

Shuoming Zhang, Ruiyuan Xu, Haofeng Li, Qiuchu Yu, Yangyu Zhang, Chunwei Xia, et al.

Large language models now write a growing share of the world's code, increasingly inside agents and serving systems that compile, execute, or dispatch generated code without line-by-line review. This works well for mainstream languages but remains brittle for low-resource program…

View free PDFSource page
arxivcs.LGcs.AIcs.PL2026-07-03

Differentiate the Evaluator, Not the Program: An Efficient Runtime Representation for Neuro-Symbolic Learning

Lucas Sheneman

AI systems increasingly propose executable scientific models whose value depends on both their symbolic structure and their fitted continuous parameters. This makes parameter calibration the bottleneck of program-and-parameter co-search: an outer loop can generate thousands of ca…

View free PDFSource page
arxivcs.AIcs.LGcs.PL2026-07-18

Exact Network Surgery: Functional Invariance and Gradient Plasticity in Reactive Computational Graphs

Abdallah Khemais

Function-preserving network growth techniques such as Net2Net and progressive stacking expand a model's capacity without destroying its learned function, but existing formulations either tolerate numerical perturbations or require a full rebuild of the training program. We formal…

View free PDFSource page
arxivcs.SEcs.AIcs.LGcs.PL2026-07-17

AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language

Qiyuan Xu, Joshua Ong Jun Leang, Renxi Wang, Wenda Li, Haonan Li, Luke Ong, et al.

Interactive theorem proving (ITP) underpins program verification and formalized mathematics, but its manual effort limits scalability. LLM-based proof agents promise to ease this effort, but their heavy token consumption and API cost remain a major obstacle. We trace this cost to…

View free PDFSource page
arxivcs.PLcs.AIcs.LGcs.MA2026-07-20

ETAS: An Effect-Typed Language for Agent Systems

Huiri Tan, Yikun Wang, Puyang Zhang, Shangyu Li, Jiasi Shen

ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic n…

View free PDFSource page
arxivcs.AIcs.CLcs.LGcs.PL2026-07-14

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

Marcus J. Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, et al.

Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target…

View free PDFSource page