  Morgan and McIver's weakest pre-expectation framework is one of the most
well-established methods for deductive verification of probabilistic programs.
Roughly, the idea is to generalize binary state assertions to real-valued
expectations, which can measure expected values of probabilistic program
quantities. While loop-free programs can be analyzed by mechanically
transforming expectations, verifying loops usually requires finding an
invariant expectation, a difficult task. We propose a new view of invariant
expectation synthesis as a regression problem: given an input state, predict
the average value of the post-expectation in the output distribution. Guided by
this perspective, we develop the first data-driven invariant synthesis method
for probabilistic programs. Unlike prior work on probabilistic invariant
inference, our approach can learn piecewise continuous invariants without
relying on template expectations, and also works with black-box access to the
program. We also develop a data-driven approach to learn sub-invariants from
data, which can be used to upper- or lower-bound expected values. We implement
our approaches and demonstrate their effectiveness on a variety of benchmarks
from the probabilistic programming literature.
