中文摘要

向量化是一种强大的优化技术，能够显著提升高性能计算应用程序在处理大规模数据数组时的性能。尽管自动向量化已经研究了几十年，编译器仍然经常错过向量化代码的机会。另一方面，使用编译器内置函数手动编写向量化代码仍然是一项复杂且容易出错的任务，需要对特定架构和编译器有深入的了解。
在本文中，我们评估了大型语言模型（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 可以优化，但是不能保证其他简洁程序的正确性
    image-20250304205307039.webp

小总结

  • LLM 有生成高效向量化代码的能力
  • Alive2 工具能够检测转换的正确性
  • 使用 Alive2 反馈错误生成的程序指导重新生成代码
  • 有一些测试可以经由一次 LLM 便可以成功生成

贡献

  • 评估 LLM 在向量化任务中的能力
  • 基于 AI 代理（AI-agents-based）的新方法
  • 形式化验证技术
  • 领域特定优化

个人总结

这是一篇中规中矩的论文，无论是从动机还是使用的方法，可以说是这一行老生长谈的套路。但是一旦有人开辟了这一领域，后续再创新就必须考虑的多一些。
他用了 pass@k 来验证输出的正确性。这一点其实是存疑的。

附录