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, developing domain-specific languages (DSLs), and improving optimization techniques. 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 techniques to find semantically equivalent translations.