PaperlayerView exact revision on arXiv

Source-linked AI summary

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

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

arXiv:2607.13921v2cs.PLcs.AIcs.LG

TL;DR

AI-generated Rust code is difficult to produce correctly, while existing compiler feedback either arrives after generation or requires constrained-decoding infrastructure. Generative compilation seals partial programs for standard compiler checking during generation, reducing non-compiling outputs and improving functional correctness over post-hoc feedback.

  • Problem

    AI-generated Rust code remains error-prone, while post-generation compiler feedback does not guide intermediate generation and constrained decoding requires white-box access and costly semantic reimplementation.

  • Method

    Generative compilation seals partial programs into complete programs with placeholders so standard compilers can provide diagnostic feedback during generation.

  • Results

    Generative compilation reduces non-compiling outputs and improves functional correctness across most model-task configurations compared with post-generation feedback.

  • Takeaways & Limitations

    Generative compilation brings black-box-compatible compiler diagnostics into intermediate code generation, detecting errors earlier and closer to their source.

  • Takeaways & Limitations

    The formal guarantees cover verdicts but do not formalize whether returned diagnostics describe genuine defects rather than sealing artifacts.

Abstract

from arXiv · show

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.

1 Introduction

Generative compilation brings compiler-style feedback into code generation by checking partial programs, bridging post-generation feedback and constrained decoding. Its sealor transformation enables existing compilers to diagnose partial programs while supporting formal guarantees and evaluation on Rust tasks.

  • Background and Related Work: Post-generation feedback waits for complete files, allowing tokens after the first unrecoverable error to be wasted and presenting accumulated diagnostics in a potentially hindered batch.Constrained decoding intervenes earlier but requires substantial language-specific reimplementation for expressive static semantics.
  • This Work: Generative Compilation: Generative compilation checks partial programs during generation and provides compiler-style diagnostics, combining intermediate feedback with off-the-shelf compiler guarantees.It is positioned as a middle ground between post-generation feedback and constrained decoding.
  • This Work: Generative Compilation: A sealor completes a partial program with missing syntax and well-typed placeholders so an existing compiler can check it.The central challenge is preserving faithful feedback while ensuring compiler rejection reflects a genuine inability to complete the partial program.
  • This Work: Generative Compilation: A lightweight, mostly syntax-guided sealor avoids reimplementing the target type system, with guarantees proved on Featherweight Rust and mechanized fully in Lean.The methodology is then carried to real Rust.
  • Evaluation: Across seven frontier black-box and open-weight LLMs and two repository-level Rust tasks, generative compilation reduces compiler errors and improves functional correctness in most model-task configurations.The tasks are C-to-Rust translation and generation against recently updated library APIs.

2 Motivation for Generative Compilation

Existing compiler feedback checks only completed programs, while constrained decoding acts during generation but requires impractical prefix-checking infrastructure and can silently force poor continuations. Generative compilation combines partial-program intervention with textual compiler diagnostics by sealing partial programs into compilable ones, providing relevant feedback four and a half lines earlier in the running example.

  • Post-Generation Compiler Feedback: Post-generation compiler feedback guarantees language membership only after a full program is generated, then asks the model to retry with the compiler diagnostic when checking fails.The compiler returns a Boolean verdict and textual diagnostic, including explanations such as failed type checks and possible fixes.
  • Constrained Decoding: Constrained decoding rejects tokens whose partial output cannot be extended to a valid program, ensuring every generated prefix remains extendable to some valid program.It intervenes during autoregressive decoding through a prefix checker rather than waiting for a complete program.
  • Constrained Decoding: Prefix checking is difficult because it reasons about partial programs, cannot directly reuse conventional compiler infrastructure, and often requires reimplementing language semantics for general-purpose languages.Matching a full compiler’s behavior for prefix checking is described as impractical for general-purpose programming languages.
  • Constrained Decoding: Constrained decoding silently filters rejected tokens, cannot explain the rejection or revise the existing prefix, and may force low-probability continuations that degrade global generation quality.In the running example, rejecting the token . leaves a use-before-definition path as the only way forward.
  • Generative Compilation on the Running Example: Generative compilation seals partial programs into complete programs for conventional compilation, maps diagnostics back to the partial source, and provides relevant feedback four and a half lines earlier than post-generation feedback.The model sees the partial program and mapped diagnostic, not the sealed program, and produces the same repaired program as post-generation feedback.

