张量完美拟合

摘要：

多维数组（NDArrays）是现代科学计算环境中的核心抽象。不幸的是，它们可能会使程序的推理变得更加困难，因为在程序执行中使用的不同数组形状的数量通常非常大，并且它们很少显式地出现在程序文本中。更糟糕的是，许多运算符对输入的形状做了隐含的假设：数组加法通常使用广播语义来丰富，而矩阵乘法假设收缩维度的长度相等。由于精确推理形状对于使用NDArrays编写正确的程序至关重要，而且由于形状通常很难通过快速浏览程序来推断，因此我们开发了Tensors Fitting Perfectly，这是一种静态分析工具，通过从程序的抽象解释中合成一组形状约束，在Swift for TensorFlow程序中推理NDArrays形状。它可以（1）检查可能的不一致性，（2）提供有关程序中出现的中间值的形状的直接见解，包括通过称为形状孔的机制。静态分析与可选的运行时断言协同工作，以提高程序作者的生产力。

英文摘要：

Multidimensional arrays (NDArrays) are a central abstraction in modern scientific computing environments. Unfortunately, they can make reasoning about programs harder as the number of different array shapes used in an execution of a program is usually very large, and they rarely appear explicitly in program text. To make things worse, many operators make implicit assumptions about the shapes of their inputs: array addition is commonly enriched with broadcasting semantics, while matrix multiplication assumes that the lengths of contracted dimensions are equal. Because precise reasoning about shapes is crucial to write correct programs using NDArrays, and because shapes are often hard to infer from a quick glance at the program, we developed Tensors Fitting Perfectly, a static analysis tool that reasons about NDArray shapes in Swift for TensorFlow programs by synthesizing a set of shape constraints from an abstract interpretation of the program. It can both (1) check for possible inconsistencies, and (2) provide direct insights about the shapes of intermediate values appearing in the program, including via a mechanism called shape holes. The static analysis works in concert with optional runtime assertions to improve the productivity of program authors.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。