We present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and replaces measure-zero predicates and discrete branches with a vanishing smoothing, yielding closed-form expressions for posterior and path probabilities. We prove differentiability of these quantities with respect to program parameters, enabling end-to-end optimization via standard automatic differentiation, without Monte Carlo estimators. On thirteen benchmark programs, DeGAS achieves accuracy and runtime competitive with variational inference and MCMC. Importantly, it reliably tackles optimization problems where sampling-based baselines fail to converge due to conditioning involving continuous variables.

Modeling the relationships between variables through probability distributions lies at the core of probabilistic models, enabling reasoning under uncertainty. Probabilistic programming offers an effective way to represent these models by blending the simplicity of standard programming constructs with the power of automatic inference algorithms. The languages for expressing probabilistic programs are augmented with primitives representing various probability distributions to effectively capture the stochastic behavior inherent in the data. However, writing a probabilistic program is hard, because it typically requires prior knowledge about the data generation mechanism. In this work, we propose a framework for automatically synthesizing probabilistic programs directly from data, thereby learning the underlying relationships between variables and the data-generating process. We adopt an evolutionary approach, specifically grammatical evolution (GE), to extensively explore the space of probabilistic programs, aiming to discover the most likely program that describes the observed data. We experimentally evaluate our method across several benchmarks, incorporating varying levels of prior knowledge through a sketching strategy embedded into the grammar fed to GE, to demonstrate the potential of this evolutionary framework. This evaluation highlights the flexibility and effectiveness of GE in synthesizing probabilistic programs under different informational constraints.

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops , (ii) continuous distributions, and (iii) conditioning . To handle loops we rely on user-provided quantitative invariants , as is well established. However, in the realm of continuous distributions, invariant verification becomes extremely challenging due to the presence of integrals in expectation-based program semantics. Our key idea is to soundly under- or over-approximate these integrals via Riemann sums . We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove convergence of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting discrete probabilistic programs for the verification of programs involving continuous sampling . Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.

Computing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means of Gaussian mixtures. It is parametrized by a map that associates each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that matches up to second-order moments analytically in face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation (SOGA) on a number of case studies from the literature. We show that it can provide accurate estimates in models not supported by other approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals. On two notable classes of problems, namely collaborative filtering and programs involving mixtures of continuous and discrete distributions, we show that SOGA significantly outperforms alternative techniques in terms of accuracy and computational time.