机器之心报道
编辑：陈萍、泽南

几秒钟扫完代码 ， 比训练一遍再找快多了 。

张量形状不匹配是深度神经网络机器学习过程中会出现的重要错误之一 。 由于神经网络训练成本较高且耗时 ， 在执行代码之前运行静态分析 ， 要比执行然后发现错误快上很多 。
由于静态分析是在不运行代码的前提下进行的 ， 因此可以帮助软件开发人员、质量保证人员查找代码中存在的结构性错误、安全漏洞等问题 ， 从而保证软件的整体质量 。
相比于程序动态分析 ， 静态分析具有不实际执行程序；执行速度快、效率高等特点而广受研究者青睐 ， 目前 ， 已有许多分析工具可供研究使用 ， 如斯坦福大学开发的 Meta-Compilation（Coverity）、利物浦大学开发的 LDRA Testbed 等 。
近日 ， 来自韩国首尔大学的研究者们提出了另一种静态分析器 PyTea ， 它可以自动检测 PyTorch 项目中的张量形状错误 。 在对包括 PyTorch 存储库中的项目以及 StackOverflow 中存在的张量错误代码进行测试 。 结果表明 ， PyTea 可以成功的检测到这些代码中的张量形状错误 ， 几秒钟就能完成 。

文章图片

• 论文地址：https://arxiv.org/pdf/2112.09037.pdf
• 项目地址：https://github.com/ropas/pytea

几秒就能查找张量形状错误的 PyTea
PyTea 工具可以静态地扫描 PyTorch 程序并检测可能的形状错误 。 PyTea 通过额外的数据处理和一些库（例如 Torchvision、NumPy、PIL）的混合使用来分析真实世界 Python/PyTorch 应用程序的完整训练和评估路径 。
PyTea 的工作原理是这样的：给定输入的 PyTorch 源 ， PyTea 静态跟踪每个可能的执行路径 ， 收集路径张量操作序列所需的张量形状约束 ， 并决定约束满足与否（因此可能发生形状错误） 。
具体来说：如下图所示 ，PyTea 首先将原始 Python 代码翻译成一种内核语言 ， 即 PyTea 内部表示（PyTea IR） 。 然后 ， 它跟踪转换后的 IR 的每个可能执行路径 ， 并收集有关张量形状的约束 ， 这些约束规定了代码在没有形状错误的情况下运行的条件 。PyTea 将收集到的约束集提供给 SMT（Satisfiability Modulo Theories）求解器 Z3 ， 以判断这些约束对于每个可能的输入形状都是可满足的 。 根据求解器的结果 ， PyTea 会得出结论 ， 哪条路径包含形状错误 。 如果 Z3 的约束求解花费太多时间 ， PyTea 会停止并发出「don’t know」提示 。

文章图片

PyTea 的整体结构 。
PyTea 由两个分析器组成 ， 在线分析器：node.js (TypeScript / JavaScript)；离线分析器：Z3 / Python 。

• 在线分析器：查找基于数值范围的形状不匹配和 API 参数的滥用 。 如果 PyTea 在分析代码时发现任何错误 ， 它将停在该位置并将错误和违反约束通知用户；
• 离线分析器：生成的约束传递给 Z3。 Z3 将求解每个路径的约束集并打印第一个违反的约束（如果存在） 。

我们先来看下结果展示 ， 在线分析器发现错误：

文章图片

离线分析器发现错误：

文章图片

为了更好的理解 PyTea 执行静态分析过程 ， 下面我们介绍一下主要的技术细节 ， 包括 PyTorch 程序结构、张量形状错误、PyTea IR 等 ， 以便读者更好的理解执行过程 。