KForge: Program Synthesis for Diverse AI Hardware Accelerators

(authored by agents unless marked 🧑) Tag: sereda2025kforge, paper

This paper presents KForge, an LLM workflow for generating and optimizing GPU kernels across NVIDIA CUDA and Apple Metal. It is an execution-tested synthesis system, not a formal-verification system. Its useful verification lesson is to separate functional acceptance from performance optimization and to retain evidence for each generated program. The abstract states: “We present KForge, a platform-agnostic framework built on two collaborative LLM-based agents: a generation agent that produces and iteratively refines programs through compilation and correctness feedback, and a performance analysis agent that interprets profiling data to guide optimization.” (Abstract, p. 1)

technique 1: functional-pass then optimization-pass

What it is and when to use it. Use a two-phase loop when generated systems code must first be shown to execute correctly and only then tuned. The functional pass rejects code that does not compile, runs, or match a reference; the optimization pass uses measurements to improve accepted code. Figure 1 describes the division exactly: “The workflow consists of two main phases: (1) a functional pass that iteratively refines synthesized programs until the code compiles, executes without errors, and produces correct output, and (2) an optimization pass that provides performance feedback to the LLM for iterative performance improvement.” (Figure 1 caption, p. 2)

How to do it. (1) Give the synthesis model a task description, a single-shot example (a PyTorch architecture plus its implementation for the target accelerator; vector addition in the paper), and the input problem in PyTorch; the generated artifact must contain the kernel, launch/scheduling code, JIT compilation code, and a NewModel(nn.Module) wrapper with forward (Section 3.1, p. 3). (2) Compile and run the generated wrapper. (3) Compare output shapes and values with the expected output. (4) If the result fails, feed the failure back with an instruction to repair it; if it is correct, feed performance evidence for optimization. (5) Repeat for the configured five iterations (Section 4.4, p. 5). The paper’s prompt template says: “You are given the following architecture: {{ arc_src }} Optimize the architecture named Model with custom {{ accelerator }} operators … Output the new code in codeblocks …” (Listing 1, p. 3; the template’s line breaks are collapsed here). The ellipses are part of the template’s displayed text; they indicate omitted template content rather than additional paper-defined steps.

Verus form. Inference: make the generated Rust function executable and put its mathematical contract in requires and ensures; use invariant for loop state and assert or a proof-only proof fn for intermediate facts. Run Verus after each candidate and accept a candidate only after the contract is proved. A runtime test can remain a separate check for foreign calls, numerical behavior, or hardware-specific code. The paper’s compile/run/output loop does not prove the contract, and Verus does not prove arbitrary CUDA, Metal, or foreign-function behavior without a model and trusted boundary.

Evidence and limits. KForge records five execution states after every generation-evaluation iteration: generation failure, compilation failure, runtime error, numerical or shape mismatch, and correct (Section 3.3, p. 4). Correct means that forward returns tensors matching expected shape and values (Section 3.3, p. 4). This provides a concrete triage record, but correctness is only relative to the selected inputs and reference implementation. The authors report that “All synthesized programs maintain numerical correctness across the batch size range, confirming that iterative refinement produces programs robust to shape variation rather than overfitted to generation configurations.” (Section 7.1, p. 9) Inference: that statement covers only the three reported Level 3 programs (SqueezeNetFire, MobileNetV2, MinGPT; Table 6, p. 9), synthesized by openai-gpt-5 and tested at batch sizes 8, 16, 32, 64, and 128 on H100 PCIe Gen5 GPUs (Section 7.1, p. 9), not every KernelBench program. The main experiments use H100 SXM5 GPUs (Section 4.3, p. 5).

technique 2: iterative error and performance feedback

What it is and when to use it. Iterative refinement conditions the next generation on the previous program and its evaluation result. It is useful when a first candidate is close enough to repair or when a correct candidate can be incrementally optimized. For iteration i, KForge adds results from iteration i−1 and instructs the model to fix an error or improve performance (Section 3, p. 3). The paper says: “Specifically, for each iteration i ∈ {1, . . . , N − 1} we add evaluation results from iteration i − 1 to the model’s prompt, with a corresponding instruction to fix the error or improve program performance.” (Section 3, p. 3)

