TensorRight: Automated Verification of Tensor Graph Rewrites
summary
TensorRight presents an automated verifier that proves tensor-graph rewrites correct for tensors of arbitrary rank and size by encoding rules in a new core language, TensorRight DSL, using an aggregated-axis abstraction, giving denotational semantics for 17 XLA operators, and an algorithm that computes a rank bound so unbounded verification reduces to a finite set of bounded cases checked by symbolic execution and an SMT solver. It expresses 121 XLA simplifier rules and verifies 115 of 175, usually in <1s (max 23s) with at most four bounded instances; artifacts and code are public.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:04Tensor computation graphs
- 2:52Example-driven rewriting
- 3:37Polymorphic rewrite rules
- 5:00Verification problem
- 6:49Need for unbounded verification
- 9:17Tensorite overview
- 11:46K-induction approach
- 13:31Aggregated axes handling
- 15:35Evaluation of Tensorite
- 17:00Conclusion
- 17:46Q&A
related talks
18mA Verified Compiler for a Functional Tensor Language
30mTensor Logic: The Language of AI
19mGuided Tensor Lifting
20mCompiling Structured Tensor Algebra
33mTeIL: a type-safe imperative Tensor Intermediate Language
20mTensor Algebra Equivalence Checker
28mOn Tensors
14mAutomated Verification of Soundness of DNN Certifiers