PaperlayerView exact revision on arXiv

Source-linked AI summary

T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework

Zahra Fazel, Sunanda Gamage, Shayan Shirahmad Gale Bagi, Amir H. Ashouri, Tomasz S. Czajkowski, Bryan Chan, Reza Azimi, Yaoqing Gao

arXiv:2608.14953v1cs.AIcs.CLcs.LGcs.PFcs.PL

TL;DR

LLMs struggle to perform broad code optimizations and verify transformed-code correctness. T-LLM Compiler combines LLM transformations with traditional compilers and iterative verification, achieving an 83% code-generation success rate and 26.7% speedup on PolyBench/C.

  • Problem

    Compilers are limited in their ability to automate significant optimizations because increasingly complex low-level transformations require substantial expertise and knowledge.

  • Method

    T-LLM Compiler uses LLM-based optimizations with syntax, symbolic, and semantic verification in an iterative framework alongside traditional compiler tools.

  • Results

    83% code-generation success rate and 26.7% speedup were achieved on PolyBench/C benchmarks.

  • Takeaways & Limitations

    Combining LLMs, verification tools, and traditional compilers can provide high-quality optimization solutions for loop-type C programs.

  • Takeaways & Limitations

    CBMC verification uses limited input spaces, so an equivalent verdict does not guarantee that two functions are equivalent.

Abstract

from arXiv · show

Recent advances in Large Language Models (LLMs) have opened opportunities to apply high-level code transformations to the field of code optimization, and it has since emerged as one of the most fundamental tasks for LLMs to perform; however, at present, LLMs struggle to apply wide-ranging code optimization tasks due to both the complexity of the code and the inability to independently verify the correctness of the transformations. In this paper, we present the Trusted LLM (T-LLM) Compiler, which proposes an advancement in compiler technology through a collaborative effort involving high-level LLM code transformations, traditional compilers, and verification tools. Experimental results reveal that it can significantly improve code correctness when tested on a set of PolyBench/C benchmarks. Our approach facilitates iterative code optimization efforts with verification strategies that enable corrective actions. Through this approach, T-LLM Compiler achieves code optimization accuracy of up to 83.3% and a speedup of up to 16.1\% on the PolyBench/C benchmarks, with the transformed code reaching an average of 26.7% speedup wrt standard baselines. Additionally, we release the project's source code to the open-source community.

1 Introduction

Compiler optimization is difficult to automate because it requires substantial algorithmic, architectural, and platform expertise. T-LLM Compiler combines LLM transformations with iterative syntax, symbolic, and semantic verification to produce correctly optimized code.

  • Compiler optimization requires substantial knowledge of algorithms, computer architecture, and the application’s underlying platform, making automation challenging.
  • Existing LLM approaches have applied source-code or LLVM-IR transformations, but have not improved transformation success rates.
  • T-LLM Compiler targets level 3 compiler-AI integration by using LLMs for optimization strategies and validating results iteratively.
  • Its validation framework combines syntax checking with LLMs, Alive2, and CBMC to address algorithmic correctness challenges.
  • 83% correctness was achieved through automated iterative code transformation and validation using the Qwen2.5-32B-Instruct model.

2 Related Work

Related work divides LLM-assisted code optimization into deep-learning methods trained for specific tasks and broader systems that combine LLM transformations with checking, retries, or refinement. Existing systems improve optimization reliability, but reported limitations include incomplete correctness validation and difficulty handling complex loop structures.

  • Research categories: Code-optimization research broadly comprises deep-learning methods and LLM-based optimization systems.The deep-learning category trains or fine-tunes models for specific tasks, while LLM-based systems build broader optimization workflows.
  • Learning and prompting: Training datasets, curated slow-fast code pairs, and prompt-selection methods are central to learning optimization patterns and guiding model-based fixes.PIE uses C++ programs from CodeNet and gem5 performance evaluation, while retrieval-augmented prompt generation retrieves prompts for similar performance bugs.
  • LLM compiler approaches: 95.6% of direct-code-generation test cases compiled successfully, but only 20% matched desired compiler output, without runtime correctness checking.The LLM Compiler work generates optimized LLVM-IR code and LLVM compiler pass sequences, with invalid pass sequences handled using -Oz.
  • Verification-oriented systems: LLM-only optimization fails when generated code is not exactly correct, motivating systems that check outputs and retry or refine transformations.These systems add validity or desirability checks around LLMs to increase the chance of successful optimization.
  • Verification-oriented systems: 52% of LLM-Vectorizer attempts generated correct vectorized code, with success increasing across attempts.The framework uses GPT-4 for transformations and Alive2 for LLVM-IR equivalence verification, although Alive2 has limited ability to handle complex loop structures.

3 System Design and Implementation

