stan: Systemic bug in Stan sampler

Summary:

Systemic bug in Stan inference engine

Description:

As demonstrated in C-K Hur, A. V. Nori, S. K. Rajamani, and S. Samuel, “A Provably Correct Sampler for Probabilistic Programs” (alternate link) Stan does not seem to converge to the correct distribution for the following model:

1: double x, y;
2: x ~ Gaussian(0, 1);
3: if (x > 0) then
4:    y ~ Gaussian(10, 2);
5: else
6:    y ~ Gamma(3, 3);
7: return y;

Reproducible Steps:

See ipython notebook 1 which demonstrates the steps to reproduce the behaviour with the following stan model:

"""
parameters {
    real x;
    real y;
}
model {
    x ~ normal(0, 1);
    if(x > 0) {
        y ~ normal(10, 2);
    } else {
        y ~ gamma(3, 3);
    }
}
"""

Current Output:

See Example 1 in ipython notebook 2. Also refer to that notebook for an alternate formulation which stan infers correctly.

Expected Output:

See the graphs in ipython notebook 2 and ipython notebook 1

Additional Information:

As mentioned in the description, we believe this points to a systemic flaw in Stan’s sampler. The paper provides the general solution as well as examples of other problematic models.

Current Version:

v2.9.0