We present BlueBell , a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behavior like independence and conditioning . The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behavior of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In BlueBell , we unify these styles of reasoning through the introduction of a new modality called “joint conditioning” that can encode and illuminate the rich interaction between conditional independence and relational liftings ; the two powerhouses from the two styles of reasoning.

Much of the complexity of social, biological, and engineering systems arises from the complicated interactions among the entities in the corresponding networks. A number of network analysis tools have been successfully used to discover latent structures termed communities in such networks. However, some communities with relatively weak structures can be difficult to uncover because they are obscured by other stronger connections. To cope with this situation, our previous work proposes an algorithm called HICODE to detect and amplify the dominant and hidden community structures. In this work, we conduct a comprehensive and systematic theoretical analysis on the impact of hidden community structure and the efficacy of the HICODE algorithm, as well as provide illustrations of the detection process and results. Specifically, we define a multi-layer stochastic block model and use this model to explain why the existence of hidden structure makes the detection of dominant structure harder than equivalent random noises, which can also explain why many community detection algorithms only focusing on the dominant structure do not work well as expected. We then provide theoretical analysis that the iterative reducing methods could help to enhance the discovery of hidden structure as well as the dominant structure in the multi-layer stochastic block model for the two cases of accurate and inaccurate detection. Finally, visual simulations and experimental results are presented to show the process of HICODE algorithm and the impact of different number of layers on the detection quality.

The weakest pre-expectation framework from Morgan and McIver for deductive verification of probabilistic programs generalizes binary state assertions to real-valued expectations to measure expected values of expressions over probabilistic program variables. While loop-free programs can be analyzed by mechanically transforming expectations, verifying programs with loops requires finding an invariant expectation. We view invariant expectation synthesis as a regression problem: given an input state, predict the average value of the post-expectation in the output distribution. With this perspective, we develop the first data-driven invariant synthesis method for probabilistic programs. Unlike prior work on probabilistic invariant inference, our approach learns piecewise continuous invariants without relying on template expectations. 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.

Abstract 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. 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.

Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence , a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a non-deterministic , rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.

Independence and conditional independence are fundamental concepts for reasoning about groups of random variables in probabilistic programs. Verification methods for independence are still nascent, and existing methods cannot handle conditional independence. We extend the logic of bunched implications (BI) with a non-commutative conjunction and provide a model based on Markov kernels; conditional independence can be directly captured as a logical formula in this model. Noting that Markov kernels are Kleisli arrows for the distribution monad, we then introduce a second model based on the powerset monad and show how it can capture join dependency, a non-probabilistic analogue of conditional independence from database theory. Finally, we develop a program logic for verifying conditional independence in probabilistic programs.