前言
本文介紹一個Pytorch模型的靜态分析器 PyTea，它不需要運作代碼，即可在幾秒鐘之内掃描分析出模型中的張量形狀錯誤。文末附使用方法。
本文轉載自機器之心
編輯：CV技術指南
關注公衆号CV技術指南 ，專注于計算機視覺的技術總結、最新技術跟蹤、經典論文解讀。
張量形狀不比對是深度神經網絡機器學習過程中會出現的重要錯誤之一。由于神經網絡訓練成本較高且耗時，在執行代碼之前運作靜态分析，要比執行然後發現錯誤快上很多。
由于靜态分析是在不運作代碼的前提下進行的，是以可以幫助軟體開發人員、品質保證人員查找代碼中存在的結構性錯誤、安全漏洞等問題，進而保證軟體的整體品質。
相比于程式動态分析，靜态分析具有不實際執行程式；執行速度快、效率高等特點而廣受研究者青睐，目前，已有許多分析工具可供研究使用，如斯坦福大學開發的 Meta-Compilation（Coverity）、利物浦大學開發的 LDRA Testbed 等。
近日，來自南韓首爾大學的研究者們提出了另一種靜态分析器 PyTea，它可以自動檢測 PyTorch 項目中的張量形狀錯誤。在對包括 PyTorch 存儲庫中的項目以及 StackOverflow 中存在的張量錯誤代碼進行測試。結果表明，PyTea 可以成功的檢測到這些代碼中的張量形狀錯誤，幾秒鐘就能完成。
論文位址：https://arxiv.org/pdf/2112.09037.pdf
項目位址：https://github.com/ropas/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 等，以便讀者更好的了解執行過程。
首先是 PyTorch 程式結構，PyTorch、TensorFlow 和 Keras 等現代機器學習架構需要使用 Python API 來建構神經網絡。使用此類架構訓練神經網絡大多遵循如下四個階段的标準程式。
在 PyTorch 中，正常神經網絡訓練代碼的結構。
訓練模型需要先定義網絡結構，圖 2 為一個簡化的圖像分類代碼，取自官方的 PyTorch MNIST 分類示例：
在這裡，上述代碼首先定義一系列神經網絡層，并使它們成為單一的神經網絡子產品。為了正确組裝層，前一層的傳回張量必須滿足下一層的輸入要求。網絡使用超參數的初始化參數進行執行個體化，例如隐藏層的數量。接下來，對輸入資料集進行預處理并根據網絡的要求進行調整。從該階段開始，每個資料集都被切成較小的相同大小的塊（minibatch）。最後，主循環開始，minibatch 按順序輸入網絡。一個 epoch 是指将整個資料集傳遞到網絡的單個循環，并且 epoch 的數量通常取決于神經網絡的目的和結構。除了取決于資料集大小的主訓練循環之外，包括 epoch 數在内，訓練代碼中的疊代次數在大多數情況下被确定為常數。
在構模組化型時，網絡層之間輸入、輸出張量形狀的不對應就是張量形狀錯誤。通常形狀錯誤很難手動查找，隻能通過使用實際輸入運作程式來檢測。下圖就是典型的張量形狀錯誤（對圖 2 的簡單修改），如果不仔細檢視，你根本發現不了錯誤：
對于張量形狀錯誤（如上圖的錯誤類型），PyTea 将原始 Python 代碼翻譯成 PyTea IR 進行查找，如下圖是 PyTea IR 示例：
上面提到，PyTea 會跟蹤轉換後的 IR 的每個可能執行路徑，并收集有歇業量形狀限制。其實限制是 PyTorch 應用程式所需要的條件，以便在沒有任何張量形狀誤差的情況下執行它。例如，一個矩陣乘法運算的兩個操作數必須共享相同的維數。下圖顯示了限制的抽象文法：
限制的抽象文法部分截圖
首先，安裝環境要求：node.js >= 12.x，python >= 3.8，z3-solver >= 4.8。
安裝和使用可參考以下代碼：
編譯代碼：
相關文章閱讀：
Pytorch代碼調試工具--torchsnooper
資源分享 | SAHI：超大圖檔中對小目标檢測的切片輔助超推理庫
資源分享 | 使用 FiftyOne 加快您的論文寫作速度
歡迎關注公衆号 CV技術指南 ，專注于計算機視覺的技術總結、最新技術跟蹤、經典論文解讀。
在公衆号中回複關鍵字 “入門指南“可擷取計算機視覺入門所有必備資料。
ICCV2021 | Tokens-to-Token ViT:在ImageNet上從零訓練Vision Transformer
CVPR2021 | TrivialAugment：不用調優的SOTA資料增強政策
PyTorch和TensorFlow在模型可用性、部署便捷度和生态系統方面對比
CB Loss：基于有效樣本的類别不平衡損失
計算機視覺中的資料預處理與模型訓練技巧總結
Panoptic SegFormer：端到端的 Transformer 全景分割通用框
ICCV2021 | 簡單有效的長尾視覺識别新方案：蒸餾自監督(SSD)
AAAI2021 | 任意方向目标檢測中的動态Anchor學習
ICCV2021 | 用于視覺跟蹤的學習時空型transformer
論文的科學寫作與哲學
計算機視覺中的傳統特征提取方法總結
ICCV2021 | TOOD：任務對齊的單階段目标檢測
Pytorch 資料流中常見Trick總結
計算機視覺中的transformer模型創新思路總結
PNNX: PyTorch 神經網絡交換格式
論文創新的常見思路總結 | 卷積神經網絡壓縮方法總結
神經網絡超參數的調參方法總結 | 資料增強方法總結
Batch Size對神經網絡訓練的影響 | 計算機視覺入門路線
論文創新的常見思路總結 | 池化技術總結
歸一化方法總結 | 欠拟合與過拟合技術總結
注意力機制技術總結 | 特征金字塔技術總結
2021-視訊監控中的多目标跟蹤綜述
一文概括機器視覺常用算法以及常用開發庫
統一視角了解目标檢測算法：最新進展分析與總結
給模型加入先驗知識的常見方法總結 | 談CV領域審稿
全面了解目标檢測中的anchor | 執行個體分割綜述總結綜合整理版
HOG和SIFT圖像特征提取簡述 | OpenCV高性能計算基礎介紹
目标檢測中回歸損失函數總結 | Anchor-free目标檢測論文彙總
2021年小目标檢測最新研究綜述 | 小目标檢測常用方法總結
單階段執行個體分割綜述 | 語義分割綜述 | 多标簽分類概述
視訊目标檢測與圖像目标檢測的差別
視訊了解綜述：動作識别、時序動作定位、視訊Embedding