Gradual Tensor Shape Checking
share
Tensor shape mismatch is a common source of bugs in deep learning programs. Most of the studies conducted to solve this problem use the whole-program analysis approach, which lacks compositionality. A type-based approach is desirable in this respect, but since the problem of shape inference is undecidable in general, fully automated shape inference is bound to be either unsound or too conservative. We propose a type-based approach to detect tensor shape mismatches that works practically under such limitations. One of the main features of our approach is the best-effort shape inference. Because of the undecidability of shape inference, our procedure performs it only in a best-effort manner. The inference result may be too imprecise to statically guarantee the absence of the shape inconsistencies, and in such cases, dynamic checks are inserted into the program. Another main feature is gradual typing. Users can improve the precision of the inference by adding appropriate type annotations to the program. We formalize our approach and prove that it satisfies the criteria of gradual typing proposed by Siek et al. in 2015. We implement a prototype shape checking tool based on our approach and evaluate its effectiveness by applying it to some deep neural network programs.
READ FULL TEXT