LLM-Vectorizer： LLM-Based Verified Loop Vectorizer

中文摘要

向量化是一种强大的优化技术，能够显著提升高性能计算应用程序在处理大规模数据数组时的性能。尽管自动向量化已经研究了几十年，编译器仍然经常错过向量化代码的机会。另一方面，使用编译器内置函数手动编写向量化代码仍然是一项复杂且容易出错的任务，需要对特定架构和编译器有深入的了解。
在本文中，我们评估了==大型语言模型==（LLMs）==从处理单个数组元素的标量程序生成向量化（单指令多数据，SIMD）代码的潜力==。我们提出了一种基于有限状态机多代理的新方法，==利用LLMs和基于测试的反馈来生成向量化代码==。我们的研究结果表明，与最先进的编译器（如Intel编译器、GCC和Clang）相比，LLMs能够生成高性能的向量化代码，运行速度提升范围从1.1倍到9.4倍。
为了验证向量化代码的正确性，我们使用了Alive2，这是一个领先的用于LLVM IR的有界翻译验证工具。我们描述了一些特定领域的技术，以提高Alive2在我们基准数据集上的可扩展性。总体而言，我们的方法能够在TSVC基准数据集上验证==38.2%的向量化为正确==。（只有 38.2%吗）

using LLM+PGO→Vectorize with Alive2 on TSVC > ICC/GCC/LLVM

Background

背景
LoopVec 在 HPC、AI 非常重要
Auto LoopVec 的（编译器级别的）静态分析不精确
LoopVec 依赖于“数据依赖分析”，编译器成本模型过于保守
观察
AVX2 提供了 Intrinsics 函数如 _mm256_loadu_si256
(问题所在)向量化成了开发者而不是编译器的责任
能否利用大模型和形式化验证，自动将标量 C 程序转为 AVX2 内建函数的向量化程序?
一个动机程序展示了 GCC 和 LLVM 容易分析错误循环导致无法优化
GPT-4 可以优化，但是不能保证其他简洁程序的正确性

小总结
LLM 有生成高效向量化代码的能力
Alive2 工具能够检测转换的正确性
使用 Alive2 反馈错误生成的程序指导重新生成代码
有一些测试可以经由一次 LLM 便可以成功生成
贡献
评估 LLM 在向量化任务中的能力
基于 AI 代理（AI-agents-based）的新方法
形式化验证技术
领域特定优化