3 Generative Compilation

Generative compilation checks whether partial programs can admit valid completions while retaining compiler diagnostics, by sealing them into complete programs for conventional compilers. Its design prioritizes completeness, integrates with black-box autoregressive generation, and uses diagnostic-triggered revision.

  • Generative Compilers: Definition: A generative compiler checks whether a partial program admits a valid completion and returns a Boolean verdict with a textual compiler diagnostic.Unlike constrained decoding, it retains compiler diagnostics for rejected prefixes.
  • Sealors: Definition: A sealor lightweightly closes unfinished structure so an existing compiler can process partial programs, avoiding costly reimplementation of semantic checking.The induced generative compiler is GC,S(c) = C(S(c)); diagnostics can be mapped from sealed-program spans back to the original prefix.
  • Sealors: Completeness and Soundness: Sealor completeness and soundness lift to the induced generative compiler when the underlying compiler is exact: valid continuations are not rejected, and dead ends are not accepted.Completeness requires sealing every extendable prefix into a valid program; soundness requires that a valid sealed program have a valid continuation.
  • Target Guarantees: Global Completeness and Selective Soundness: Generative compilation prioritizes completeness over soundness because rejecting an extendable prefix can confuse generation, whereas rejection enables diagnostic-guided revision.Exact prefix checking requires both global properties and is undecidable in general for expressive semantic constraints [34].
  • LLM Integration: The system streams prefixes to a concurrent generative compiler that sends rejected prefixes and diagnostics back as augmented prompts, requiring only plain-text communication with black-box LLMs.Generation restarts on rejection, while latest-wins validation coalesces prefixes and concurrency avoids blocking token sampling.

4 FR: A Core Calculus for Rust

The paper uses Featherweight Rust (FR) as a compact, source-close calculus for formally defining and analyzing generative compilation while retaining Rust’s core ownership and borrowing features. FR simplifies the metatheory through syntactic moves, lexical lifetimes, and flow-sensitive typing while preserving soundness guarantees.

  • Why a Core Calculus: FR satisfies the need for a compact Rust formalization that remains close to source syntax while capturing prominent language features.Existing formalisms are either too abstract or too elaborate for this purpose; FR provides a concise, sound alternative [15].
  • Why FR: FR preserves copy and move semantics, mutable and immutable borrows, and lexical lifetimes while supporting a concise type-soundness argument.Unlike modern Rust’s non-lexical lifetimes, FR ends borrows according to enclosing lexical blocks, simplifying the metatheory while remaining sound.
  • Syntax: FR makes copy versus move syntactic, allowing operational semantics to remain type-independent while typing restricts copy expressions to copyable types.In the mechanization, unit, integers, and shared borrows are copyable, whereas mutable borrows and boxes are not.
  • Syntax: FR represents lexical lifetimes explicitly and names each borrowed lval in reference types, enabling borrow checking through lifetime nesting and lval overlap or conflict tracking.Its reference types distinguish shared and mutable borrows, while restricting targets to single lvals supports cycle-freedom.
  • Typing: FR’s main typing judgment threads environments from input to output, marking moved-out slots and incorporating declarations, assignments, lifetime validity, and partial-type shape checks.This flow-sensitive structure rejects later uses of moved values and relies on auxiliary judgments for lvals, well-formedness, and shape compatibility; the rules are summarized in Fig. 8.

5 Instantiating Generative Compilation on FR

The section instantiates generative compilation for FR with a lightweight, syntax-guided sealor SFR whose implementation and proofs are mechanized in Lean. SFR is globally complete and sound at statement boundaries, yielding exactness there.

  • Partial syntax and realization: Partial syntax models autoregressive prefixes by allowing one component of an otherwise full FR term, lvalue, or value to remain partially generated.Realization relates such prefixes to full programs obtainable by extending the unfinished frontier without revising earlier text.
  • Sealor construction: SFR defines a total syntax-guided transformation from partial FR terms to full terms, preserving generated structure when it exposes useful typing obligations and abstracting unresolved obligations.Unfinished fragments that remain ambiguous or lack enough information may seal to the unit value ε, while recursive cases preserve relevant subterms.
  • Completeness proof: The completeness proof establishes that whenever a partial term realizes a well-typed program, sealing it with SFR also produces a well-typed term.The theorem is stated for arbitrary typing environments, store typings, and lifetimes, enabling application to intermediate terms within larger programs.
  • Global completeness: SFR is globally complete for FR, including arbitrary input strings, and this lifts to completeness of the generative compiler GFR.The result follows from SFR’s completeness together with an exact FR compiler.
  • Statement-boundary soundness: At statement boundaries, SFR is sound for FR and therefore exact; the same exactness guarantee holds for GFR.This applies to partial programs whose completed statements precede the next generation frontier.

