2022/03/16 by Momoko Hattori, Naoki Kobayashi, Hattori, Momoko +3
Computer Science · Mathematics · #Advanced Neural Network Applications #Algorithm #Artificial intelligence #Artificial neural network #Computer science #Feature (linguistics) #Geometry #Inference #Machine learning #Mathematics #Parallel Computing and Optimization Techniques #Software Testing and Debugging Techniques #Tensor (intrinsic definition) #Theoretical computer science #Type (biology) #Type inference #Undecidable problem
paper · pdf · doi:10.48550/arxiv.2203.08402
openalex publication_date 2022/03/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our approach is the best-effort shape inference. As the tensor shape inference problem is undecidable in general, we allow static type/shape inference to be performed only in a best-effort manner. If the static inference cannot guarantee the absence of the shape inconsistencies, dynamic checks are inserted into the program. Another main feature is gradual typing, where 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 have implemented a prototype shape checking tool based on our approach and evaluated its effectiveness by applying it to some deep neural network programs.