Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
Takashi Suwa, Atsushi Igarashi

TL;DR
This paper introduces a compile-time tensor shape checking method using staged shape-dependent types, enabling early detection of shape inconsistencies without proof burdens.
Contribution
It formalizes a staging approach for shape verification, allowing implicit shape inference and a surface language resembling dependently-typed languages.
Findings
Successfully verified tensor programs including ocaml-torch examples
Detected shape inconsistencies at compile-time as assertion failures
Achieved a practical language with static shape guarantees
Abstract
When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before actual computation. For this purpose, some languages provide dependent types such as Mat m n, and others offer refinement types to track predicates for shapes. Despite the theoretical maturity, however, such methods are often unhandy for continuous software development due to the requirement of proofs for judging type equality or subtyping; even automated proving is often unsuitable due to its unforeseeable time consumption. To remedy this, our study provides an alternative formalization by using staging. Based on the observation that conditions for the shape consistency can be extracted before running the actual tensor computations in many typical cases, we ensure such consistency by assertions evaluated as…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
