Enhancing Translation Validation of Compiler Transformations with Large Language Models

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 utilizes the existing tools, like Alive2, to perform initial validation. For transformations deemed unsolvable by traditional methods, our approach leverages fine-tuned LLMs to predict soundness or unsoundness, with subsequent fuzzing applied to identify counterexamples for unsound transformations. Our approach has proven effective in complex scenarios, such as deep-learning accelerator designs, enhancing the reliability of compiler transformations.