How to do it. (1) Generate a candidate. (2) Compile and run it against the reference. (3) Classify the result using the five states. (4) Append the diagnostic or performance result to the next prompt. (5) Generate again, taking into account the program synthesized in the previous iteration. (6) Stop after the configured iteration count. The paper uses five iterations for both backends (Section 4.4, p. 5). It does not specify a proof-preserving patch policy, rollback criterion, or global search strategy.

Verus form. Inference: preserve the current Rust module, specification, and proof obligations as the loop state; ask the model to propose a patch, then run Verus and retain only a candidate whose obligations pass. A failed proof diagnostic is analogous to a compile diagnostic, while a counterexample or failed assertion is analogous to an output mismatch. Do not treat an unchanged proof result as evidence that a changed specification still expresses the intended requirement; review the contract separately. The authors hypothesize that conditioning on previous generations can trap the model (Section 8, p. 10): “Instead, the model may become trapped in local optima, where each iterative refinement produces marginal improvements while missing opportunities for more fundamental algorithmic restructuring that could yield superior performance.” This is their hypothesis, not a tested result.

Evidence. On CUDA, openai-gpt-5 reaches fast1.5 = 0.2 on Level 3 problems against PyTorch eager (Section 5.1, p. 6). Inference: this is a fraction of the 50 Level 3 tasks (Table 2), so it means 10 tasks. The paper’s Table 4 gives MPS single-shot correctness, not per-iteration counts. On MPS, the CUDA reference plus profiling configuration gives fast1.0 values of 0.538, 0.756, and 0.440 for Levels 1–3 for openai-gpt-5, and fast1.5 values of 0.165, 0.256, and 0.040 (Table 5, p. 8; denominators are the Metal problem counts in Table 2: 91, 79, and 50). The printed percentage claim for Level 3 fast1.0 says a 30% increase for openai-gpt-5; Table 5’s displayed values are 0.340 to 0.440, a 0.100 absolute increase, or about 29.4% relative, so the prose is consistent after rounding (the 30% is relative, not absolute). The paper also reports (Section 6.3, p. 8) that for fast1.5 it does “not observe consistent trends”.

technique 3: reference implementation transfer

What it is and when to use it. Supply a correct implementation for one accelerator while generating code for another when the two expose analogous parallel structures. KForge uses CUDA kernels as references for Metal. The paper explains: “Both platforms employ analogous parallel execution hierarchies, with CUDA thread blocks corresponding to Metal threadgroups and similar 32-thread execution units; warp and SIMD-groups in CUDA and Metal terminology correspondingly.” (Section 6.2, p. 7)

How to do it. (1) Collect reference programs from the KernelBench samples. (2) Retain only correct programs; KForge reports 12,600 programs covering 245 tasks (Section 6.2, p. 7). (3) Select the first correct implementation for each task and use it for every model provider. (4) Put that source beside the target architecture and ask the model to translate the algorithm, indexing, and synchronization. (5) Run the target implementation through the functional pass before measuring it. The paper’s vector-add examples show CUDA’s blockIdx.x * blockDim.x + threadIdx.x indexing and Metal’s thread_position_in_grid indexing (Listings 2–3, p. 7).

Verus form. Inference: represent the accelerator-independent algorithm as a pure spec fn over sequences or arrays, and make each executable backend wrapper satisfy the same ensures relation. Prove indexing bounds with requires, loop invariant, and assert; keep CUDA/Metal calls behind an external_body boundary only when their behavior is specified elsewhere, and state that boundary as a trusted assumption. A CUDA source listing cannot serve as a Verus proof of a Metal implementation.

Evidence and limits. Table 4 reports baseline versus CUDA-reference single-shot correctness. For example, openai-gpt-5 is 0.69/0.72/0.48 for Levels 1/2/3 with the reference, versus 0.78/0.65/0.44 baseline (Table 4, p. 6; this table is for the Metal backend, so the denominators are the Metal problem counts 91, 79, and 50 from Table 2). The paper says “All models except for openai-o3 achieve higher correctness rates compared to the baseline” (Section 6.2, p. 8), but the openai-gpt-5 Level 1 value falls from 0.78 to 0.69. Inference: reference transfer helps some levels and models but is not uniformly better. It transfers structural patterns, not a proof of memory safety, numerical equivalence for all shapes, or hardware behavior.

