This paper presents a framework that integrates Large Language Models (LLMs) into translation validation, targeting LLVM compiler transformations where formal verification tools are insufficient. Our framework first utilizes existing formal verification frameworks for translation validation. In this work, we use Alive2, a well-known tool in LLVM compiler verification, as an example. When formal verification frameworks are unable to confirm a transformation's soundness, our framework employs fine-tuned LLMs for prediction. It applies fuzzing to transformations predicted as potentially unsound by the LLMs due to return value 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 areas like deep-learning accelerator design, where traditional tools struggle.

翻译：本文提出了一种将大语言模型（LLMs）集成到编译验证中的框架，针对LLVM编译器变换中形式化验证工具不足的问题。该框架首先利用现有形式化验证框架进行翻译验证，本研究以LLVM编译器验证领域知名工具Alive2为例。当形式化验证框架无法确认变换的正确性时，我们的框架采用微调后的LLM进行预测。对于LLM因返回值或内存不一致而预测为潜在不安全的变换，框架通过模糊测试寻找反例。当变换因其他原因不安全或安全时，若未发现反例，框架直接报告这些结果而无需进一步模糊测试。该方法在深度学习加速器设计等传统工具难以处理的复杂领域展现出有效性。