6 From FR to Real Rust

The Rust sealor SRS transfers FR’s lightweight, syntax-guided sealing methodology to real Rust while adapting to Rust’s larger syntax and typing behavior. It uses context-sensitive placeholders, future-aware error handling, and diagnostic projection to preserve completeness and provide useful feedback on partial programs.

  • Design principles: SRS preserves generated structure, recursively seals the partial frontier, and targets global completeness with selective soundness while handling Rust-specific constructs.Unlike FR, SRS addresses constructs without FR counterparts and uses informal per-feature arguments rather than mechanized proofs.
  • Design principles: SRS uses separate statement and expression sealors, selecting the expression sealor when context infers a type and the statement sealor otherwise.The statement sealor closes partial statements into statement lists, while the expression sealor produces an expression with an unconstrained type.
  • Placeholders: holediv() preserves completeness for divergent control-flow branches, while holeval() supplies a context-inferred value without exposing never-type fallback errors.holediv() is implemented with panic!() and has type !; holeval() uses a generic helper whose call has inferred return type T.
  • Diagnostics: SRS suppresses errors that may depend on later-generated code and projects rustc diagnostics from the sealed program back onto the original partial program.This handles cases such as incomplete trait implementations, later-declared functions, and ambiguous expression types, while positional maps preserve correspondence for re-rendered diagnostics.
  • Expression and statement rules: For conditionals, SRS is complete because recursively sealed branches inherit completeness and appended holediv() introduces no branch-type obligation.Because holediv() diverges, rustc excludes it from branch-type merging, so it cannot constrain the live branch.

7 Experimental Evaluation

The evaluation across seven coding models and two repository-level Rust tasks shows that generative compilation reduces compiler errors and runtime while detecting unrecoverable mistakes early and focusing diagnostics on their causes.

  • Models and Agent Harness: The study evaluates seven coding models twice per task using a deterministic harness across Translation and UpdatedAPI, reporting compiler error rate and functional correctness.Translation uses 20 complex CRUST-Bench instances, while UpdatedAPI tests adaptation to recently changed Rust library APIs.
  • Limitations: The evaluation cannot compare against Rust constrained decoding because no implementation is known, and GC’s global-completeness guarantee does not meet constrained decoding’s global-soundness requirement.Building a real-Rust constrained decoder would be highly complex and costly.
  • Decreased Runtime: GC lowers average runtime overhead from 233 seconds (+283%) with post-generation feedback to 135 seconds (+170%) over LLM.For Qwen 9B on Translation, runtime falls from 879 to 357 seconds per sample.
  • Mitigated Error Snowballs: GC resolves 55.4% of tasks correctly within its early-feedback phase, while 85.3% complete without switching back to post-generation feedback.Interrupting at the first unrecoverable error also yields more focused reports: 65% contain only one or two distinct diagnostics, averaging 5.5 diagnostics per message.
  • Errors Are Detected Long before File Completion: GC detects errors at a mean of 33.3% of file generation, nearly matching the 32.7% timing-free upper bound and avoiding the remaining 66.7% of unrecoverable output.Its median detection delay is 3 lines after the eventual error’s primary span, versus 14 lines for GCfn and 89 lines for post-generation feedback.

8 Discussion and Future Work

