一句话：提出用程序合成与验证自动把通用语言程序翻译为语义等价的张量运算，替代传统模式匹配。
张量运算广泛用于图像处理、深度学习和科学计算。硬件与软件社区分别通过新硬件和领域特定语言来提升张量处理效率，而编译器是连接两者的关键。本文旨在构建高效编译器，把通用语言编写的程序翻译为张量运算，使其能利用这些优化。与传统模式匹配方法不同，作者提出搜索式翻译：借助程序合成寻找可能的翻译候选，并用验证确保源程序与目标张量运算语义等价。摘要未报告具体实现和实验结果，评估预计围绕翻译正确性及生成张量代码的性能展开。
Tensor operations are essential for various tasks, including image processing, deep learning, and scientific computing. Both hardware and software communities are working to make tensor processing more efficient. This includes creating new hardware and developing domain-specific languages (DSLs). A crucial link between these communities is the compiler. In this work, we propose developing efficient compilers that translate programs written in general-purpose languages into tensor operations, enabling them to benefit from these optimizations. Unlike traditional pattern-matching approaches, our method uses program synthesis and verification to find semantically equivalent translations.