PyTea: PyTorch Tensor shape error analyzer

Related tags

Deep Learningmachine-learningstatic-analysispytorch
Overview

PyTea: PyTorch Tensor Shape Error Analyzer

paper project page

Requirements

  • node.js >= 12.x
  • python >= 3.8
    • z3-solver >= 4.8

How to install and use

# install node.js
sudo apt-get install nodejs

# install python z3-solver
pip install z3-solver

# download pytea
wget https://github.com/ropas/pytea/releases/download/v0.1.0/pytea.zip
unzip pytea.zip

# run pytea
python bin/pytea.py path/to/source.py

# run example file
python bin/pytea.py packages/pytea/pytest/basics/scratch.py

How to build

# install dependencies
npm run install:all
pip install z3-solver

# build
npm run build

Documentations

Brief explanation of the analysis result

PyTea is composed of two analyzers.

  • Online analysis: node.js (TypeScript / JavaScript)
    • Find numeric range-based shape mismatch and misuse of API argument. If PyTea has found any error while analyzing the code, it will stop at that position and inform the errors and violated constraints to the user.
  • Offline analysis: Z3 / Python
    • The generated constraints are passed to Z3Py. Z3 will solve the constraint sets of each path and print the first violated constraint (if it exists).

The result of the Online analyzer is divided into three classes:

  • potential success path: the analyzer does not found shape mismatch until now, but the final constraint set can be violated if Z3 analyzes it on closer inspection.
  • potential unreachable path: the analyzer found a shape mismatch or API misuses, but there remain path constraints. In short, path constraint is an unresolved branch condition; that means the stopped path might be unreachable if remaining path constraints have a contradiction. Those cases will be distinguished from Offline analysis.
  • immediate failed path: the analyzer has found an error, stops its analysis immediately.

CAVEAT: If the code contains PyTorch or other third-party APIs that we have not implemented, it will raise false alarms. Nevertheless, we also record each unimplemented API call. See LOGS section from the result and search which unimplemented API call is performed.

The final result of the Offline analysis is divided into several cases.

  • Valid path: SMT solver has not found any error. Every constraint will always be fulfilled.
  • Invalid path: SMT solver found a condition that can violate some constraints. Notice that this does not mean the code will always crash, but it found an extreme case that crashes some executions.
  • Undecidable path: SMT solver has met unsolvable constraints, then timeouts. Some non-linear formulae can be classified into this case.
  • Unreachable path: Hard and Path constraints contain contradicting constraints; this path will not be realized from the beginning.

Result examples

  • Error found by Online analysis

test1

  • Error found by Offline analysis

test2

License

MIT License

This project is based on Pyright, also MIT License

Comments
  • LSTM/GRU input_size tensor shape errors

    LSTM/GRU input_size tensor shape errors

    Hi, I have met a problem while detecting LSTM tensor shape errors. The testing file below is runnable and pytea returns correctly.

    import torch
import torch.nn as nn
import torch.nn.functional as F


class Model(nn.Module):

    def __init__(self):
        super().__init__()
        self.cnn = nn.Conv2d(3, 1, 3, 1, 1)
        self.rnn = nn.LSTM(32, 64, 1, batch_first=True)
        self.pool = nn.MaxPool2d(2, 2)
        self.fc = nn.Linear(64, 16)

    def forward(self, x):
        x = self.pool(F.relu(self.cnn(x)))
        x = x.view(-1, 32, 32)
        x, _ = self.rnn(x)
        x = x[:, -1, :].squeeze(1)
        x = F.relu(self.fc(x))
        x = F.softmax(x, dim=-1)
        return x


if __name__ == "__main__":
    net = Model()
    x = torch.randn(2, 3, 64, 64)
    y = net(x)
    target = torch.argmax(torch.randn(2, 16), dim=-1)
    loss = F.cross_entropy(y, target.long())
    loss.backward()
    print(y.size())

    However, If I change self.rnn = nn.LSTM(32, 64, 1, batch_first=True) into self.rnn = nn.LSTM(64, 64, 1, batch_first=True), torch will report a RuntimeError: Expected 64, got 32. pytea didn't return any CONSTRAINTS information, as it supposed to.

    Then I tried to more LSTM input_size shape errors, all failed. Same situation with GRU. I think it is a bug, because I can detect Conv2d, Linear error successfully.

    opened by MCplayerFromPRC 4
  • Inconsistent with document description

    Inconsistent with document description

    Hello, I have encountered the following problems:

    First question: The content of my source file is:

       import torch
   import torch.nn as nn

  class Net(nn.Module):
      def __init__(self):
          super(Net, self).__init__()
          self.layers = nn.Sequential(
              nn.Linear(28 * 28, 120),
              nn.ReLU(),
              nn.Linear(80, 10))
  
      def a(self):
          pass

    if __name__ == "__main__":
        n = Net()

    But when I execute the command, I get the following results:

    image

    There should be a problem with defining shape in this model.

    Second question: I used it https://github.com/pytorch/examples/blob/master/mnist/main.py , but the command is stuck and no result is returned. As follows:

    image
    opened by dejavu6 2
  • Ternary expression (A if B else C) bug report

    Ternary expression (A if B else C) bug report

    아래와 같은 코드 실행에서 문제가 발생한다는 것을 깨달았습니다.

    x = 0 if 0 <= 1 else 1

    # runtime output
