逐步张量形状检查
Gradual Tensor Shape Checking
摘要：
张量形状不匹配是深度学习程序中常见的错误来源。我们提出了一种新的基于类型的方法来检测张量形状不匹配。我们的方法的主要特点之一是尽最大努力的形状推理。由于张量形状推理问题一般是不可判定的，我们允许静态类型/形状推理只能以尽力而为的方式进行。如果静态推断不能保证不存在形状不一致，则将动态检查插入到程序中。另一个主要特性是渐进类型，用户可以通过向程序添加适当的类型注释来提高推理的精度。我们形式化了我们的方法，并证明它满足Siek等人在2015年提出的渐进分型标准。我们已经实现了一个原型形状检查工具，我们的方法的基础上，并评估其有效性，将其应用到一些深神经网络程序。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