The discussion identifies limitations in modeling diagnostics and hand-written sealor construction, while outlining opportunities to decouple generative compilation from its fixed invocation loop. The implementation currently renders feedback in rustc’s format because models are assumed to be most familiar with it.

  • Modeling Error Messages: The formal completeness and soundness results cover only the ok verdict, not whether err reflects a genuine defect rather than a sealing artifact.The authors report observing this behavior empirically and suppressing sealing artifacts, but do not formalize the property.
  • Modeling Error Messages: The current rendering follows rustc diagnostic formatting because the authors assume models are most familiar with that feedback from their training corpus.This follows established formatting used for programmers and, more recently, AI coding agents [21].
  • When and How to Invoke Generative Compilation: Generative compilation is currently invoked after each completed check, with rejection triggering prompt augmentation and generation restart.Concurrent validation makes this loop practical by running alongside token generation with modest overhead; decoupling it could enable alternative invocation strategies.
  • Automating Sealor Construction: Sealor construction for both FR (§5) and Rust (§6) is hand-written, motivating synthesis from a language specification or reference implementation.Automation must search for rules that are both complete and strongly sound.

9 Related Work

Prior work uses compiler feedback, constrained decoding, syntax and types, and typed holes to support program generation or completion. Generative compilation differs by applying compiler-oriented reasoning to incomplete LLM-generated programs without relying on sampling restrictions or language extensions.

  • Compiler Feedback: Compiler feedback provides both guarantees, including memory safety and information-flow security, and revision guidance through error messages.
  • Constrained Decoding: Constrained decoding checks programs during autoregressive generation by restricting next-token choices during sampling, whereas generative compilation uses compiler feedback on partial programs.Local token-level constraints can harm final programs [4], while global constraints still operate at the sampling level [12] [25].
  • Constrained Decoding: Beyond syntax, constrained decoding requires significant reimplementation [31] [34], and incomplete language subsets can degrade performance [6], leaving no comparable technique for Rust borrow and lifetime properties.
  • Syntax- and Type-Guided Program Construction: Syntax- and type-guided program construction has long supported search, especially synthesis from formal specifications, while this work targets LLM-based code generation.
  • Typed Holes: Typed holes make incomplete programs well-typed so static type contexts can be extracted [7], but require holes to become first-class citizens through a language extension.Generative compilation instead uses placeholders such as 𝜀for FR (§5.2), holediv(), and holeval() for Rust (§6.1).

10 Conclusion

Generative compilation brings compiler feedback into intermediate LLM code-generation steps by sealing partial programs into compiler-checkable complete programs. Formalization and evaluation show that this approach supports sound prefix checking for Rust and improves generation outcomes through early diagnostics.

  • Generative compilation seals partial programs into complete programs that standard compilers can check, enabling intermediate feedback with black-box models, real compilers, and rich error messages.
  • Sealors formalize this approach with mechanized completeness and soundness guarantees in Featherweight Rust, and extend it to real Rust with Rust-specific structural handling.The real-Rust prefix checker handles expression and statement structure, control flow, placeholders, and future-dependent compiler errors.
  • Generative compilation detects type, borrow-check, and lifetime errors near their sources and before file completion, reducing non-compiling outputs and improving functional correctness over standard post-hoc feedback.

A Experimental Details · A.1 Construction of UpdatedAPI · A.2 Construction of Translation

The experimental datasets target Rust coding under API evolution and difficult C-to-Rust translation settings. UpdatedAPI samples recently version-bumped crates with public API changes, while Translation focuses on unsolved CRUST-Bench tasks and evaluates file-level translations in repository context.

  • A.1 Construction of UpdatedAPI: UpdatedAPI samples the 100 most downloaded Rust crates with minor or major version bumps during the preceding six months.The sampling was performed at the time of writing.
  • A.1 Construction of UpdatedAPI: Codex with GPT 5.3 filters the sampled packages for public-facing API changes during their version bumps.
  • A.2 Construction of Translation: Translation uses the CRUST-Bench benchmark [20], which contains 100 C-to-Rust translation tasks.
  • A.2 Construction of Translation: GPT 5.3 and Claude Opus 4.8 solve around 80 CRUST-Bench tasks zero-shot without compiler feedback, leaving 20 tasks for focused evaluation.
  • A.2 Construction of Translation: Each selected translation task, originally covering an entire library, is divided into separate tasks for each library file.
  • A.2 Construction of Translation: Final evaluation embeds each generated file into a repository rather than assessing it in isolation.

A.3 Experimental Setup Details

