Paper deep dive
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
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 8/18/2026, 4:59:38 AM
Summary
The paper introduces the T-LLM Compiler, a framework that integrates Large Language Models (LLMs) with traditional compilers and verification tools to optimize code. It uses a Qwen2.5-32B-Instruct model for code transformations guided by a strategy recommender (Qwen2.5-Coder-3B-Instruct) and validates correctness using syntax, symbolic (CBMC, Alive2), and semantic checkers. The system achieves up to 83.3% optimization accuracy and significant speedups on PolyBench/C benchmarks.
Entities (8)
Relation Signals (9)
T-LLM Compiler â evaluatedon â PolyBench/C
confidence 98% ¡ Experimental results reveal that it can significantly improve code correctness when tested on a set of PolyBench/C benchmarks.
T-LLM Compiler â achievesaccuracy â 83.3%
confidence 95% ¡ T-LLM Compiler achieves code optimization accuracy of up to 83.3%
T-LLM Compiler â achievesspeedup â 16.1%
confidence 95% ¡ speedup of up to 16.1% on the PolyBench/C benchmarks
T-LLM Compiler â developedby â Huawei Technologies
confidence 95% ¡ Authors are affiliated with Huawei Technologies, Heterogeneous Compiler Lab
T-LLM Compiler â usesmodel â Qwen2.5-Coder-3B-Instruct
confidence 95% ¡ The Recommender employs a low-rank adaptation supervised-finetuned (LoRA-SFT) Qwen2.5-Coder-3B-Instruct large language model
T-LLM Compiler â usesmodel â Qwen2.5-32B-Instruct
confidence 95% ¡ This automated iterative framework leverages the Qwen2.5-32B-Instruct LLM model for code transformations
T-LLM Compiler â verifieswith â Alive2
confidence 92% ¡ verification framework comprising ... Alive2 [16]
T-LLM Compiler â verifieswith â CBMC
confidence 92% ¡ verification framework comprising ... CBMC [13]
Qwen2.5-Coder-3B-Instruct â trainedon â LORE dataset
confidence 90% ¡ To fine-tune the Qwen2.5-Coder-3B-Instruct model ... we employed the LORE dataset
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2608.14953v1
- Canonical: https://arxiv.org/abs/2608.14953v1
Trouble viewing inline? Open PDF directly â
Full Text
72,458 characters extracted from source content.
Expand or collapse full text
T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework Zahra Fazel zahra.fazel@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Sunanda Gamage sunanda.gamage@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Shayan Shirahmad Gale Bagi shayan.shirahmad.bagi@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Amir H. Ashouri amirh.ashouri@gmail.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Tomasz S. Czajkowski tomasz.czajkowski@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Bryan Chan bryan.chan@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Reza Azimi reza.azimi1@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Yaoqing Gao yaoqing.gao@huawei.com Huawei Technologies, Heterogeneous Compiler Lab Toronto, Canada Abstract Recent advances in Large Language Models (LLMs) have opened opportunities to apply high-level code transforma- tions 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 strate- gies 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 commu- nity 1 . 1 Introduction During compilation, program optimization is an important task for improving application performance and usability. The task requires substantial knowledge of algorithms, com- puter architecture, and the underlying platform on which 1 https://github.com/BiSheng-Compiler-Agents/CCE-WOZ/tree/tllm- compiler the application runs. However, because of the high degree of expertise and low-level knowledge required, it becomes a challenging task to automate. Since the early days of pro- gramming, compilers have emerged as core tools to first transform code into executable instructions, and later, with the advent of optimizing compilers, to actually perform mid- to-low-level transformations that reduce the runtime, power, and code size of any given application. Compilers, however, are limited in what they can do in part because of program- ming languages that impose certain restrictions on code writ- ten, as well as the increasing complexity of low-level code transformations required to make significant improvements. To address this problem, numerous approaches have been proposed that leverage artificial intelligence (AI), be it through the use of machine learning (ML) models [2â4,26], AI-powered tools such as RL-based autotuners [27], or large language models [9,24]. ML models are generally used to replace a hand-coded heuristic that determines when a certain trans- formation should be applied or is profitable. This is a very useful approach, as it allows a more data-driven approach to optimization that can easily adapt to new architectures with only model retraining being required, while retaining the correctness of the transformation since that portion is performed by traditional compiler approaches. AI-powered tuners serve a similar purpose, but leverage compiler flags to redirect a search of viable solutions in a particular direc- tion. While the search typically involves sweeping many hundreds of parameters, RL-based approaches have proven to be highly effective in guiding the search. Finally, with the advent of LLMs, a wide range of efforts has emerged to replace some compiler optimizations with LLM source code changes, which can be a viable path to performance arXiv:2608.14953v1 [cs.AI] 15 Aug 2026 Fazel et al. improvement. Also, work has been done on low-level virtual machine intermediate representation (LLVM-IR) to apply large language models to predict pass ordering for the best code size optimization sequence or direct IR-to-IR transfor- mations [9]. These approaches, however, have not improved the transformation success rate. In this paper, we propose that AI can catalyze the ad- vancement of optimizing compilers in a collaborative fash- ion, where LLMs can unlock performance opportunities in tandem with existing compiler tools. To achieve this, we propose that an increasing level of compiler-AI integration is the key to this next generation of compilers. To illustrate the idea, we have divided compiler AI-enablement into levels inspired by [19] as shown in Fig. 1. In the figure, level 0 represents a base compiler without any AI, or more specifically, machine learning-based enable- ment, where the decisions are made by heuristic algorithms. Changes to the compiler require code rewriting and can be time-consuming. Level 1 is basic machine-learning-based enablement, where decisions of profitability can be made by machine learning models that are trained on a large cor- pus of data, allowing for fine-grained cost function tuning and data-driven compiler design. The transformations them- selves are still performed using traditional methods. At level 2, we inject the use of LLMs to rewrite code in a more sub- stantial way, for example, by permitting algorithmic changes that general compilers are not able to do. This, by definition, requires correctness checking, but it provides an opportunity to open up optimization space for compilers. At this stage, we consider AI/LLMs as consultants to help in unlocking the performance or effectiveness of existing compiler passes. This collaborative effort mirrors minor code changes devel- opers would do to boost performance, with some knowledge of where and why optimizing compilers fail to apply the most effective transformations. This approach can be further advanced to level 3, where more complex transformation sequences are entrusted to LLMs but do not replace the compiler fundamentals that are used for otherwise effective optimizations. In this flow, the level 3 compiler integrates LLMs in synergy with traditional optimizing compilers. Fi- nally, level 4 elevates the optimization process to one where a wide range of tools are integrated into the compilation process, allowing for both local and global optimizations to be performed by a combination of LLM and traditional trans- forms, aided by code analysis tooling to direct optimization effort. In this paper, we propose the Trusted LLM Compiler (T- LLM Compiler), which approaches level 3 by leveraging var- ious code transformations to unlock compiler capabilities and produce fast code. In this approach, we leverage LLMs to apply optimization strategies and then validate the re- sults using a wide range of verification techniques. This is done in an iterative fashion to generate a correctly optimized program. To ensure correctness, we include a comprehen- sive validation framework comprising a compiler for syntax checking, as well as LLMs and tools such as Alive2 [16] and CBMC [13], to address algorithmic correctness challenges. This automated iterative framework leverages the Qwen2.5- 32B-Instruct LLM model for code transformations, and to- gether with a validation strategy, shows both high speedup and correctness reaching 83%, significantly advancing the state-of-the-art in LLM-enabled compiler technology. In the following sections, we describe key contributions of our work: 1) the T-LLM Compiler framework, detailed design information of the flow and prompting strategies, and 2) our transformation verification framework that comprises syn- tax, symbolic, and semantic checking approaches to improve the correctness of optimized code. 2 Related Work With the popularity and potential impact LLMs promise, many attempts to improve code optimization have been pro- posed. Generally, we can categorize them into two groups: deep-learning methods for code optimization and LLM-based code optimization systems. 2.1 Deep-learning methods for code optimization The first category of works focuses on the training and/or fine-tuning of large language models towards a specific task. The idea is to enclose within the LLM the capability to ef- fectively perform a task in a single step on the basis of prior experience gained via training or finetuning. The main thrust in the context of compilation and code optimization tasks is therefore to replace compilers with LLMs, although in many cases, the works still use a compiler as a final step for executable generation. In the domain of code optimization, a great deal of focus is given to training datasets and methodologies for models. For example, [22] [23] uses C++ programs from CodeNet [21], using gem5 [6] as a simulator to evaluate the performance of each solution to a problem. The data is curated and cat- egorized by problems and used for training and validation purposes. Their proposed dataset, performance-improving edits (PIE), is used to create slow-fast code pairs to help LLMs learn optimization patterns to replicate. In addition to training, prompt selection has emerged as an important consideration for LLM-based code optimiza- tion systems. Works such as [11] discuss the challenge of addressing performance bugs and use retrieval-augmented prompt generation to identify similar performance-related bugs that can then be used to retrieve an appropriate prompt that has been proven to successfully guide an LLM in prob- lem resolution, showing that such an approach can be more successful than purely manual approaches 60% of the time. In the compiler domain, the LLM Compiler work [9] fo- cuses on training foundational models that take as input T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework L0 L2 L3 LLM Code Rewriting Agent Cost model LLM-Based Transforms LLM Code Intent Analysis Agent LLM Planning Agent LLM Code Optimization Agent Cost model Intelligent decision- making Intelligent Autotuning Cost model Decision algorithm Optimization algorithm 1 Optimization algorithm n Transforms ... Optimization algorithm 1 Optimization algorithm n Cost model Decision algorithm heuristic Decision- making Transforms ... Intelligent decision- making LLM-Based Simple Code Transformation Cost model Decision algorithm Optimization algorithm 1 Optimization algorithm n Transforms ... LLM-Based Transform Code Analyzer Automated Validation Prompt Generation LLM Code Generation Code/IR Rewrite Intelligent decision- making LLM-Based Complex Code Transformation Cost model Decision algorithm Optimization algorithm 1 Optimization algorithm n Transforms ... LLM-Based Transforms Code Analyzer Automated Validation Prompt Generation LLM Code Generation Code/IR Rewrite L0 (No AI) L1 (AI as a tool) L2 (AI as a Consultant) L3 (AI as a Collaborator) L4 (AI as an Expert) Figure 1. T-LLM Compiler AI-Assistance levels LLVM-IR [14] to drive the generation of optimized code (op- timized for code size) and a pass sequence that an LLVM compiler would use to generate the desired outcome. In the case of direct code generation, they achieve successful compi- lation in 95.6% of test cases; however, only 20% matched com- piler output (desired), and correctness via runtime checking was not performed. In the scenario of pass inference, the flow used -Oz pass in cases where the generated pass sequence was invalid, and the actual transformation was performed by the LLVM compiler, resulting in a modest 5.58% code size reduction. In contrast to optimizing code at the LLVM-IR level, Deep- PERF [10] proposes an approach to suggest C# code changes for developers to apply. The model is trained on both the English language and source code corpora, followed by fine- tuning for the task of generating patches aimed at perfor- mance optimization. Similarly, [7] proposes a model trained on code pairs to guide programmers in writing high-performance code. 2.2 LLM-based code optimization systems The limitation of LLM-only approaches is that if the LLM fails to generate the exact result required, the process fails. To address this, other works have developed comprehensive systems around LLMs to enhance the chances of success. These systems usually comprise a form of checking to deter- mine if the output is valid or desirable, which causes a retry or a refinement step in the code optimization process. LLM-Vectorizer [24] is a recent LLM-based code optimiza- tion flow geared toward producing more effective AVX2 vectorized code, tested on the TSVC-2 benchmark set. The framework shows the ability to generate correct vectorized code in 52% of the time; however, the success rate increases with an increased number of attempts. This framework uti- lizes GPT-4 [1] for code transformations and Alive2 [16] for verifying the transformed code. Alive2 essentially performs analysis on two input LLVM-IR representations of presum- ably equivalent code to verify if the provided inputs are indeed equivalent, which is very useful in validating LLVM compiler transforms. However, it is limited in its ability to handle complex loop structures. ECO [15] is another framework that examines code im- provements based on performance anti-patterns, or code patterns that indicate a performance opportunity. In this case, the work focuses on issues such as memory allocation and the use of data structures, including vectors and maps. The objective is to propose patches to address these perfor- mance bottlenecks, and the results are validated via unit tests and integration tests. LLMs are used to correct some sim- ple failures, but eventually, failing test cases are abandoned. Passing cases are still reviewed by engineers. Similar works include [5][17][18]. 3 System Design and Implementation To implement our T-LLM compiler, we constructed a system depicted in Fig. 2. The system takes as input a benchmark source code and feeds it to the optimizer. Within the opti- mizer, the first step is to determine if this is a retry or a first attempt at optimization. In the case of a first attempt, which combines constructions and optionally includes examples of transformations, along with the code to be optimized, it passes the instructions to the LLM for optimization. Then, the LLM applies the prompt, which comprises instructions and code to be optimized, and produces the resulting opti- mized code. The code is then checked using syntax, symbolic and semantic checkers that validate its correctness against Fazel et al. the input source code. In the case of failure, the feedback loop to the optimizer is engaged, and corrective actions are taken to fix the code previously generated. This could range from simple syntax fixes to logical corrections detected during verification. Finally, once a verified code has been generated or the maximum iteration count is reached, the flow exits, producing the proposed optimized program. The resulting output is then tested against the provided test cases, and performance is measured. 3.1 Optimizer The optimizer employs a Qwen2.5-32B-instruct [25] large language model (LLM) to perform code transformations for loop optimization. This process is guided by prompts that de- fine the optimization strategy, leveraging few-shot learning and chain-of-thought techniques to improve reliability and quality of the transformations. The optimizer covers both the original code optimization attempt and the feedback from the verifier. The prompt applied to the LLM comprises the following: â˘Original code to be optimized, together with instruc- tions (based on the recommended prompt) to perform code optimization. ⢠Depending on the strategy, the optimizer incorporates few-shot learning or chain-of-thought exemplars, pro- viding the LLM with representative transformations that guide its reasoning process. â˘Feedback from the verification chain to address enu- merated errors in the case of verifier rejections. To create prompts for optimization, we constructed them around five representative loop optimization techniques: loop unrolling, loop jamming (also known as loop fusion), loop tiling, loop distribution (also known as loop fission), and loop interchange. The prompts comprise instructions and, optionally, include examples of specific optimization techniques. The type of prompts we investigated includes a zero-shot prompt, which comprises no examples, five one- shot prompts with each including one of four examples, and ten two-shot prompts, each comprising a permutation of example pairs together. In total, this resulted in 16 distinct prompts. In our study, we found that these types of prompts were effective, and most of the prompts were suitable for some of the benchmarks; however, it was not the case that one prompt was generally the best across the board. This generated a need to develop a recommender system that se- lects prompts and optimization examples based on the input code provided for optimization. 3.1.1 Optimization Strategy Recommender. The Rec- ommender module functions as an integral sub-component of the overall optimization framework, tasked with identify- ing the most suitable optimization strategies and illustrative examples to include in the code-optimization prompt. To perform this selection, the Recommender employs a low- rank adaptation supervised-finetuned (LoRA-SFT) Qwen2.5- Coder-3B-Instruct large language model (LLM) [25]. Given an input code fragment, the model is prompted to determine which, if any, of the five predefined loop-optimization tech- niques are applicable. In cases where the submitted code is already optimized with respect to looping constructs, the Recommender explicitly returns the label âNo Loop Opti- mization Needed.â Each of the five optimization strategies is paired with a corresponding example. Once the Recommender identifies the relevant strategies, the associated examples are assem- bled to form the few-shot context used by the downstream optimizer. Conversely, if the Recommender concludes that no further optimization is warranted, the system constructs a prompt instructing the optimizer to reproduce the orig- inal code without modification. This mechanism ensures that the optimization pipeline remains both targeted and conservative - providing guidance only when beneficial and preserving correctness when no additional improvement is advisable. To fine-tune the Qwen2.5-Coder-3B-Instruct model for the task of recommending loop optimization strategies, we employed the LORE dataset [8], explicitly excluding the Poly- Bench/C subset to prevent overlap with downstream evalua- tion. The LORE corpus comprises approximately 70,000 code samples, each accompanied by program mutations and asso- ciated speedup metadata. From this collection, we retained only those mutated variants that achieved a performance improvement greater than 5%, yielding a subset of approxi- mately 17,000 candidate examples. To avoid bias toward any particular optimization technique, we drew a class-balanced sample from this filtered pool, ensuring an equal representa- tion of the five loop optimization strategies. Additionally, we extracted an equal number of samples from the unfiltered dataset where mutations resulted in per- formance regressions exceeding a 20% slowdown. These were used to construct negative instances, examples in which no loop optimization should be applied, thereby enabling the model to distinguish between beneficial and detrimental transformation contexts. The resulting dataset contained 3,418 total examples, partitioned into 3,009 training samples and 409 validation samples. Fine-tuning was performed using low-rank adaptation (LoRA), configured with a rank of 32 and a scaling factor (alpha) of 32, together with a LoRA-plus learning-rate ratio of 16. The model was trained for three epochs. This config- uration was chosen to balance training stability, parameter efficiency, and the ability to capture the nuanced decision boundaries required for reliable optimization strategy rec- ommendations. T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework Optimization Recommender LLM T-LLM Compiler Framework Benchmark Feedback & Prompt Synthesizer LLM-Based Semantic Checker Syntax Checker Symbolic Checker Verification System LLMCBMCCompiler Tools Final Verifier & Performance Measurement Optimized Benchmark Optimizer Code Extractor Figure 2. Architecture of our code optimization and verification system. LLMs are shown in yellow, and other tools are shown in blue. 3.1.2 Feedback & Prompt Synthesizer. After the first transformation attempt, the feedback received from the ver- ification chain (detailed below) is used to refine the opti- mizerâs strategy. For example, if the verification feedback indicates that certain optimizations did not preserve correct- ness, the optimizer can modify its approach in subsequent attempts, enhancing the transformation process iteratively. 3.2 Transform Verification The code transformations generated by the LLM-based Opti- mizer have the potential to be incorrect in several ways. Most importantly, the optimization attempt may have resulted in code that is functionally not equivalent to the original code. The goal of the verification chain is to assess the correctness of the transformed code using different approaches. Code transformations flagged as incorrect by the verification chain are rejected with an explanation (error messages, etc.) and sent back to the optimizer for another attempt. As demon- strated in the results, the verification chain increases the correctness of the overall optimization system. The verification chain comprises three verification steps, each targeting distinct aspects of the codeâs correctness and functionality. These are: syntax verification, symbolic verifi- cation using the CBMC tool (bounded model checking) [13], and LLM-based verification. Note that we avoid test-based verification in the system, as it introduces runtime complex- ities that do not fit a compiler workflow (e.g., the need for setting up test cases, impact on workflow speed, etc.). 3.2.1 Syntax Verifier. The first step in the verification chain checks whether the optimized code adheres to correct syntax. This is performed by invoking the compiler with the -fsyntax-onlyflag. Syntax checking at the beginning of the chain helps root out clearly unusable transforms and fail early without the need for attempting more computationally expensive checks. In the case of syntax errors, the errors are communicated back to the optimizer for an attempt to fix the discovered problems. 3.2.2 Symbolic Verification. We explored two candidate tools for symbolic verification of transforms generated by the optimizer: Alive2 [16] and the C Bounded Model Checker (CBMC) [13]. Alive2 [16]. Alive2 provides a formal mechanism for veri- fying compiler optimizations through refinement checking, a technique that validates the optimized program preserves the semantics of the original. Its approach encodes the original and optimized LLVM IR functions into SMT constraints and proves refinement by discharging them with efficient SMT solvers. Inspired by the use of Alive2 in the LLM-based code vectorization system described in [24], we experimented with Alive2 within our compiler workflow to validate the equivalence of LLM-generated optimizations at the LLVM-IR level. The C Bounded Model Checker (CBMC) [13]. CBMC is a widely used software verification tool that checks the prop- erties of programs via symbolic execution within a bounded space. It translates a given C program with assertions (prop- erties to be checked) into an intermediate representation with loops unrolled to a specified depth (bounded), and de- rives an SMT (Satisfiability Modulo Theories). The SMT for- mula is then checked for satisfiability with an efficient SMT solver, where satisfiability indicates violation of a property or assertion in the input program. Prior works have demonstrated the potential of using CBMC for equivalence checking of programs. For example, it has been used for regression verification (proving that a modification to a program does not violate equivalence, which is highly useful for regression testing in software de- velopment) [12]. In more recent work, CBMC has been used Fazel et al. to detect faults (assertion failures) in Python code by first translating Python to C code using a large language model [20]. However, to the best of our knowledge, our T-LLM Com- piler is the first use case of CBMC for equivalence checking of C-level optimizations, particularly for LLM-generated op- timizations. To perform equivalence checking between the original function and the transformed or optimized function, a pro- gram needs to have the structure illustrated in Fig. 3. The CBMC tool is invoked on this program as: cbmc âcvc5 âno-standard-checks âfunction main âunwind 20 In this invocation, standard CBMC property checks are disabled (e.g. pointer and array bound checks etc.) as we are primarily interested in the equivalence assertion in the main function (âfunction main). Theâunwindflag specifies the loop unrolling depth for performing bounded checking, which has to be reasonably small for tractable equivalence checking. Thecvc5SMT solver is used in this work, as empirical results have shown that it is able to perform equivalence checking for larger loop unrolling depths than the default SMT solver in CBMC or the Z3 SMT solver. Limitations of CBMC for Equivalence Checking While CBMC is a very useful tool, it does come with some limitations. These include limited loop bounds, handling floating-point data types, and potential false equivalence outcomes. In particular: Limited loop bounds. A loop unrolling depth or bound needs to be specified for each loop in the code, which means the CBMC equivalence assertion is validated for a constrained set of paths in the program (bounded model checking). This typically corresponds to limited input and output array sizes, as loops often iterate on arrays. When large array sizes are used, CBMC is unable to complete the validation in a reason- able amount of time. For example, on PolyBench/C, matrix sizes needed to be under 15 x 15 for successful CBMC verifi- cation. High computational complexity with floating point data types. For code with complex operations on arrays (e.g. matrix operations such as those in PolyBench/C), the CBMC validation takes too long or fails when the array data type is float. This is likely due to the search space explosion caused by float data types and the complexities of the floating-point decision procedure in CBMC. On PolyBench/C, this forced us to use integer array elements, resulting in tractable and useful equivalence checking. Potential for false equivalence outcomes. Equivalence verification on a limited input space means that a violation existing outside this space will not be detected by CBMC. In other words, a CBMC verification pass (decision: equivalent) does not guarantee that the two functions are equivalent. However, it remains a strong indication of equivalence, as corroborated by our empirical experiments. #include <assert.h> #define N 15 int nondet_int (); // CBMC function // Original function void kernel_original(int n, int input[N], int output[N ]) for (int i = 0; i < n; i++) output[i] = input[i] * 2; // Transformed function void kernel_transformed(int n, int input[N], int output[N]) for (int i = 0; i < n; i++) output[i] = input[i] + input[i]; int main() int input1[N], output1[N]; int input2[N], output2[N]; // Initialize input arrays with non -deterministic values for (int i = 0; i < N; i++) input1[i] = nondet_int (); input2[i] = input1[i]; // Make identical copies // Run both functions kernel_original(N, input1 , output1); kernel_transformed(N, input2 , output2); // Assert equivalence of outputs per array element for (int i = 0; i < N; i++) assert(output1[i] == output2[i]); return 0; Figure 3. C program with code augmentations necessary for function equivalence checking by CBMC 3.2.3 LLM-based Semantic Verifier. While CBMC has been shown in our experiments to provide an improvement in the code optimization accuracy, it was unable to detect as many errors as we hoped. As such we had to supplement this symbolic verification with our own LLM-based veri- fication strategy. In our approach, functional equivalence between the original and the transformed code is determined by prompting an LLM in the form shown in Fig. 4. In this work, we use detailed prompts on pretrained and instruction- tuned LLMs without doing any finetuning, to evaluate the potential of base LLMs for the task for assessing equivalence between two versions of code. The prompting strategies explored in our work include: ⢠Single independent prompt (Fig. 8). A generic prompt asking to check equivalence between the two versions of C code (original and transformed). Detailed instruc- tions and hints are given on the important aspects of the code comparison (e.g. code paths, data dependen- cies). T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework â˘Three prompts dependent on the CBMC Verifierâs de- cision. The CBMC Verifier can produce one of three decisions: accept, reject, non-decision (failures such as timeouts). Also, a rejection by CBMC is more trustwor- thy than an accept (due to constrained input search space). To reflect this, we prepare two additional prompts for the reject and accept decisions of the CBMC Veri- fier, by adding information about the CBMC decision to the prompt (Figs. 9, 10). In the case of a non-decision from the CBMC Verifier, the system resorts to the pre- vious single independent prompt. Given below are two versions of a C function ... [more context] ... Task: Evaluate whether the optimized version is functionally equivalent to the original. Original function: ORIGINAL_CODE Optimized version: TRANSFORMED_CODE Instructions on elements to look for (e.g. code paths , data dependencies): Output format instructions: Figure 4. Structure of the prompts used in the LLM Verifier 4 Experiments and Results To test the effectiveness of the T-LLM Compiler we tested it on a set of 30 PolyBench/C benchmarks suite and compared it to the -O3 BiSheng Enterprise compiler. The runtime of each benchmark was measured on a 128C AArch64 ARM64 server with 512GB RAM. The two primary performance metrics used to evaluate the system are: â˘Correctness: The percentage of correctly transformed functions, as validated by a test suite. â˘Average speedup: The average runtime performance improvement achieved by the optimizations across the dataset. Note that if an optimization produced by the system is incorrect, we treat its speedup as 1.0. â˘Average speedup of Correctly Transformed Ker- nels: The average runtime performance improvement of kernels that were transformed and correct. In addition to end-to-end testing, we examine the utility and effectiveness of each system component in more detail. This includes how we arrived at different prompting strate- gies and how they perform individually, challenges we faced with symbolic checker tools, and finally, the performance of different verification strategies. We also executed our baseline using both the Bisheng and GCC compilers under the O2 and O3 optimization levels. As reported in Table 1, the resulting runtimes exhibit no statistically significant differences, indicating comparable performance across compilers and optimization settings. 4.1 Optimizer Performance Table 2 presents a comparative analysis of prompting strate- gies, examining their impact on kernel transformation suc- cess, functional correctness, and execution speedup. The baseline prompt, which contained no examples, achieved a 90% success rate in kernel transformation and 80% accu- racy, accompanied by a modest average speedup of 1.167Ă. Incorporating one-shot prompts produced variable effects depending on the chosen example. For instance, One-shot Prompt 1 increased accuracy to 90% but reduced transfor- mation success to 86.67%, while One-shot Prompt 2 main- tained 90% accuracy but yielded the lowest transformation rate at 73.33%. One-shot Prompt 3 yielded a more balanced outcome, with 83.33% transformation success and 86.67% ac- curacy. Two-shot prompts provided greater stability across the evaluated metrics. Notably, combining Examples 2 and 3 resulted in the highest accuracy (96.67%), albeit at a mod- erate transformation success rate of 80%. In contrast, the pairing of Examples 3 and 4 yielded a more balanced perfor- mance, achieving an 86.67% transformation, 90% accuracy, and a reasonable speedup of 1.084Ă. These results suggest that carefully curated example combinations can enhance correctness while maintaining acceptable transformation re- liability. Comparing one-shot prompts to two-shot prompts, we find that they have similar average accuracy; however, one-shot prompts show, on average, a higher overall speedup compared to two-shot prompts (11.83% vs 9.37%). One- and two-shot prompts are more accurate than the base prompt by approximately 7.5%. This suggests that leveraging prompts with examples is more effective overall in producing a cor- rect result; however, focusing on fewer classes of examples also provides more robust guidance to the LLM, enabling high-quality optimization to take effect. When selecting the best-performing transformation for each kernel across all prompting strategies, the T-LLM com- piler framework demonstrated 90% transformation success and perfect functional correctness (100%), alongside the high- est observed speedup of 1.178Ă. This highlights the impor- tance of prompt optimization in achieving both reliable cor- rectness and improved efficiency. Building upon these results, we constructed an optimization- strategy recommender system capable of autonomously se- lecting the most appropriate prompting configuration for each kernel. We evaluated the recommender under two con- ditions: with chain-of-thought (CoT) reasoning enabled and with CoT disabled. When CoT was employed, the system achieved a transformation success rate of 80% and yielded a substantial average speedup of 1.115Ă. However, this im- provement came with a reduction in accuracy, which was also measured at 80%. Conversely, when CoT was omitted, the recommender achieved a slightly higher transformation success rate of 83.33% and an average speedup of 1.079Ă, along with a modest gain in accuracy of 0.33%. Although Fazel et al. Table 1. Kernels Execution Times in Seconds with Different Compilers and Flags KernelBisheng with O3 Flag Bisheng with O2 Flag GCC with O3 Flag GCC with O2 Flag durbin0.0050.0050.0050.005 lu5.2575.2585.2695.283 gramschmidt3.9113.9753.8843.941 ludcmp5.2575.235.2435.229 trisolv0.0050.0040.0050.005 cholesky2.7112.712.7122.712 mvt0.0160.0160.0170.017 doitgen1.0051.0051.0061.007 3m5.5035.5155.4975.5 2m3.3423.3343.3293.33 bicg0.0270.0270.0270.027 atax0.0090.0090.0120.012 gesummv0.0120.0110.0120.012 symm2.5022.5072.5322.553 syr2k2.8992.9662.1372.148 gemver0.0190.0190.0210.021 syrk1.3021.3180.8920.869 gemm0.7660.7560.8150.769 trmm1.4191.4121.4191.444 adi17.65917.6217.10717.127 heat-3d6.8836.8487.1617.15 jacobi-2d3.5953.5674.1734.179 seidel-2d32.43332.42132.35632.349 fdtd-2d2.492.452.6132.624 jacobi-1d0.0020.0020.0020.002 floyd-warshall27.66329.62223.66223.626 deriche0.2120.2120.2150.216 nussinov4.0574.0754.2574.266 correlation2.7162.6632.5532.556 covariance2.6972.6112.612.581 this comparison reveals a trade-off between the magnitude of speedup and predictive reliability, the overall findings indicate that automated prompt selection, irrespective of CoT usage, provides meaningful performance benefits while maintaining a high degree of transformation consistency. Overall, the results highlight that the design of prompts has a significant impact on model performance. While indi- vidual one-shot and two-shot prompts illustrate the sensi- tivity of outcomes to example quality, the best results are achieved by carefully selecting optimal prompts for maxi- mum accuracy and speedup or by employing a recommender system to enhance speed and consistency. In our experimental evaluation, we employed three large language models (LLMs): CodeLlama-7B-Instruct, CodeLlama- 13B-Instruct, and Qwen2.5-32B-Instruct. Table 3 summarizes the âBest of All Promptsâ performance for each model. As the results indicate, Qwen2.5-32B-Instruct demonstrates a sub- stantial performance advantage, markedly outperforming both CodeLlama variants across all reported metrics. 4.2 T-LLM Compiler Workflow in Action To demonstrate the flow, we elaborate on one of the examples as it was processed by our T-LLM compiler. This example is the doitgen benchmark in the PolyBench/C suite shown in Fig. 5. The core computation of this kernel is found in the q loop where an array sum is essentially computing a vector inner product. The performance problem here is that while array A is accessed efficiently, array C4 is not. The solution to the performance problem is to interchange loops p and s, which T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework Table 2. PolyBench/C results with different optimizer prompts using Qwen2.5 - 32B - Instruct as the LLM ExperimentExamplesTransformed Kernels Accuracy Average speedup Average speedup of Correctly Transformed Kernels Base PromptNo examples90.00%80.00%1.1671.240 One-shot Prompt 1Unrolling86.67%90.00%1.0911.122 One-shot Prompt 2Jamming73.33%90.00%1.1091.175 One-shot Prompt 3Tiling83.33%86.67%1.1121.163 One-shot Prompt 4Interchange76.67%83.33%1.1611.267 One-shot Prompt 5Distribution76.67%90.00%1.0351.055 Two-shot Prompt 1Unrolling & Jamming83.33%83.33%1.0981.114 Two-shot Prompt 2Unrolling & Tiling86.67%83.33%1.1041.149 Two-shot Prompt 3Unrolling & Interchange83.33%83.33%1.1241.186 Two-shot Prompt 4Jamming & Tiling80.00%96.67%1.0981.127 Two-shot Prompt 5Jamming & Interchange80.00%90.00%1.0541.080 Two-shot Prompt 6Tiling & Interchange86.67%90.00%1.0841.110 Two-shot Prompt 7Distribution & Unrolling83.33%76.67%1.0691.116 Two-shot Prompt 8Distribution & Tiling83.33%76.67%1.0561.092 Two-shot Prompt 9Distribution & Interchange83.33%86.67%1.1651.237 Two-shot Prompt 10Distribution & Jamming86.67%66.67%1.0921.174 Recommender without CoT-83.33%83.33%1.0791.120 Recommender with CoT-80.00%80.00%1.1151.194 Best of All Prompts-90.00%100.00%1.1751.195 Table 3. Best PolyBench/C results with different LLMs LLM ModelTransformed Kernels Accuracy Average speedup Average speedup of Correctly Transformed Kernels CodeLlama - 7B6.67%100%0.990.99 CodeLLama - 13B10%100%0.970.74 Qwen2.5 - 32B90%100%1.1781.198 will cause array A to be accessing a loop invariant value in the inner most loop p, but now array C4 will be accessing data sequentially. The prompt used in this example is a one-shot prompt with a loop interchange example, which initially generates code in Fig. 6. This code contains an easy-to-identify error, where the final results are prematurely stored in array A. This error is detected by the CBMC verifier, which causes the T-LLM Compiler flow to reject this solution and attempt a second iteration to fix the problem. Based on a feedback prompt, the second attempt is made in which a correct transformation is applied and verified by CMBC as shown in Fig. 7. This enables the BiSheng Enterprise compiler to effectively handle this loop and generate efficient code that runs 4.33X faster than the original. It is noteworthy that this solution was only found by ex- actly one prompt that exclusively suggested interchange as a proposed avenue of optimization. In addition, we exam- ined the LLVM-IR of the two versions of the code and found that an improved memory layout was only part of the rea- son for the speedup. The other part was the application of vectorization by a factor of 2 to the inner most p loop. Al- though the prompt did not request vectorization, and none was applied by the LLM, the loop interchange and associated code changes enabled the BiSheng compiler to recognize that vectorization was profitable in this case, causing it to be applied. This is a very clear example of LLM collaborating with the traditional compiler flow to overcome performance bottlenecks. A summary of all results for one-shot prompt 4, from which this example is taken, is provided in Table 4. void kernel_doitgen(int nr , int nq , int np , int 3 D_ARRAY(A,NR ,NQ ,NP ,nr ,nq ,np), int 2D_ARRAY(C4 ,NP , NP ,np ,np), int 2D_ARRAY(sum ,NP ,np)) int r, q, p, s; for (r = 0; r < _PB_NR; r++) for (q = 0; q < _PB_NQ; q++) for (p = 0; p < _PB_NP; p++) sum[p] = SCALAR_VAL (0.0); for (s = 0; s < _PB_NP; s++) sum[p] += A[r][q][s] * C4[s][p]; for (p = 0; p < _PB_NP; p++) A[r][q][p] = sum[p]; Figure 5. Original PolyBench kernel: doitgen Fazel et al. Table 4. Kernels Transformation, Verification, Speedup, & Correctness with One-shot Prompt 4 KernelTransformed No. of Attempts Syntax Verification CBMC Verification LLM Verification Test-based Validation speedup durbinTrue1TrueTrueTrueTrue1.250 luFalse1TrueTrueTrueTrue0.997 gramschmidtFalse1TrueTrueTrueTrue1.018 ludcmpTrue1TrueTrueTrueTrue1.004 trisolvFalse1TrueTrueTrueTrue1.000 choleskyFalse1TrueTrueTrueTrue0.999 mvtTrue1TrueTrueTrueTrue1.455 doitgenTrue2TrueFalseTrueTrue4.332 3mmFalse1TrueTrueTrueTrue0.999 2mmFalse1TrueTrueTrueTrue1.003 bicgTrue2TrueTrueTrueTrue1.000 ataxTrue1TrueTrueTrueTrue0.692 gesummvTrue1TrueTrueTrueTrue1.500 symmTrue1TrueTrueTrueTrue0.996 syr2kTrue1TrueFalseTrueFalse1.000 gemverTrue1TrueTrueTrueTrue1.188 syrkTrue2TrueTrueTrueTrue1.303 gemmTrue1TrueTrueTrueTrue1.028 trmmTrue1TrueTrueTrueTrue1.054 adiTrue1TrueFalseTrueFalse1.000 heat-3dTrue1TrueFalseTrueFalse1.000 jacobi-2dTrue1TrueFalseTrueFalse1.000 seidel-2dTrue1TrueTrueTrueTrue1.000 fdtd-2dTrue1TrueFalseTrueFalse1.000 jacobi-1dTrue1TrueTrueTrueTrue0.667 floyd-warshallTrue1TrueTrueTrueTrue1.218 dericheTrue1TrueTrueTrueTrue0.986 nussinovFalse1TrueTrueTrueTrue0.994 correlationTrue1TrueTrueTrueTrue1.137 covarianceTrue1TrueTrueTrueTrue1.001 void kernel_doitgen(int nr , int nq , int np , int 3 D_ARRAY(A,NR ,NQ ,NP ,nr ,nq ,np), int 2D_ARRAY(C4 ,NP , NP ,np ,np), int 2D_ARRAY(sum ,NP ,np)) int r, q, p, s; for (r = 0; r < _PB_NR; r++) for (q = 0; q < _PB_NQ; q++) // Initialize sum array for (p = 0; p < _PB_NP; p++) sum[p] = SCALAR_VAL (0.0); // Optimization attempt: compute the sum and update A in a single loop to reduce memory access latency for (s = 0; s < _PB_NP; s++) for (p = 0; p < _PB_NP; p++) sum[p] += A[r][q][s] * C4[s][p]; A[r][q][p] = sum[p]; // INCORRECT: premature assignment Figure 6. Attempt #1 by the Optimizer: incorrect, rejected by the CBMC Verifier 4.3 Verification Chain Ablations To understand the contribution of individual verification components and their combinations, we conducted an abla- tion study. The goal of this study is to isolate the effect of void kernel_doitgen(int nr , int nq , int np , int 3 D_ARRAY(A,NR ,NQ ,NP ,nr ,nq ,np), int 2D_ARRAY(C4 ,NP , NP ,np ,np), int 2D_ARRAY(sum ,NP ,np)) int r, q, p, s; for (r = 0; r < _PB_NR; r++) for (q = 0; q < _PB_NQ; q++) // Initialize sum array for (p = 0; p < _PB_NP; p++) sum[p] = SCALAR_VAL (0.0); // Compute the sum and update A in a single loop to reduce memory access latency for (s = 0; s < _PB_NP; s++) for (p = 0; p < _PB_NP; p++) sum[p] += A[r][q][s] * C4[s][p]; // Update A with the computed sums for (p = 0; p < _PB_NP; p++) A[r][q][p] = sum[p]; Figure 7. Attempt #2 by the Optimizer: correct and fast (4.33x speedup) different verification setups on system performance, both in terms of correctness and achieved speedup. The results are shown in Table 5. T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework Verification substantially improves correctness. Adding more verification steps consistently increases the overall accuracy of optimized code produced by the system, as in- correct or non-equivalent transformations are rejected and retried by the optimizer. For example, accuracy improves from 60% in the no-verification baseline to 87% with the full verification chain. Importantly, the addition of verification does not hinder speedup. If the verification is too strict or conserva- tive, there is potential for good optimizations (correct and fast) to be rejected. The minimal false rejection rates of the verifiers in our system allow valid optimizations to pass through, which preserves or slightly enhances speedup. A modest increase in average speedup is observed from 1.13 to 1.16. This indicates that catching and filtering incorrect opti- mizations, followed by re-attempts, yields not only correct but also faster optimized code. While all three verification setups shown in the last three rows of Table 5 (combinations of CBMC Verifier and LLM Verifier) are suitable candidates for the T-LLM Compiler workflow, the configuration with Optimizer + Syntax Verifier + CBMC Verifier + LLM Verifier with 3 prompts (based on CBMC decision) consistently produces both high accuracy and speedup. The âMultiple attemptsâ metric quantifies the proportion of kernels that required re-optimization due to verification rejections. Results show that only a small subset of kernels undergo re-attempts; however, these retries meaningfully contribute to the improved accuracy of the final outputs. This demonstrates that the verification chain effectively identifies incorrect optimizations without excessively penalizing the optimizer. Finally, the âTransformed kernelsâ column reflects the fraction of kernels for which the system successfully pro- duced a transformed version of the code. Since the system can, in principle, output the original code after exceeding the maximum number of attempts, this measure ensures that the pipeline is actually producing optimizations. Across all setups, the system achieves a consistently high proportion of transformations, with the maximum number of optimization attempts set to 3. 4.4Classification Performance of the CBMC Verifier In the context of transform verification, type I errors corre- spond to false rejections of correct optimizations, thereby sacrificing opportunities for performance gains. Conversely, type I errors correspond to false acceptances of incorrect op- timizations, which undermine correctness guarantees. The balance between these two error types is critical: reducing false rejections preserves potential speedups, while reducing false acceptances improves the correctness and trustworthi- ness of optimizations produced by the system. Across 400 test cases (multiple runs on PolyBench/C with different prompting strategies), the CBMC Verifier reported an accuracy of 87%, a false rejection rate of 8.4% and a false acceptance rate of 33.8%. The low false rejection rate makes a rejection by CBMC trustworthy (it indicates that a code path violating equivalence between the original and optimized function was found). However, the CBMC Verifier has a high false acceptance rate (does not detect many incorrect optimizations), which likely results from the constrained or bounded nature of the CBMC search. 4.5 Practical Challenges in Alive2 Verification In our experiments, Alive2 did not prove effective for vali- dating equivalence between original and optimized C-level functions. Even at modest loop unwind depths, the tool fre- quently encountered timeouts, failing to complete the refine- ment check. We attribute this to the complexity of PolyBench kernels, which often contain deep nested loops and intricate data dependencies. These structures translate into complex LLVM IR semantics and, consequently, highly non-trivial re- finement relationships that Alive2 must reason about. More- over, Alive2 was primarily designed as a translation valida- tion framework for compiler-driven IR-level optimizations, with particular emphasis on correctly handling undefined behaviour in LLVM. In this context, its strengths do not directly align with verifying C-level transformations gener- ated by our LLM-based optimizer, making it less suitable as a practical verification backend for our system. 5 Conclusion In this paper, we presented a comprehensive framework for optimizing C programs, with a focus on loop-type programs from the PolyBench/C benchmark suite. We demonstrate that a combination of different types of tooling, including compilers, symbolic verifiers, and LLMs, can successfully coexist to provide high-quality optimization solutions. This is particularly evident in the 83% success rate of code gen- eration optimizations, which generally in prior art hovers around 50% for code optimization tasks. While this success rate is high, the overall speedup of transformed programs reaches an impactful 26.7% (one-shot prompt 4). The main reason for this success is the effective utiliza- tion of a wide range of tools, including compilers, symbolic checkers and LLMs. This, in combination with the iterative flow that allows the framework to retry multiple times to successfully create a viable solution, is the key to success. In addition, one step that crucially differentiates us from competing approaches is that a traditional compiler is not removed from the flow of execution. In fact, the frameworkâs output is presented to the BiSheng compiler as input for low-level optimization. The reason we did this stems from the realization that traditional compilers are highly effective in the tasks for which they were designed. What they cannot do is change the input source to unlock optimizations that a programmer would otherwise be able to apply. The T-LLM Fazel et al. Table 5. System performance with different verification setups on PolyBench/C ExperimentTransformed kernels Multiple attempts Accuracy Speedup Optimizer only100%0%60%1.13 Optimizer + Syntax Verifier100%0%73%1.14 Optimizer + Syntax Verifier + CBMC90%7%83%1.19 Optimizer + Syntax Verifier + LLM (single independent prompt)97%17%80%1.18 Optimizer + Syntax Verifier + CBMC + 3-way LLM (3 prompts)90%10%87%1.16 Compiler opens this path wide open with an accurate code generation approach and a collaboration with traditional compiler frameworks. 6 Future Directions While the results presented in this paper are compelling, the natural question becomes: can we do better? The answer is a resounding yes. In our experiments, we found that there is a wider variety of prompting and optimization strategies we could apply to this set of benchmarks, and we have seen up to 52% speedup possible if further advancements are made. To materialize these benefits, we need to solve a number of problems. The first challenge, as previously discussed, lies in de- termining the most appropriate prompt for a given code segment. Prompt effectiveness can vary substantially across kernels and computational settings, making prompt selection a nontrivial component of the optimization pipeline. This variability highlights the need for a systematic investigation into how prompt design interacts with kernel characteristics and influences overall performance. While we introduced an intelligent prompt-recommendation mechanism capable of automatically proposing or selecting suitable prompts, its current performance indicates room for further enhance- ment. Improving this component would not only increase the reliability of prompt selection but also contribute to greater efficiency and scalability in future large-scale optimization systems. A second observation is that, in our prompt analysis, we found one-shot prompting to be slightly more effective in terms of producing better speedups. This was intended to unlock optimization opportunities that the BiSheng com- piler could then exploit to produce fast code. However, two- shot prompts performed well in certain examples as well, which perhaps suggests that rather than combining the re- quest for two optimizations to be considered, sequential requests might be more effective. While this may not always be feasible and sometimes more complex multi-step opti- mizations are required using multi-shot prompts, at least for PolyBench/C-type benchmarks, this approach may be more productive and worth exploring. Finally, there is the problem of handling large code bases. In the benchmarks we explored in this work, most of the functions being optimized fit roughly under 50 lines of code; however, for larger functions that are more complex and longer, optimization remains a challenge. In addition, further optimization efforts will need to attempt to focus on program- wide transformations, which will face this kind of problem much faster. Solving this challenge, however, is how we believe we can reach level 4 in our vision for the T-LLM Compiler. References [1]Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al.2023. GPT-4 Technical Report. arXiv preprint arXiv:2303.08774 (2023). [2]Amir H Ashouri, Mostafa Elhoushi, Yuzhe Hua, Xiang Wang, Muham- mad Asif Manzoor, Bryan Chan, and Yaoqing Gao. 2022. MLGOP- erf: An ML Guided Inliner to Optimize Performance. arXiv preprint arXiv:2207.08389 (2022). [3]Amir H Ashouri, Muhammad Asif Manzoor, Duc Minh Vu, Raymond Zhang, Ziwen Wang, Angel Zhang, Bryan Chan, Tomasz S Czajkowski, and Yaoqing Gao. 2023. ACPO: AI-Enabled Compiler-Driven Program Optimization. arXiv preprint arXiv:2312.09982 (2023). [4]Amir H. Ashouri, Shayan Shirahmad Gale Bagi, Kavin Satheeskumar, Tejas Srikanth, Jonathan Zhao, Ibrahim Saidoun, Ziwen Wang, Bryan Chan, and Tomasz S. Czajkowski. 2026. Protean Compiler: An Agile Framework to Drive Fine-grain Phase Ordering. ACM Trans. Archit. Code Optim. 23, 3, Article 107 (Aug. 2026), 26 pages. doi:10.1145/ 3831596 [5]Ramakrishna Bairi, Atharv Sonwane, Aditya Kanade, Vageesh D C, Arun Iyer, Suresh Parthasarathy, Sriram Rajamani, Balasubramanyan Ashok, and Shashank Shet. 2024. CodePlan: Repository-Level Cod- ing using LLMs and Planning. Proceedings of the ACM on Software Engineering 1, FSE (2024), 675â698. [6]Nathan Binkert, Bradford Beckmann, Gabriel Black, Steven K Rein- hardt, Ali Saidi, Arkaprava Basu, Joel Hestness, Derek R Hower, Tushar Krishna, Somayeh Sardashti, et al.2011. The gem5 simulator. ACM SIGARCH computer architecture news 39, 2 (2011), 1â7. [7] Binghong Chen, Daniel Tarlow, Kevin Swersky, Martin Maas, Pablo Heiber, Ashish Naik, Milad Hashemi, and Parthasarathy Ranganathan. 2022.Learning to Improve Code Efficiency. arXiv preprint arXiv:2208.05297 (2022). [8] Zhi Chen, Zhangxiaowen Gong, Justin Josef Szaday, David C. Wong, David Padua, Alexandru Nicolau, Alexander V. Veidenbaum, Neftali Watkinson, Zehra Sura, Saeed Maleki, Josep Torrellas, and Gerald DeJong. 2017. LORE: A loop repository for the evaluation of compilers. In 2017 IEEE International Symposium on Workload Characterization (IISWC). 219â228. doi:10.1109/IISWC.2017.8167779 [9] Chris Cummins, Volker Seeker, Dejan Grubisic, Baptiste Roziere, Jonas Gehring, Gabriel Synnaeve, and Hugh Leather. 2025. LLM Compiler: Foundation Language Models for Compiler Optimization. In Proceed- ings of the 34th ACM SIGPLAN International Conference on Compiler Construction. 141â153. T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework [10]Spandan Garg, Roshanak Zilouchian Moghaddam, Colin B Clement, Neel Sundaresan, and Chen Wu. 2022. DeepDev-PERF: A Deep Learning-based Approach for Improving Software Performance. In Proceedings of the 30th ACM Joint European Software Engineering Con- ference and Symposium on the Foundations of Software Engineering. 948â958. [11] Spandan Garg, Roshanak Zilouchian Moghaddam, and Neel Sundare- san. 2025. RAPGen: An Approach for Fixing Code Inefficiencies in Zero-Shot. In 2025 IEEE/ACM 47th International Conference on Soft- ware Engineering: Software Engineering in Practice (ICSE-SEIP). IEEE, 124â135. [12]Benny Godlin and Ofer Strichman. 2013. Regression verification: prov- ing the equivalence of similar programs. Software Testing, Verification and Reliability 23, 3 (2013), 241â258. [13] Daniel Kroening and Michael Tautschnig. 2014. CBMC â C Bounded Model Checker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 389â391. [14]Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Frame- work for Lifelong Program Analysis & Transformation. In International symposium on code generation and optimization, 2004. CGO 2004. IEEE, 75â86. [15]Hannah Lin, Martin Maas, Maximilian Roquemore, Arman Hasan- zadeh, Fred Lewis, Yusuf Simonson, Tzu-Wei Yang, Amir Yazdan- bakhsh, Deniz AltinbĂźken, Florin Papa, et al.2025. ECO: An LLM- Driven Efficient Code Optimizer for Warehouse Scale Computers. arXiv preprint arXiv:2503.15669 (2025). [16]Nuno P Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: Bounded Translation Validation for LLVM. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 65â79. [17] Na Meng, Miryung Kim, and Kathryn S McKinley. 2011. Systematic Editing: Generating Program Transformations from an Example. ACM Sigplan Notices 46, 6 (2011), 329â342. [18]Anders Miltner, Sumit Gulwani, Vu Le, Alan Leung, Arjun Radhakr- ishna, Gustavo Soares, Ashish Tiwari, and Abhishek Udupa. 2019. On the fly synthesis of edit suggestions. Proceedings of the ACM on Programming Languages 3, OOPSLA (2019), 1â29. [19]Meredith Ringel Morris, Jascha Sohl-Dickstein, Noah Fiedel, Tris Warkentin, Allan Dafoe, Aleksandra Faust, Clement Farabet, and Shane Legg. 2024. Position: Levels of AGI for Operationalizing Progress on the Path to AGI. In Forty-first International Conference on Machine Learning. [20]Pedro Orvalho and Marta Kwiatkowska. 2025. PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C. arXiv preprint arXiv:2508.08171 (2025). [21]Ruchir Puri, David S Kung, Geert Janssen, Wei Zhang, Giacomo Domeniconi, Vladmir Zolotov, Julian Dolby, Jie Chen, Mihir Choud- hury, Lindsey Decker, et al.2021. CodeNet: A Large-Scale AI for Code Dataset for Learning a Diversity of Coding Tasks. arXiv preprint arXiv:2105.12655 1035 (2021). [22]Alexander Shypula, Aman Madaan, Yimeng Zeng, Uri Alon, Ja- cob Gardner, Milad Hashemi, Graham Neubig, Parthasarathy Ran- ganathan, Osbert Bastani, and Amir Yazdanbakhsh. 2023. Learning Performance-Improving Code Edits. arXiv preprint arXiv:2302.07867 (2023). [23]Alexander Shypula, Aman Madaan, Yimeng Zeng, Uri Alon, Ja- cob Gardner, Milad Hashemi, Graham Neubig, Parthasarathy Ran- ganathan, Osbert Bastani, and Amir Yazdanbakhsh. 2025. Automated High-Level Code Optimization for Warehouse Performance. IEEE Micro (2025). [24]Jubi Taneja, Avery Laird, Cong Yan, Madan Musuvathi, and Shu- vendu K Lahiri. 2025. LLM-Vectorizer: LLM-based Verified Loop Vec- torizer. In Proceedings of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization. 137â149. [25]Qwen Team. 2024.Qwen2 technical report. arXiv preprint arXiv:2407.10671 (2024). [26] Mircea Trofin, Yundi Qian, Eugene Brevdo, Zinan Lin, Krzysztof Choro- manski, and David Li. 2021. MLGO: A Machine Learning Framework for Compiler Optimization. arXiv preprint arXiv:2101.04808 (2021). [27]Huanting Wang, Zhanyong Tang, Cheng Zhang, Jiaqi Zhao, Chris Cummins, Hugh Leather, and Zheng Wang. 2022. Automating re- inforcement learning architecture design for code optimization. In Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction. 129â143. Fazel et al. A Verification & Optimization Prompts This section presents the prompt collection we used in our work. Given below are two versions of a C function that should compute the same result. Note that the second version was an attempt to optimize the original code , and the optimization may have broken the logic or the behavior of the original function (incorrect optimization). On the other hand , it may be a correctly optimized version as well. Your goal is to determine whether the optimized version of the code is functionally equivalent to the original version. Original function: ORIGINAL_CODE Optimized version: TRANSFORMED_CODE Steps to verify functional equivalence: 1. Analyze the code paths/ flow and identify key operations and their order in both versions 2. Check for data dependencies and whether they are correctly preserved in the optimized version 3. Analyze boundary conditions and loop invariants 4. Compare mathematical equivalence of computations Output format instructions: - First , give your analysis of the the two code versions - List of key similarities and differences detected - Your verdict on functional equivalence: *MUST produce this output *: : [Only use the phrases: EQUIVALENT/ NOT_EQUIVALENT] - Confidence level on your verdict: [HIGH/MEDIUM/LOW] Figure 8. Single independent LLM Verifier prompt For further context , consider that the C Bounded Model Checker (CBMC) tool has asserted that the optimized code is equivalent to the original. CBMC does this via symbolical execution by asserting that function calls to original and optimized versions produce the same output for a defined input space. However , the input search space is small for computational feasibility (eg: small input arrays), so its' equivalent' decision *cannot* be treated as final (it's possible that non -equivalence exists outside its search space). Leverage the given context , but perform your own careful analysis Figure 9. LLM Verifier prompt with context on CBMC decision: accept (equivalent) For further context , consider that the C Bounded Model Checker (CBMC) tool has asserted that the optimized code is not equivalent to the original. CBMC does this via symbolical execution by asserting that function calls to original and optimized versions produce different outputs for some case of input within a defined input space. This makes it highly likely that the optimized code is not equivalent to the original. However , the CBMC decision can also be incorrect for various practical reasons. Leverage the given context , but perform your own careful analysis Figure 10. LLM Verifier prompt with context on CBMC decision: reject (not equivalent) T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework You are a helpful assistant specialized in optimizing C code. Your goals are to improve the execution speed of the provided code by applying loop -level optimizations (loop unrolling , loop jamming , loop tiling , etc.) while preserving the logic of the code. Rules to follow: 1. Preserve the logic of the code. 2. DO NOT change function signatures. 3. DO NOT define macros or include any header files. 4. DO NOT introduce calls to any undefined functions (e.g. min , max). 5. DO NOT use any external libraries. 6. DO NOT use any parallelization or concurrency libraries (e.g., OpenMP). 7. Do NOT use any compiler pragmas. In particular , any form of #pragma unroll (...) , #pragma ivdep , #pragma omp , or any vendor -specific variant is strictly disallowed. If you include any #pragma , your answer is invalid. 8. DO NOT produce any line containing #pragma. This includes #pragma unroll(N) for any integer N. If a #pragma appears anywhere in your output , that output is invalid. 9. Return only valid C code with the requested transformations. 10. Enclose the final optimized code only between [OPT] and [/OPT] tags , with no extra text. If you fail to follow any of the rules , the answer will be considered invalid. Figure 11. Optimizer system prompt You are a specialized assistant for compilers and code optimization in C. You will help me optimize my C code. Follow these steps to optimize the given C code: 1. Analyze the provided C code to understand its functionality. 2. Optimize it to improve its execution running time by applying loop optimization techniques such as loop unrolling , loop jamming , loop fusion , loop tiling , or other relevant optimizations that can help reduce execution time. 3. Wrap your final optimized C code between [OPT] and [/OPT] tags. Only return the best optimized code. Rules to follow: 1. Put one and only one version of the optimized code between [OPT] and [/OPT] tags. 2. Follow the steps that are defined in the prompt. 3. Do NOT use any external libraries. 4. Do NOT change the provided function signature , name or arguments. 5. Do NOT use undefined functions like min , max , or swap. 6. Do NOT include any header files or define any macros. 7. Do NOT write any function with the name "main". Here is the original C code: ORIGINAL_CODE Return only the most optimized C code within [OPT] and [/OPT] tags. Figure 12. Optimizer zero-shot prompt Fazel et al. Below is a negative example , demonstrating that compiler pragmas (e.g., #pragma ivdep , #pragma unroll , etc.) are not allowed: NEGATIVE EXAMPLE (Input): [ORG] void anotherNegativeExample(int *arr , int n) #pragma unroll(N) for (int i = 0; i < n; i++) arr[i] += 2; [/ORG] NEGATIVE EXAMPLE (Output): [OPT] // We remove any compiler directive , especially #pragma unroll(N). // Instead , we manually unroll or keep the loop as is. void anotherNegativeExample(int *arr , int n) // Example: manually unroll by factor 2, if desired: int i; for (i = 0; i < n - 2; i += 2) arr[i] += 2; arr[i+1] += 2; for (; i < n; i++) arr[i] += 2; [/OPT] Below are several examples of unoptimized code (within [ORG] and [/ORG]) paired with their optimized versions ( within [OPT] and [/OPT]). EXAMPLES Now , using the same approach , please optimize the following code. Return only the optimized version between [OPT] and [/OPT] tags , with nothing else outside those tags: [ORG] ORIGINAL_CODE [/ ORG] Figure 13. Optimizer few-shot prompts Below is your previously returned code , which failed verification , followed by the verifier's feedback. Please revise the code so that it addresses the verifier's concerns. Continue to follow the rules about preserving function signatures , avoiding macros or undefined functions , avoiding compiler pragmas , and preserving the original logic. Here is the original code: [ORG] ORIGINAL [/ORG] Your previously returned code which failed verification: [OPT] FAILED_CODE [/OPT] Verifier's feedback: FEEDBACK Now , please produce a corrected version of the code that addresses the feedback , adheres to all the rules , and returns only the optimized C code between [OPT] and [/OPT] tags with no extra text. Figure 14. Optimizer feedback prompt T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework EXAMPLE 1 (Input): [ORG] void doubleElements(int *arr , int n) for (int i = 0; i < n; i++) arr[i] *= 2; [/ORG] EXAMPLE 1 (Output): Optimization Technique: Loop Unrolling [OPT] void doubleElements(int *arr , int n) int i; for (i = 0; i <= n - 4; i += 4) arr[i] *= 2; arr[i+1] *= 2; arr[i+2] *= 2; arr[i+3] *= 2; // Handle leftover elements for (; i < n; i++) arr[i] *= 2; [/OPT] EXAMPLE 2 (Input): [ORG] void processArrays(int *arr1 , int *arr2 , int n) for (int i = 0; i < n; i++) arr1[i] += 1; for (int i = 0; i < n; i++) arr2[i] += 2; [/ORG] EXAMPLE 2 (Output): Optimization Technique: Loop Jamming [OPT] void processArrays(int *arr1 , int *arr2 , int n) for (int i = 0; i < n; i++) arr1[i] += 1; arr2[i] += 2; [/OPT] EXAMPLE 3 (Input): [ORG] void addMatrices(int *A, int *B, int *C, int N) for (int i = 0; i < N; i++) for (int j = 0; j < N; j++) C[i*N + j] = A[i*N + j] + B[i*N + j]; [/ORG] EXAMPLE 3 (Output): Optimization Technique: Loop Tiling [OPT] void addMatrices(int *A, int *B, int *C, int N) int tileSize = 4; for (int i0 = 0; i0 < N; i0 += tileSize) for (int j0 = 0; j0 < N; j0 += tileSize) for (int i = i0; i < i0 + tileSize && i < N; i++) for (int j = j0; j < j0 + tileSize && j < N; j++) C[i*N + j] = A[i*N + j] + B[i*N + j]; Figure 15. Optimizer examples used in few-shot prompts and recommender (1/2) Fazel et al. EXAMPLE 4 (Input): [ORG] void sumCols(int *matrix , int *result , int rows , int cols) for (int j = 0; j < cols; j++) result[j] = 0; for (int j = 0; j < cols; j++) for (int i = 0; i < rows; i++) result[j] += matrix[i*cols + j]; [/ORG] EXAMPLE 4 (Output): Optimization Technique: Loop Interchange [OPT] void sumCols(int *matrix , int *result , int rows , int cols) // Initialize result for (int j = 0; j < cols; j++) result[j] = 0; // Interchange loop order for better memory locality for (int i = 0; i < rows; i++) for (int j = 0; j < cols; j++) result[j] += matrix[i*cols + j]; [/OPT] EXAMPLE 5 (Input): [ORG] void processArrays(int a[], int b[], int c[], int size) // One loop performs two independent operations for (int i = 0; i < size; i++) b[i] = a[i] * 2; // Task 1 c[i] = a[i] + 10; // Task 2 [/ORG] EXAMPLE 5 (Output): Optimization Technique: Loop Distribution (Fusion) [OPT] void processArrays(int a[], int b[], int c[], int size) // First loop: Task 1 for (int i = 0; i < size; i++) b[i] = a[i] * 2; // Second loop: Task 2 for (int i = 0; i < size; i++) c[i] = a[i] + 10; [/OPT] Figure 16. Optimizer examples used in few-shot prompts and recommender (2/2) T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework You are a specialized assistant for compilers and code optimization in Given an Original Code snippet , without access to the Optimized Code , analyze the code and select optimization strategies that could be applied to improve performance from the list below: - Loop Unrolling - Loop Distribution(Fission) - Loop Tiling - Loop Interchange - Loop Unroll and Jam If the code is already optimal or no strategies are applicable , respond with "No Loop Optimization Needed ". Provide the list of applicable strategies in this format: [STR] - [Strategy 1] - [Strategy 2] ... - [Strategy N] [/STR] --- Now analyze the code: ORIGINAL_CODE #### Optimization Suggestions: Figure 17. Recommender strategy prompt You are an expert code optimization assistant. Your task is to analyze the provided C code snippets and apply each given optimization strategy to enhance performance. Here are the optimization strategies you can use: STRATEGIES Below are several examples of unoptimized code (within [ORG] and [/ORG]) paired with their optimized versions ( within [OPT] and [/OPT]) that used the given strategies. EXAMPLES Now , using the same approaches to optimize the following code. Return only the optimized version between [OPT] and [/OPT] tags , with nothing else outside those tags: [ORG] ORIGINAL_CODE [/ORG] Figure 18. Optimizer prompt using recommender suggestions You are an expert code optimization assistant. Your task is to analyze the provided C code snippets and apply each given optimization strategy to enhance performance. Here are the optimization strategies you can use: STRATEGIES Below are several examples of unoptimized code (within [ORG] and [/ORG]) paired with their optimized versions ( within [OPT] and [/OPT]) that used the given strategies. EXAMPLES Explain how each optimization strategy has been applied in the examples above. Provide a brief description of the techniques used in each optimized code snippet. Use the following optimization strategies and the provided descriptions to optimize the given C code snippet. Wrap your optimized code between [OPT] and [/OPT] tags. Here is the optimization strategies and their descriptions: STRATEGIES EXPLANATION Here is the C code to optimize: [ORG] ORIGINAL_CODE [/ORG] Return only the optimized version between [OPT] and [/OPT] tags , with nothing else outside those tags. Figure 19. Optimizer prompt using recommender suggestions using chain of thought prompting