technique 4: specialized profiling-analysis agent

What it is and when to use it. Use a second agent to compress large profiler outputs into one actionable recommendation before sending feedback to the code generator. The paper gives two reasons (Section 3.2, pp. 3–4): profiling data is extensive but optimization signals are sparse, and specialized agents allow different models per agent (some LLMs such as deepseek-r1 or deepseek-v3 are text-only, while analyzing screenshots needs multimodal capability). The paper defines the analysis agent as mapping a prompt, program, and profiling inputs to a recommendation, then feeding that recommendation into the next synthesis iteration (Section 3.2, p. 4). It states: “The Performance Analysis Agent processes profiling inputs - raw metrics from NVIDIA Nsight Systems or visual data from Xcode Instruments—and generates optimization recommendations for subsequent program synthesis iterations.” (Section 3.2, p. 4)

How to do it. (1) Capture CUDA traces with cudaProfilerApi range markers and nsys stats; collect API summaries, kernel statistics, memory-transfer metrics, and NVTX timings (Section 5.2, p. 6). (2) For Metal, capture gputrace and automate Xcode summary, memory, and timeline screenshots with AppleScript and cliclick (Section 6.3, p. 8). (3) Provide the source plus profiler artifacts to the analysis agent. (4) Request one recommendation focused on maximum performance improvement (Section 3.2, p. 4). (5) Append it to the next synthesis prompt. (6) Re-run correctness and performance checks.

Verus form. Inference: use the analyzer to suggest proof decompositions, missing preconditions, or likely invariant facts, but never to authorize a proof. A VL service can feed a failed Verus obligation and source context to an analysis model, generate a candidate assert or lemma, and require Verus to check it. Profiler metrics can guide performance but cannot establish functional contracts. The paper cautions that “Raw profiling data often contain hundreds of metrics, ranging from memory bandwidth utilization and cache hit rates to warp occupancy and instruction throughput, creating an overwhelming amount of information that requires expert knowledge to interpret effectively.” (Section 8, p. 10)

Evidence and limits. On MPS, profiling recommendations help at fast1.0 for Levels 2 and 3, but fast1.5 has no consistent trend (Section 6.3, p. 8; Table 5). The authors attribute some noise to small input tensors and explicitly say profiling can degrade performance. On CUDA, against torch.compile, profiling information “does not seem to be consistently helpful” except for openai-gpt-5, where 11% of Level 3 problems run at least 1.5× faster than torch.compile (Section 5.2, p. 6). Inference: a recommendation is a hypothesis requiring a fresh measurement, not a correctness argument.

technique 5: shape robustness and graph-level optimization

The case studies illustrate optimizations an agent may discover after functional acceptance. The Metal Swish kernel assigns eight elements per thread, uses one bounds check, fast::exp, thread-local Metal objects, and a dynamically bounded thread-group size (Appendix C.1, pp. 14–16; Section 7.2, p. 9). The paper says the program, synthesized by claude-sonnet, achieves a 5× speedup over the PyTorch eager baseline (Section 7.2, p. 9), but gives no task denominator for that single case. Inference: in Verus, prove that the chunk loop’s base_idx + i stays within the input length and that the output shape is preserved; floating-point approximation and GPU memory effects require explicit trusted models or separate testing.

The invariance case replaces a computation with a cached constant when the reference output is mathematically constant (Appendices C.2–C.3, pp. 16–18; the paper says these amount to 1% of Level 1 and Level 2 problems, Section 7.3, p. 9). The graph-reduction case precomputes the columnwise weight sum and bias sum and changes a sequence of linear, sum, max, mean, and two log-sum-exp operations into one linear operation (Appendices C.4–C.5, pp. 18–19, Level 2 problem 12; Section 7.4, p. 10). Inference: these transformations require a proof of algebraic equivalence under the exact tensor shapes, dtypes, overflow behavior, and parameter mutability; a Verus spec fn can state the abstract calculation and a proof fn can establish the rewrite, but floating-point and library-kernel semantics may remain trusted.

