一句话：提出首个可验证任意秩与尺寸张量图重写正确性的自动验证系统 TensorRight。
张量编译器依赖张量图重写来优化深度学习模型，但重写需在任意秩和尺寸下保持语义；现有工作只能验证具体秩，无法覆盖无界情形。本文提出 TensorRight，首个针对任意秩与尺寸输入的自动验证系统。其核心是 TensorRight DSL，用 aggregated-axis 表示重写规则以推理无界多个轴；作者证明存在张量秩上界，使所有有界实例验证通过即可推出无界正确性，并利用指称语义设计计算秩上界的算法。TensorRight 据此生成有限个有界验证证明义务，再经符号执行交给 SMT 求解器自动验证。在 XLA 代数化简器规则上，175 条中可完整证明 115 条，而最接近的自动有界系统仅能表达 18 条。
Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting. To fill this gap, we introduce T ensor R ight , the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, T ensor R ight DSL, to represent rewrite rules using a novel axis definition, called aggregated-axis , which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of T ensor R ight DSL. T ensor R ight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate T ensor R ight ’s verification capabilities by implementing rewrite rules present in XLA ’s algebraic simplifier. The results demonstrate that T ensor R ight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic, bounded -verification system can express only 18 of these rules.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AroraLJXHPLNMBSM25,
title = {TensorRight: Automated Verification of Tensor Graph Rewrites},
author = {Jai Arora and Sirui Lu and Devansh Jain and Tianfan Xu and Farzin Houshmand and Phitchaya Mangpo Phothilimthana and Mohsen Lesani and Praveen Narayanan and Karthik Srinivasa Murthy and Rastislav Bodik and Amit Sabne and Charith Mendis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704865}
}