Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk from POPL 2025 introduces TensorRight, the first automatic verification system capable of verifying tensor graph rewrites for input tensors of arbitrary rank and size. Discover how tensor compilers, crucial for generating efficient code for deep learning models, can benefit from this groundbreaking approach to optimization verification. Learn about the novel TensorRight DSL language with its aggregated-axis definition that enables reasoning about an unbounded number of axes. The presentation explains how the system proves that bounded verification under certain conditions implies correctness in unbounded settings, and demonstrates its effectiveness by successfully verifying 115 out of 175 rules in XLA's algebraic simplifier—far surpassing previous bounded-verification systems. The talk features work by researchers from the University of Illinois at Urbana-Champaign, University of Washington, Google, Google DeepMind, and University of California at Santa Cruz, with supplementary materials available through Zenodo that have earned "Artifacts Available" and "Artifacts Evaluated — Reusable" badges.
