It is shown that generative compilation reduces non-compiling outputs and improves functional correctness, relative to standard post-generation feedback, by detecting a broad range of errors close to their source and early during generation, thereby reducing errors cascades and enabling focused diagnostics.
Abstract
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.
Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.
Minh Le-Anh, Cuong Chi Le, Tien N. Nguyen· 0 citations
Differential compiler testing requires automatically generated programs that are not only diverse and bug-revealing, but also semantically well-defined and reproducible. Rule-based generators provide strong validity guarantees but offer limited control over semantic variation, while large language models (LLMs) can synthesize expressive programs without principled mechanisms for balancing competing testing objectives. This paper proposes LMOEC, a constrained multi-objective evolutionary framework that integrates code language models as semantic genetic operators within an NSGA-II search process. Instead of using the LLM as a one-shot generator, we employ it for population initialization, crossover, and mutation at the program level, enabling semantics-aware recombination while preserving strict admissibility constraints. Compiler test generation is formulated as a multi-objective optimization problem that simultaneously promotes structural diversity, cross-configuration output inconsistency, semantic complexity, and robustness to mutation. A constraint-driven acceptance pipeline enforces syntactic validity, deterministic execution, bounded runtime, and avoidance of undefined behavior before evolutionary selection. By maintaining a Pareto front of non-dominated programs, LMOEC preserves multiple high-value test archetypes reflecting different trade-offs between bug exposure and reproducibility. The framework demonstrates how expressive code models can be systematically embedded into evolutionary multi-objective optimization for reliability-critical software testing.
Lang Hong Nguyet Anh, Ho Viet Duc Luong, Vu Van An· Annual Conference on Genetic...· 0 citations
The paper investigates the possibility of predicting function-inlining decisions in compact compilers, source-to-source tools, and interpreters where the reuse of GCC or LLVM optimization infrastructure is impractical. The relevance of this work is determined by the need to transfer mature inlining heuristics to systems with limited compiler infrastructure, restricted runtime dependencies, and reduced access to target-specific analysis. Existing production compilers already contain strong inliners, but their decisions depend on internal intermediate representations (IRs), pass ordering, target models, and analysis stacks that are difficult to reproduce in lightweight systems. To overcome these constraints, we propose a portable inlining-prediction framework. Production compiler diagnostics serve as supervision; a separate extractor reconstructs caller-callee callsites, prepares sterile source snippets, normalizes them into a universal AST, optionally lowers them to a lightweight structural IR, and exports scalar features for model training. Thus, a trained predictor can be emitted as ordinary C code without a compiler-runtime dependency. To evaluate the proposed framework, we constructed a dataset comprising 336,938 callsites from fifteen open-source C projects, including 79,287 compiler-reported inline events. A comparison of several tabular models is performed using project-aware validation. Under leave-one-project-out validation, CatBoost reaches ROC-AUC 0.928 and PR-AUC 0.713; after threshold tuning, F1 improves from 0.670 to 0.729 and the false-positive rate drops from 0.192 to 0.084. Feature analysis shows that most signal is concentrated in source locality, explicit inline intent, callee size, side effects, branch and call structure, signature shape, and callsite argument shape.
Compilers for structured data pipelines, often specified using domain-specific languages such as P4, are notoriously difficult to validate. We introduce compilomorphic fuzzing, a new validation approach that turns a compiler into its own test oracle via structure-preserving transformations over programs and structured inputs. The core idea is to generate pairs of semantically equivalent but structurally distinct inputs (e.g., packets) and programs (e.g., pipeline specifications), and then assert that the compiler's observable behaviour remains invariant. Any deviation exposes a deep semantic bug. We present the formal basis for this approach, compilomorphism, and a prototype fuzzing framework that operationalises it, establishing a practical, model-free foundation for validating compilers in critical DSL domains.