Recently, probabilistic Satisfiability Modulo Theories has emerged as a very expressive formalism for modeling complex distributions over continuous and discrete variables. By encoding the probability density function over an SMT formula with piecewise polynomials, any joint probability distribution can be represented with arbitrary precision, granting unprecedented flexibility and enabling probabilistic reasoning with both algebraic and logical constraints. In this talk, I will introduce the core concepts, challenges and applications of probabilistic SMT in the fields of machine learning and quantitative formal verification.
