This paper presents Prism, the first symbolic superoptimizer for tensor programs. The key idea is sGraph, a symbolic, hierarchical representation that compactly encodes large classes of tensor programs by symbolically representing some execution parameters. Prism organizes optimization as a two-level search: it constructs symbolic graphs that represent families of programs, and then instantiates them into concrete implementations. This formulation enables structured pruning of provably suboptimal regions of the search space using symbolic reasoning over operator semantics, algebraic identities, and hardware constraints. We develop techniques for efficient symbolic graph generation, equivalence verification via e-graph rewriting, and parameter instantiation through auto-tuning. Together, these components allow Prism to bridge the rigor of exhaustive search with the scalability required for modern ML workloads. Evaluation on five commonly used LLM workloads shows that Prism achieves up to $2.2\times$ speedup over best superoptimizers and $4.9\times$ over best compiler-based approaches, while reducing end-to-end optimization time by up to $3.4\times$.

翻译：本文提出Prism，首个面向张量程序的符号化超级优化器。其核心思想是sGraph——一种符号化、层次化表示，通过符号化表征部分执行参数，紧凑地编码大规模张量程序类别。Prism将优化组织为双层搜索：构建表示程序族的有向符号图，随后将其实例化为具体实现。这种形式化方法利用对算子语义、代数恒等式及硬件约束的符号化推理，对搜索空间中可证明为次优的区域进行结构化剪枝。我们发展了高效符号图生成技术、基于e-graph重写的等价性验证方法，以及通过自动调优的参数实例化技术。这些组件共同使Prism能够将穷举搜索的严谨性与现代机器学习工作负载所需的可扩展性相融合。对五个常用大语言模型工作负载的评估表明，Prism相较最优超级优化器实现最高2.2倍加速比，相较最优编译器方法实现最高4.9倍加速比，同时端到端优化时间减少最高3.4倍。