REDUCED HEAP: (size: 250)
  x => 1

    파이썬의 삼항연산자가 x = (((0 <= 1) and 0) or 1)로 파싱됩니다. Logical statement가 True, true-value가 0일 때 발생하는 오류인 것으로 보입니다.

    당장 벤치마크 코드에서 나타나는 문제는 아닙니다. Pylib builtin 구현에서 발생한 문제이므로, 다른 방식으로 구현함으로써 일단은 피해갈 수 있을 것 같습니다.

    감사합니다.

    opened by lego0901 1
  • Develop sehoon

    Develop sehoon

    UT-1~6 코드 분석에 필요한 torch API 구현 완료.

    UT-2: epoch을 1로 수정하지 않으면 timeout이됨. UT-3: Python 빌트인 함수 iter, next의 구현은 우선 넘어갔음. UT-6: buggy 코드에서 target이 free variable인데, 이를 처리해 주지 않고 분석을 실행하면 아무것도 출력하지 않는 버그가 있음.

    위 특이사항을 적절히 처리해주고 분석을 실행하면 1~6 모두 buggy 코드는 invalid, fix 코드는 valid 결과를 냄.

    opened by Sehun0819 0
  • path constraint check

    path constraint check

    분석중 한 패스에서 (텐서 모양 오류 등의) 에러를 만나면 해당 패스는 처리됨. 문제는 분기 조건문에 의해 실제로는 진행되지 않는 패스여도 로 처리가 되는 것.

    따라서 분석중 에러를 만났을 때 그 패스가 path constraint를 갖고 있으면 로 처리하여 z3단에 넘기게 수정하였음.

    TODO: z3단에 넘기기 전에 path constraint를 계산하여 Valid면 , Unsat이면 로 처리하기(else )

    opened by Sehun0819 0
  • Bump node-notifier from 8.0.0 to 8.0.1 in /packages/pyright-internal

    Bump node-notifier from 8.0.0 to 8.0.1 in /packages/pyright-internal

    Bumps node-notifier from 8.0.0 to 8.0.1.

    Changelog

    Sourced from node-notifier's changelog.

    v8.0.1

    • fixes possible injection issue for notify-send
    Commits

    Dependabot compatibility score

    Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

    Dependabot commands and options

    You can trigger Dependabot actions by commenting on this PR:

    • @dependabot rebase will rebase this PR
    • @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
    • @dependabot merge will merge this PR after your CI passes on it
    • @dependabot squash and merge will squash and merge this PR after your CI passes on it
    • @dependabot cancel merge will cancel a previously requested merge and block automerging
    • @dependabot reopen will reopen this PR if it is closed
    • @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
    • @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
    • @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
    • @dependabot use these labels will set the current labels as the default for future PRs for this repo and language
    • @dependabot use these reviewers will set the current reviewers as the default for future PRs for this repo and language
    • @dependabot use these assignees will set the current assignees as the default for future PRs for this repo and language
    • @dependabot use this milestone will set the current milestone as the default for future PRs for this repo and language

    You can disable automated security fix PRs for this repo from the Security Alerts page.

    dependencies 
    opened by dependabot[bot] 0
Releases(v0.1.0)
Owner
ROPAS Lab.
ROPAS Lab. @ Seoul National University
ROPAS Lab.
GitHub Repository https://sf.snu.ac.kr/pytea/
PyTorch code for training MM-DistillNet for multimodal knowledge distillation

There is More than Meets the Eye: Self-Supervised Multi-Object Detection and Tracking with Sound by Distilling Multimodal Knowledge MM-DistillNet is a

51 Dec 20, 2022
ParaGen is a PyTorch deep learning framework for parallel sequence generation

ParaGen is a PyTorch deep learning framework for parallel sequence generation. Apart from sequence generation, ParaGen also enhances various NLP tasks, including sequence-level classification, extrac

Bytedance Inc. 169 Dec 22, 2022
Automatic learning-rate scheduler

AutoLRS This is the PyTorch code implementation for the paper AutoLRS: Automatic Learning-Rate Schedule by Bayesian Optimization on the Fly published

