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.

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