The T-LLM Compiler combines LLM-based optimization with iterative verification and corrective feedback. It outputs verified optimized code or stops after a maximum iteration count, then tests the result against provided cases.

  • Optimizer: The system feeds benchmark source code to an optimizer that distinguishes first optimization attempts from retries.First attempts combine constructions and may include transformation examples.
  • Verification: Syntax, symbolic, and semantic checkers validate generated code against the input source code.These checks are used to assess the correctness of the proposed transformation.
  • Feedback loop: Verification failures trigger feedback to the optimizer, enabling syntax fixes and logical corrections to previously generated code.The corrective loop continues until verified code is generated or the maximum iteration count is reached.
  • Output: After the verification loop exits, the proposed optimized program is produced and tested against the provided test cases.The flow exits either when verified code is generated or when the maximum iteration count is reached.

3.1 Optimizer

The optimizer uses a Qwen2.5-32B-instruct LLM to transform loops through prompted optimization strategies, few-shot or chain-of-thought guidance, and verifier feedback. A recommender selects applicable loop techniques and examples, enabling iterative refinement and preserving already optimized code when appropriate.

  • Optimizer: The optimizer uses Qwen2.5-32B-instruct to perform loop code transformations guided by few-shot learning and chain-of-thought prompts.Prompts include the original code, optimization instructions, optional exemplars, and verifier feedback addressing rejected transformations.
  • Optimizer: Five representative techniques structure the prompts: loop unrolling, loop jamming, loop tiling, loop distribution, and loop interchange.The investigated prompt types include zero-shot and one-shot prompts with technique-specific examples.
  • Recommender: The recommender uses LoRA-SFT Qwen2.5-Coder-3B-Instruct to identify applicable techniques and assemble their paired examples into the optimizer’s few-shot context.If no loop optimization is warranted, it returns “No Loop Optimization Needed” and prompts the optimizer to reproduce the original code unchanged.
  • Optimizer: Verifier feedback enables iterative refinement when transformations fail to preserve correctness.After the first attempt, the optimizer modifies its strategy in subsequent attempts based on errors identified by the verification chain.

3.2 Transform Verification

T-LLM Compiler verifies LLM-generated transformations through a staged chain that checks syntax, symbolic equivalence, and LLM-based correctness. Incorrect transformations are rejected with explanations and returned to the optimizer for correction.

  • Verification chain: The verification chain uses syntax checking, CBMC-based symbolic verification, and LLM-based verification, while avoiding test-based verification because of runtime and workflow complexities.The system invokes the compiler with -fsyntax-only for early syntax validation and uses CBMC for bounded model checking.
  • Verification chain: Syntax verification detects unusable transformations early, and syntax errors are communicated back to the optimizer for repair.Early failure avoids more computationally expensive checks.
  • Symbolic verification: Alive2 and CBMC were explored as candidate symbolic-verification tools for checking whether optimized code preserves the original program’s behavior.Alive2 uses refinement checking over LLVM IR and SMT solvers, whereas CBMC performs bounded symbolic execution of C programs.
  • Symbolic verification: The T-LLM Compiler is presented as the first use of CBMC for equivalence checking of C-level optimizations generated by an LLM.The equivalence check focuses on an assertion connecting the original and transformed functions, with standard CBMC property checks disabled.

Limitations of CBMC for Equivalence Checking

CBMC equivalence checking is limited by bounded loop exploration, floating-point complexity, and possible false equivalence outcomes. Because CBMC missed some errors, the approach supplemented symbolic verification with LLM-based equivalence prompts, including prompts conditioned on CBMC decisions.

  • Bounded loop exploration: CBMC validates equivalence only over constrained paths determined by specified loop-unrolling bounds, limiting the input and output array sizes it can practically analyze.Large array sizes can make validation impossible to complete in a reasonable amount of time.
  • Floating-point complexity: Floating-point array operations can cause CBMC validation to time out or fail because of search-space explosion and the complexity of floating-point decision procedures.For PolyBench/C, the authors therefore used integer array elements to make equivalence checking tractable.
  • False equivalence outcomes: A CBMC pass declaring two functions equivalent does not guarantee equivalence, because violations outside the limited input space remain undetected.The authors describe such a pass as a strong indication of equivalence, supported by their empirical experiments.
  • LLM-based supplementation: CBMC improved code optimization accuracy but failed to detect as many errors as desired, so the authors supplemented symbolic verification with an LLM-based verification strategy.Functional equivalence was assessed by prompting pretrained and instruction-tuned LLMs with detailed instructions.
  • Prompting strategies: The LLM verifier used either a generic independent prompt or prompts incorporating the CBMC decision for accept, reject, or non-decision outcomes.CBMC rejection was treated as more trustworthy than acceptance because its input search space is constrained.

4 Experiments and Results