Yuchen Jin 33 Nov 18, 2022
CNN Based Meta-Learning for Noisy Image Classification and Template Matching

CNN Based Meta-Learning for Noisy Image Classification and Template Matching Introduction This master thesis used a few-shot meta learning approach to

Kumar Manas 2 Dec 09, 2021
DirectVoxGO reconstructs a scene representation from a set of calibrated images capturing the scene.

DirectVoxGO reconstructs a scene representation from a set of calibrated images capturing the scene. We achieve NeRF-comparable novel-view synthesis quality with super-fast convergence.

sunset 709 Dec 31, 2022
Tensors and Dynamic neural networks in Python with strong GPU acceleration

PyTorch is a Python package that provides two high-level features: Tensor computation (like NumPy) with strong GPU acceleration Deep neural networks b

61.4k Jan 04, 2023
[TIP 2021] SADRNet: Self-Aligned Dual Face Regression Networks for Robust 3D Dense Face Alignment and Reconstruction

SADRNet Paper link: SADRNet: Self-Aligned Dual Face Regression Networks for Robust 3D Dense Face Alignment and Reconstruction Requirements python

Multimedia Computing Group, Nanjing University 99 Dec 30, 2022
Dual Attention Network for Scene Segmentation (CVPR2019)

Dual Attention Network for Scene Segmentation(CVPR2019) Jun Fu, Jing Liu, Haijie Tian, Yong Li, Yongjun Bao, Zhiwei Fang,and Hanqing Lu Introduction W

Jun Fu 2.2k Dec 28, 2022
Detectorch - detectron for PyTorch

Detectorch - detectron for PyTorch (Disclaimer: this is work in progress and does not feature all the functionalities of detectron. Currently only inf

Ignacio Rocco 558 Dec 23, 2022
An Inverse Kinematics library aiming performance and modularity

IKPy Demo Live demos of what IKPy can do (click on the image below to see the video): Also, a presentation of IKPy: Presentation. Features With IKPy,

Pierre Manceron 481 Jan 02, 2023
Independent and minimal implementations of some reinforcement learning algorithms using PyTorch (including PPO, A3C, A2C, ...).

PyTorch RL Minimal Implementations There are implementations of some reinforcement learning algorithms, whose characteristics are as follow: Less pack

Gemini Light 4 Dec 31, 2022
DL & CV-based indicator toolset for the vehicle drivers via live dash-cam footage.

Vehicle Indicator Toolset Deep Learning and Computer Vision based indicator toolset for vehicle drivers using live dash-cam footages. Tracking of vehi

Alex Xu 12 Dec 28, 2021
Efficient Deep Learning Systems course

Efficient Deep Learning Systems This repository contains materials for the Efficient Deep Learning Systems course taught at the Faculty of Computer Sc

Max Ryabinin 173 Dec 29, 2022
Graph-based community clustering approach to extract protein domains from a predicted aligned error matrix

Using a predicted aligned error matrix corresponding to an AlphaFold2 model , returns a series of lists of residue indices, where each list corresponds to a set of residues clustering together into a

Tristan Croll 24 Nov 23, 2022
Wide Residual Networks (WideResNets) in PyTorch

Wide Residual Networks (WideResNets) in PyTorch WideResNets for CIFAR10/100 implemented in PyTorch. This implementation requires less GPU memory than

Jason Kuen 296 Dec 27, 2022
A Multi-modal Model Chinese Spell Checker Released on ACL2021.

ReaLiSe ReaLiSe is a multi-modal Chinese spell checking model. This the office code for the paper Read, Listen, and See: Leveraging Multimodal Informa

DaDa 106 Dec 29, 2022
Code for our WACV 2022 paper "Hyper-Convolution Networks for Biomedical Image Segmentation"

Hyper-Convolution Networks for Biomedical Image Segmentation Code for our WACV 2022 paper "Hyper-Convolution Networks for Biomedical Image Segmentatio

Tianyu Ma 17 Nov 02, 2022
A NSFW content filter.

Project_Nfilter A NSFW content filter. With a motive of minimizing the spreads and leakage of NSFW contents on internet and access to others devices ,

1 Jan 20, 2022
PyTorch code of my ICDAR 2021 paper Vision Transformer for Fast and Efficient Scene Text Recognition (ViTSTR)

Vision Transformer for Fast and Efficient Scene Text Recognition (ICDAR 2021) ViTSTR is a simple single-stage model that uses a pre-trained Vision Tra

Rowel Atienza 198 Dec 27, 2022
Official code for "Maximum Likelihood Training of Score-Based Diffusion Models", NeurIPS 2021 (spotlight)

Maximum Likelihood Training of Score-Based Diffusion Models This repo contains the official implementation for the paper Maximum Likelihood Training o

Yang Song 84 Dec 12, 2022