{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:31Z","timestamp":1780994611739,"version":"3.54.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2338739, CCF-2122950, ITE-2132318, CCF-2437238"],"award-info":[{"award-number":["CCF-2338739, CCF-2122950, ITE-2132318, CCF-2437238"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-2-0032, D22AP00146-00"],"award-info":[{"award-number":["FA8750-16-2-0032, D22AP00146-00"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["ACE Center, CONIX Research Center"],"award-info":[{"award-number":["ACE Center, CONIX Research Center"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>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.<\/jats:p>\n                  <jats:p>\n                    To fill this gap, we introduce T\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    , 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\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    DSL, to represent rewrite rules using a novel axis definition, called\n                    <jats:italic toggle=\"yes\">aggregated-axis<\/jats:italic>\n                    , 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\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    DSL. T\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    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\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    \u2019s verification capabilities by implementing rewrite rules present in\n                    <jats:monospace>XLA<\/jats:monospace>\n                    \u2019s algebraic simplifier. The results demonstrate that T\n                    <jats:sc>ensor<\/jats:sc>\n                    R\n                    <jats:sc>ight<\/jats:sc>\n                    can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic,\n                    <jats:italic toggle=\"yes\">bounded<\/jats:italic>\n                    -verification system can express only 18 of these rules.\n                  <\/jats:p>","DOI":"10.1145\/3704865","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"832-863","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["TensorRight: Automated Verification of Tensor Graph Rewrites"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7759-481X","authenticated-orcid":false,"given":"Jai","family":"Arora","sequence":"first","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2757-7603","authenticated-orcid":false,"given":"Sirui","family":"Lu","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1442-1502","authenticated-orcid":false,"given":"Devansh","family":"Jain","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2528-0507","authenticated-orcid":false,"given":"Tianfan","family":"Xu","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8516-2401","authenticated-orcid":false,"given":"Farzin","family":"Houshmand","sequence":"additional","affiliation":[{"name":"Google, Sunnyvale, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3492-3690","authenticated-orcid":false,"given":"Phitchaya Mangpo","family":"Phothilimthana","sequence":"additional","affiliation":[{"name":"Google DeepMind, Mountain View, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3165-2322","authenticated-orcid":false,"given":"Mohsen","family":"Lesani","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz, Santa Cruz, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3331-9627","authenticated-orcid":false,"given":"Praveen","family":"Narayanan","sequence":"additional","affiliation":[{"name":"Google, Sunnyvale, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6063-9653","authenticated-orcid":false,"given":"Karthik Srinivasa","family":"Murthy","sequence":"additional","affiliation":[{"name":"Google, Sunnyvale, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6639-1647","authenticated-orcid":false,"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"Google DeepMind, San Francisco, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2179-0078","authenticated-orcid":false,"given":"Amit","family":"Sabne","sequence":"additional","affiliation":[{"name":"Google, Sunnyvale, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8140-2321","authenticated-orcid":false,"given":"Charith","family":"Mendis","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Urbana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"265","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek G. Murray, Benoit Steiner, Paul Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. 2016. TensorFlow: A System for Large-Scale Machine Learning. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 265\u2013283. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/abadi"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640366"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Jai Arora Sirui Lu Devansh Jain Tianfan Xu Farzin Houshmand Phitchaya Mangpo Phothilimthana Mohsen Lesani Praveen Narayanan Karthik Srinivasa Murthy Rastislav Bodik Amit Sabne and Charith Mendis. 2024. Artifact for \"TensorRight: Automated Verification of Tensor Graph Rewrites\". https:\/\/doi.org\/10.5281\/zenodo.14159871 10.5281\/zenodo.14159871","DOI":"10.5281\/zenodo.14159871"},{"key":"e_1_3_2_5_2","unstructured":"The JAX Authors. 2024. Named axes and easy-to-revise parallelism with xmap. https:\/\/web.archive.org\/web\/20240320140219\/https:\/\/jax.readthedocs.io\/en\/latest\/notebooks\/xmap_tutorial.html archived 2024-03-20."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1168917.1168906"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294107"},{"key":"e_1_3_2_9_2","unstructured":"James Bradbury Roy Frostig Peter Hawkins Matthew James Johnson Chris Leary Dougal Maclaurin George Necula Adam Paszke Jake VanderPlas Skye Wanderman-Milne and Qiao Zhang. 2018. JAX: composable transformations of Python+NumPy programs. http:\/\/github.com\/google\/jax"},{"key":"e_1_3_2_10_2","unstructured":"JAX Contributors. 2024. jax.lax module. https:\/\/jax.readthedocs.io\/en\/latest\/jax.lax.html"},{"key":"e_1_3_2_11_2","unstructured":"ONNX Contributors. 2024. ONNX. https:\/\/onnx.ai\/onnx\/operators\/"},{"key":"e_1_3_2_12_2","unstructured":"OpenXLA Contributors. 2024. OpenXLA Project. https:\/\/web.archive.org\/web\/20241009145043\/https:\/\/openxla.org\/xla"},{"key":"e_1_3_2_13_2","unstructured":"OpenXLA Contributors. 2024. XLA-HLO Operation Semantics. https:\/\/openxla.org\/xla\/operation_semantics"},{"key":"e_1_3_2_14_2","unstructured":"PyTorch Contributors. 2024. Named Tensors. https:\/\/web.archive.org\/web\/20240703124627\/https:\/\/pytorch.org\/docs\/stable\/named_tensor.html archived 2024-07-03."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_12"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.17"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359630"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446751"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_25_2","volume-title":"ERTS 2018: Embedded Real Time Software and Systems","author":"K\u00e4stner Daniel","year":"2018","unstructured":"Daniel K\u00e4stner, Ulrich W\u00fcnsche, J\u00f6rg Barrho, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. In ERTS 2018: Embedded Real Time Software and Systems. SEE. http:\/\/xavierleroy.org\/publi\/erts2018_compcert.pdf"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498717"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656390"},{"key":"e_1_3_2_28_2","unstructured":"Zhengyang Liu Stefan Mada and John Regehr. 2023. Minotaur: A SIMD-Oriented Synthesizing Superoptimizer. arXiv:2306.00229 [cs.PL] https:\/\/arxiv.org\/abs\/2306.00229"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571209"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428234"},{"key":"e_1_3_2_32_2","unstructured":"Adam Paszke Sam Gross Soumith Chintala Gregory Chanan Edward Yang Zachary DeVito Zeming Lin Alban Desmaison Luca Antiga and Adam Lerer. 2017. Automatic differentiation in PyTorch. In NIPS-W."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_34_2","unstructured":"James Reed Zachary DeVito Horace He Ansley Ussery and Jason Ansel. 2022. torch.fx: Practical Program Capture and Transformation for Deep Learning in Python. In Proceedings of Machine Learning and Systems D. Marculescu Y. Chi and C. Wu (Eds.) Vol. 4. 638\u2013651. https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2022\/file\/7c98f9c7ab2df90911da23f9ce72ed6e-Paper.pdf"},{"key":"e_1_3_2_35_2","unstructured":"Raimondas Sasnauskas Yang Chen Peter Collingbourne Jeroen Ketema Gratian Lup Jubi Taneja and John Regehr. 2018. Souper: A Synthesizing Superoptimizer. arXiv:1711.04422 [cs.PL] https:\/\/arxiv.org\/abs\/1711.04422"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499368.2451150"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460945.3464953"},{"key":"e_1_3_2_39_2","first-page":"37","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Wang Haojie","year":"2021","unstructured":"Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. 2021. PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated Corrections. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 37\u201354. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/wang"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498686"},{"key":"e_1_3_2_42_2","unstructured":"Yichen Yang Phitchaya Phothilimthana Yisu Wang Max Willsey Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. In Proceedings of Machine Learning and Systems A. Smola A. Dimakis and I. Stoica (Eds.) Vol. 3. 255\u2013268. https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2021\/file\/cc427d934a7f6c0663e5923f49eba531-Paper.pdf"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704865","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:22Z","timestamp":1770200242000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704865"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704865"],"URL":"https:\/\/doi.org\/10.1145\/3704865","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}