The experiments use a minimally patched Rust 1.95.0 compiler to expose type-inference information during generation. Models are accessed through provider-specific APIs, with temperature 0.6 except for Claude Opus 4.8, whose endpoint does not permit temperature control.

  • Rust Implementation: The Rust 1.95.0 implementation adds a minimal compiler patch exposing defined identifiers, available functions and methods, and expected parameter counts from type inference.The changes are supplied as a code patch with the implementation.
  • Hyperparameters: Qwen 3.5, GLM 5.2, and Kimi K2.7 use OpenRouter, while Gemini 3.5 Flash, GPT 5.3 Codex, and Claude Opus 4.8 use provider-specific APIs.Gemini uses Google Vertex, GPT 5.3 Codex uses the OpenAI responses API, and Claude Opus 4.8 uses Anthropic’s API.
  • Hyperparameters: All models except Claude Opus 4.8 use temperature 0.6; Opus omits temperature because its API endpoint does not support setting it.The UpdatedAPI task has a maximum output of 20,000 tokens.

A.4 Detailed Analysis of Detected Error Kinds · A.5 Restart Budget and Token Limit

The analysis shows that rollback errors are dominated by type mismatches, while restart-budget results indicate rapid early gains followed by flattening, suggesting the evaluated budgets capture most attainable compilability improvements.

  • A.4 Detailed Analysis of Detected Error Kinds: Rollback diagnostics span syntax errors, type violations, borrow-check and lifetime violations, and other reports lacking an associated error code.The resulting error-kind distributions are shown per dataset in Fig. 13.
  • A.4 Detailed Analysis of Detected Error Kinds: Type mismatches (E0308) are the most frequent rollback error on both datasets, comprising 38.2% of Translation reports and 37.4% of UpdatedAPI reports.The error taxonomy covers syntax, type, borrow-check and lifetime, and other errors.
  • A.4 Detailed Analysis of Detected Error Kinds: On Translation, unknown-field accesses are the next reported error category at 9.5% (E0609), reflecting difficulties porting C data layouts to Rust skeletons.This follows the 38.2% share of E0308 type mismatches.
  • A.4 Detailed Analysis of Detected Error Kinds: On UpdatedAPI, wrong-argument-count calls account for 18.1% (E0061), followed by wrong generic-argument counts at 7.2%.These are the subsequent errors reported after E0308 mismatches on UpdatedAPI.
  • A.5 Restart Budget and Token Limit: Across pooled generations, both methods improve steeply in compilable outputs during the first few restarts before the gains flatten.The analysis pools all evaluated models on both datasets and measures compilability attainable within a given restart count.
  • A.5 Restart Budget and Token Limit: Raising the restart budget from 15 to 20 increases the fraction of compilable outputs, with budgets set to 15 restarts for UpdatedAPI and 20 for Translation.The reported token limits are 20,000 for UpdatedAPI and 30,000 for Translation.

B End-to-End Example · C Inference Prompts

The end-to-end example shows Generative Compilation catching a Rust lifetime error early and enabling a correct repair. The inference prompts specify grading prefixes, task-specific inputs, and diagnostic feedback for both Generative Compilation and Post Compilation.

  • B End-to-End Example: Both methods’ compilable-output fractions flatten well before 20 restarts, while generated output lengths remain far below the token limit.
  • C Inference Prompts: Inference sends one user message containing the dataset prompt, with the grading prefix prefilled for open-weight models or requested explicitly for black-box models.
  • C.1 Generic Inference Wrappers: After Generative Compilation rejects partial output, the prompt history adds it as an assistant message and appends a user message containing rendered compiler diagnostics before restarting generation.
  • C.2 UpdatedAPI: UpdatedAPI prompts provide crate files, tests, and comments while asking the model to implement only the incomplete interface file, instantiated as src/lib.rs.
  • C.3 Translation: Translation prompts provide the C sources and the incomplete Rust interface of the target file, with the required prefix instruction appended for black-box inference.
  • B End-to-End Example: Generative Compilation rejects a temporary borrow with E0716 at line 4 of a 32-line function, after which Claude Opus 4.8 introduces a longer-lived binding and generates semantically valid code.The example concerns the UpdatedAPI task for rustls-webpki and demonstrates early feedback preventing substantial unnecessary generation.
  • C.3 Translation: Post Compilation instead adds the rejected complete output and rendered diagnostics to the prompt history, then permits full replacement files, patches, or both before rechecking.
Loading 2607.13921v2…