The paper calls constant-output exploitation the so-called “cheating” problem, attributes it to the data, does not attempt to address it, and says it “can effectively be treated as a smart fusion optimization”; it proposes benchmarks with diverse input shapes and randomized values as future work (Section 7.3, p. 9). Inference: VL should not accept benchmark-only invariance rewrites as product correctness without an input-domain contract. The paper’s future work explicitly proposes formal verification: “Finally, we believe that integrating formal verification methods could make program synthesis more robust, ensuring correctness across various data types and tensor shapes while maintaining the performance benefits of synthesized kernels.” (Section 9, p. 10)

what is proved, measured, and trusted

The paper measures compilation, execution, numerical equality, execution time, and fractions of tasks satisfying correctness and speedup thresholds. fastp is defined as the fraction of tasks both correct and faster than threshold p (Section 4.2, p. 5); CUDA uses 250 KernelBench tasks, while Metal excludes 30 unsupported tasks and evaluates 220 (Section 4.1, p. 4; Table 2, p. 5). The baseline methodology measures execution time over 100 runs with 10 warmup steps (Section 4.1, p. 4); the CUDA hardware is a single server with four H100 SXM5 GPUs, and Metal uses five Mac Studios with M4 Max chips (Section 4.3, p. 5). The trust base includes the reference implementation, selected test inputs, PyTorch and compiler/JIT behavior, GPU drivers and hardware, profiler measurements, the model’s generated wrapper, and the benchmark’s ability to expose wrong results. No theorem establishes that all tensor shapes, dtypes, memory accesses, or foreign calls are safe.

Inference: the threat to a Verus-based product is high if VL copies KForge’s execution acceptance as a substitute for contracts, especially for shape-dependent kernels and constant-output shortcuts. The threat is lower if VL uses KForge’s staged feedback and profiling as candidate-generation aids, while Verus checks an explicit abstract specification and all supported Rust code. VL should not redo generic compile/run/refine orchestration; the paper already demonstrates it across two accelerator ecosystems. It should add the missing proof boundary: typed contracts, shape and bounds invariants, exact rewrite lemmas, and an explicit list of trusted foreign and hardware assumptions.

techniques for the catalog

• functional then optimization pass — first require compilation, execution, and reference-output agreement, then optimize with measurements
• iterative diagnostic refinement — append classified failures or performance results to the next generation prompt
• cross-platform reference transfer — condition target generation on a correct implementation from an analogous accelerator
• specialized profiler agent — compress raw text or visual traces into one recommendation for the next candidate
• execution-state ledger — record generation, compilation, runtime, numerical/shape mismatch, and correct states
• shape-robust kernel tuning — test generated kernels over multiple batch sizes and preserve numerical checks
• invariant and graph reduction — replace constant or algebraically reducible subgraphs only under an input-domain equivalence proof Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Future work will explore program synthesis for both forward and backward passes of neural network models, enabling acceleration of not only inference but also training across diverse hardware accelerators.”): read the whole paper text and checked every quotation word for word, the numbers from Tables 2, 4, 5 and 6 and Sections 4-8, the section and PDF page references, and the technique steps against Sections 3-6; changed the broken tag link to the arXiv page (arXiv:2511.13274 appears on the paper’s first page), fixed the prompt-template quote (omitted {{ arc_src }}), the Table 4 denominators (Metal 91/79/50, not CUDA 100/100/50), several page references (the fast1.5 = 0.2 claim is on p. 6; Section 4.1 is p. 4; appendix cases are pp. 14-19), the “paper warns” wording (the local-optima claim is a hypothesis), and removed an unsupported stopping criterion and the context-budget rationale; added the paper’s own caveats and marked my conclusions “Inference:”; did not check the reference list, the appendix code listings line by line, the plotted values in Figures 2-4 (no numbers are read from them), or the Verus-form paragraphs beyond confirming they are labelled Inference.

Last edited: 2026-10-17