Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDensities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere
333
0
0.0
(
0
)
Added by
Dominik Wagner
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? To formalise the problem, we consider Statistical PCF (SPCF), an extension of call-by-value PCF with real numbers, and constructs for sampling and conditioning. We give SPCF a sampling-style operational semantics a la Borgstrom et al., and study the associated weight (commonly referred to as the density) function and value function on the set of possible execution traces. Our main result is that almost-surely terminating SPCF programs, generated from a set of primitive functions (e.g. the set of analytic functions) satisfying mild closure properties, have weight and value functions that are almost-everywhere differentiable. We use a stochastic form of symbolic execution to reason about almost-everywhere differentiability. A by-product of this work is that almost-surely terminating deterministic (S)PCF programs with real parameters denote functions that are almost-everywhere differentiable. Our result is of practical interest, as almost-everywhere differentiability of the density function is required to hold for the correctness of major gradient-based inference algorithms.
rate research
Read More
Extending our own and others earlier approaches to reasoning about termination of probabilistic programs, we propose and prove a new rule for termination with probability one, also known as almost-certain termination. The rule uses both (non-strict) super martingales and guarantees of progress, together, and it seems to cover significant cases that earlier methods do not. In particular, it suffices for termination of the unbounded symmetric random walk in both one- and two dimensions: for the first, we give a proof; for the second, we use a theorem of Foster to argue that a proof exists. Non-determinism (i.e. demonic choice) is supported; but we do currently restrict to discrete distributions.
The extension of classical imperative programs with real-valued random variables and random branching gives rise to probabilistic programs. The termination problem is one of the most fundamental liveness properties for such programs. The qualitative (aka almost-sure) termination problem asks whether a given program terminates with probability 1. Ranking functions provide a sound and complete approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via ranking supermartingales (RSMs). RSMs have been extended to lexicographic RSMs to handle programs with involved control-flow structure, as well as for compositional approach. There are two key limitations of the existing RSM-based approaches: First, the lexicographic RSM-based approach requires a strong nonnegativity assumption, which need not always be satisfied. The second key limitation of the existing RSM-based algorithmic approaches is that they rely on pre-computed invariants. The main drawback of relying on pre-computed invariants is the insufficiency-inefficiency trade-off: weak invariants might be insufficient for RSMs to prove termination, while using strong invariants leads to inefficiency in computing them. Our contributions are twofold: First, we show how to relax the strong nonnegativity condition and still provide soundness guarantee for almost-sure termination. Second, we present an incremental approach where the process of computing lexicographic RSMs proceeds by iterative pruning of parts of the program that were already shown to be terminating, in cooperation with a safety prover. In particular, our technique does not rely on strong pre-computed invariants. We present experimental results to show the applicability of our approach to examples of probabilistic programs from the literature.
We study ternary sequences associated with a multidimensional continued fraction algorithm introduced by the first author. The algorithm is defined by two matrices and we show that it is measurably isomorphic to the shift on the set ${1,2}^mathbb{N}$ of directive sequences. For a given set $mathcal{C}$ of two substitutions, we show that there exists a $mathcal{C}$-adic sequence for every vector of letter frequencies or, equivalently, for every directive sequence. We show that their factor complexity is at most $2n+1$ and is $2n+1$ if and only if the letter frequencies are rationally independent if and only if the $mathcal{C}$-adic representation is primitive. It turns out that in this case, the sequences are dendric. We also prove that $mu$-almost every $mathcal{C}$-adic sequence is balanced, where $mu$ is any shift-invariant ergodic Borel probability measure on ${1,2}^mathbb{N}$ giving a positive measure to the cylinder $[12121212]$. We also prove that the second Lyapunov exponent of the matrix cocycle associated with the measure $mu$ is negative.
Let $L$ be a non-negative self-adjoint operator acting on the space $L^2(X)$, where $X$ is a metric measure space. Let ${ L}=int_0^{infty} lambda dE_{ L}({lambda})$ be the spectral resolution of ${ L}$ and $S_R({ L})f=int_0^R dE_{ L}(lambda) f$ denote the spherical partial sums in terms of the resolution of ${ L}$. In this article we give a sufficient condition on $L$ such that $$ lim_{Rrightarrow infty} S_R({ L})f(x) =f(x), {rm a.e.} $$ for any $f$ such that ${rm log } (2+L) fin L^2(X)$. These results are applicable to large classes of operators including Dirichlet operators on smooth bounded domains, the Hermite operator and Schrodinger operators with inverse square potentials.
We show that if $fcolon S_n to {0,1}$ is $epsilon$-close to linear in $L_2$ and $mathbb{E}[f] leq 1/2$ then $f$ is $O(epsilon)$-close to a union of mostly disjoint cosets, and moreover this is sharp: any such union is close to linear. This constitutes a sharp Friedgut-Kalai-Naor theorem for the symmetric group. Using similar techniques, we show that if $fcolon S_n to mathbb{R}$ is linear, $Pr[f otin {0,1}] leq epsilon$, and $Pr[f = 1] leq 1/2$, then $f$ is $O(epsilon)$-close to a union of mostly disjoint cosets, and this is also sharp; and that if $fcolon S_n to mathbb{R}$ is linear and $epsilon$-close to ${0,1}$ in $L_infty$ then $f$ is $O(epsilon)$-close in $L_infty$ to a union of disjoint cosets.
suggested questions
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
