Enhancing Translation Validation of Compiler Transformations with Large Language Models

Authors

Fei Xie, Portland State University
Yanzhao Wang, Portland State UniversityFollow

Document Type

Pre-Print

Publication Date

2024

Abstract

This paper presents a framework that integrates Large Language Models (LLMs) into translation validation, targeting LLVM compiler transformations where formal verification tools fall short. Our framework first utilizes existing formal verification tools for translation validation. In this work, we use Alive2, a well-known tool in LLVM compiler verification, as an example. When formal verification tools are unable to confirm a transformation's soundness, our framework employs fine-tuned LLMs for prediction. It then applies fuzzing to transformations predicted as potentially unsound by the LLMs due to return values or memory inconsistencies, aiming to find counterexamples. In cases where transformations are unsound for other reasons or sound, or if no counterexamples emerge, the framework directly reports these outcomes without further fuzzing. This methodology has shown effectiveness in complex application such as deep-learning accelerator designs, where traditional formal verification tools struggle.

Rights

Description

Preprint of an article submitted for consideration in International Journal of Software Engineering and Knowledge Engineering © 2024 World Scientific Publishing Company

https://doi.org/10.1142/S0218194024500475

DOI

10.1142/S0218194024500475

Persistent Identifier

https://archives.pdx.edu/ds/psu/42722

Citation Details

Wang, Y., & Xie, F. (2024). Enhancing Translation Validation of Compiler Transformations with Large Language Models. International Journal of Software Engineering and Knowledge Engineering, 1-13.