一句话：提出机器化验证框架，用层级抽象定义和组合稀疏张量格式，并在 ATL 调度重写中可靠地将稠密程序优化为稀疏程序。
论文解决稀疏张量程序优化中缺少可组合、可验证格式抽象的问题。作者扩展原先仅支持稠密算子的 ATL 张量语言与调度框架，提出层级化抽象：按维度用编码、访问和迭代函数描述张量格式，并给出保证稀疏结构正确表示原稠密张量的形式性质。基于该抽象，他们组合式定义格式无关的多维压缩与解压缩，证明抽象稀疏格式的顶层可靠性定理；再将该定理作为伴随对重写定理，通过 ATL 现有调度重写把稀疏数据结构和迭代引入稠密内核。最终可从稠密操作数程序推导出可证明语义等价的优化稀疏程序，并证明一组可组合的层级格式实例，覆盖多种经典多维张量压缩格式。
In this paper, we introduce a verified framework for defining and composing sparse tensor formats. We extend the ATL tensor language and scheduling framework, which formerly could only express dense tensor kernels. We define a levelized abstraction to describe per-dimension tensor formats via their encoding routines, access and iteration functions, and formal properties enforcing soundness of the sparse structures as representations of the original dense tensors. Using this abstraction, we compositionally define format-agnostic, multidimensional compression and decompression functions that are used to express the top-level soundness theorem for these abstract sparse tensor formats. We then use this soundness theorem as an adjoint-pair rewrite theorem to introduce sparse data structures and iteration into a dense tensor kernel via the existing scheduling-rewrite framework of ATL. Overall, we are able to start with a program computing over dense operands and derive a proven semantically equivalent, optimized program computing over sparse structures. We further prove a minimal set of instances of the level-format abstraction, which can be composed and passed as parameters to compression to capture a broad range of canonical, multidimensional tensor-compression formats.
@article{LiuBKCR26,
title = {A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs},
author = {Amanda Liu and Gilbert Louis Bernstein and Shoaib Kamil and Adam Chlipala and Jonathan Ragan-Kelley},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808261}
}