The static analyser implemented in pyppai/ performs the following tasks:
- Verify the support correspondence for a given Pyro model-guide pair.
- Verify the absence of dimension-related errors from PyTorch's tensors and Pyro's plates.
To evaluate the static analyser, we applied it to the Pyro examples and Pyro test suite in tests/.
You can reproduce this experiment by running make batch-suite and make batch-examples.
Refer to README.txt for the details of our implementation and experiments.
Towards Verified Stochastic Variational Inference for Probabilistic Programs
Wonyeol Lee, Hangyeol Yu, Xavier Rival, Hongseok Yang
POPL 2020