Experiments on 30 PolyBench/C benchmarks evaluated transformation correctness and speedup against compiler baselines, showing that prompt selection and verification substantially improve optimization outcomes. Verification increased accuracy while preserving speedup, whereas Alive2 struggled with C-level equivalence checking because of complex kernels.

  • Experimental setup: The evaluation used 30 PolyBench/C benchmarks, compared against the -O3 BiSheng Enterprise compiler on a 128C AArch64 ARM64 server with 512GB RAM.Correctness, average speedup, and average speedup of correctly transformed kernels were the primary metrics.
  • Prompting strategies: 90% transformation success, 100% functional correctness, and 1.178× speedup were achieved by selecting the best transformation for each kernel across prompting strategies.The result exceeded the baseline prompt’s 80% accuracy and 1.167× average speedup.
  • Language models: Qwen2.5-32B-Instruct markedly outperformed CodeLlama-7B-Instruct and CodeLlama-13B-Instruct across all reported Best of All Prompts metrics.The evaluation employed all three listed language models.
  • Verification: Accuracy improved from 60% without verification to 87% with the full verification chain, as incorrect or non-equivalent transformations were rejected and retried.Only a small subset of kernels required re-optimization, but these retries contributed to improved final accuracy.
  • Verification: Average speedup increased from 1.13 to 1.16 after verification, indicating that filtering incorrect optimizations did not hinder performance.The system’s minimal false rejection rates allowed valid optimizations to pass through.
  • Verification limitations: Alive2 frequently timed out while validating equivalence between original and optimized C-level functions, even at modest loop unwind depths.The paper attributes this limitation to PolyBench kernels’ deep nested loops, intricate data dependencies, and complex LLVM IR semantics.

5 Conclusion

The framework combines LLMs, compilers, and symbolic verification tools with iterative retries to produce high-quality PolyBench/C optimizations. Its reported code-generation optimization success rate is 83%, exceeding the approximately 50% typical of prior art.

  • 5 Conclusion: 83% success rate is reported for code-generation optimizations, compared with around 50% in prior code-optimization work.The result concerns loop-type programs from the PolyBench/C benchmark suite.
  • 5 Conclusion: A broad toolchain of compilers, symbolic checkers, and LLMs, combined with iterative retries, is identified as the key to success.The iterative flow retries multiple times to create a viable solution.
  • 5 Conclusion: The framework retains a traditional compiler in the execution flow while collaborating with compiler frameworks for accurate code generation.The conclusion identifies keeping the traditional compiler as a crucial difference from competing approaches.

6 Future Directions

Future work could yield up to 52% speedup by addressing prompt selection, prompting strategy, and optimization of larger, program-wide code transformations. These challenges are central to advancing the T-LLM Compiler toward level 4 of its vision.

  • Future opportunities: 52% speedup is possible through further advances in prompting and optimization strategies, but several problems must be solved to realize these benefits.The paper identifies this as a future opportunity beyond the reported experimental results.
  • Prompt selection: Prompt selection is nontrivial because effectiveness varies substantially across kernels and computational settings.Future work should systematically study how prompt design interacts with kernel characteristics and overall performance.
  • Prompting strategy: One-shot prompting was slightly more effective for speedups, while two-shot prompts worked well in some examples and may favor sequential requests.The prompts aimed to expose optimization opportunities for the BiSheng compiler.
  • Scaling to larger code bases: Most optimized benchmark functions were roughly under 50 lines, whereas larger and more complex functions remain challenging to optimize.Programwide transformations are expected to encounter this difficulty sooner.
  • Scaling to larger code bases: Solving large-code and programwide transformation challenges is viewed as necessary for reaching level 4 in the T-LLM Compiler vision.This challenge is presented as a key direction for continued optimization efforts.

A Verification & Optimization Prompts

The prompt collection combines LLM verification instructions for checking functional equivalence with optimization prompts that direct loop-level improvements in C code. Verification prompts account for potentially incorrect transformations, while optimizer prompts require analysis and tagged optimized-code output.

  • Verification prompts: The verifier prompt presents original and optimized C functions and asks whether they are functionally equivalent.The optimized version may either preserve or break the original function’s logic or behavior.
  • Verification prompts: Verifier variants provide context from CBMC decisions to accept equivalent code or reject nonequivalent code.The collection includes both accept and reject CBMC-context prompts.
  • Optimization prompts: Optimizer prompts direct analysis of C code and apply loop-level techniques such as unrolling, jamming, fusion, or tiling to improve execution time.The optimizer is described as a specialized assistant for compilers and C code optimization.
  • Optimization prompts: The final optimized C code must be returned between [OPT] and [/OPT] tags.The prompt requests only the best optimized code after analyzing the input and applying relevant optimizations.
Loading 2608.14953v1…