Newtonian Program Analysis of Probabilistic Programs

TL;DR

This work tackles the challenge of scalable, interprocedural analysis of probabilistic programs with unstructured control-flow, nondeterminism, and recursion. It introduces NPA-PMA, a Newtonian program analysis framework built on ω-continuous pre-Markov algebras and regular infinite-tree expressions, enabling largely non-iterative solving of interprocedural equations through carefully differentiated linearizations. The authors present comprehensive theory (ωPMAs, regular-infinite-tree representations, and differentiation), a pipeline for solving interprocedural systems, and four practical case studies (Bayesian inference, linear and nonlinear expectation invariants, and higher-moment analyses) with prototype implementations. Empirical results show significant speedups over Kleene iteration and competitive performance against specialized tools, while demonstrating the framework's generality and flexibility for designing probabilistic program analyses.

Abstract

Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on iterative approximation. This article presents an interprocedural dataflow-analysis framework, called NPA-PMA, for designing and implementing (partially) non-iterative program analyses of probabilistic programs with unstructured control-flow, nondeterminism, and general recursion. NPA-PMA is based on Newtonian Program Analysis (NPA), a generalization of Newton's method to solve equation systems over semirings. The key challenge for developing NPA-PMA is to handle multiple kinds of confluences in both the algebraic structures that specify analyses and the equation systems that encode control flow: semirings support a single confluence operation, whereas NPA-PMA involves three confluence operations (conditional, probabilistic, and nondeterministic). Our work introduces $ω$-continuous pre-Markov algebras ($ω$PMAs) to factor out common parts of different analyses; adopts regular infinite-tree expressions to encode program-execution paths in control-flow hyper-graphs; and presents a linearization method that makes Newton's method applicable to the setting of regular-infinite-tree equations over $ω$PMAs. NPA-PMA allows analyses to supply a non-iterative strategy to solve linearized equations. Our experimental evaluation demonstrates that (i) NPA-PMA holds considerable promise for outperforming Kleene iteration, and (ii) provides great generality for designing program analyses.

Figures (16)

• Figure 1: A roadmap for the Overview section (\ref{['Se:Overview']}). We use dashed curves for concepts from prior work and red double borders for contributions of this work. For each variant of Newton's method for solving $\vec{X} = \vec{f}(\vec{X})$, we use $\Diamond$ for the algebraic structure of the elements, $\ocircle$ for the form of the right-hand sides $\vec{f}(\vec{X})$, and $\Square$ for the supported kind of programs. We put a $\pentagon$ (for a program representation) on top of a $\ocircle$ (for a form of right-hand sides) to denote that there is a sound transformation from $\pentagon$ to $\ocircle$.
• Figure 2: The running example of NPA.
• Figure 3: Examples to demonstrate the gap.
• Figure 4: A nondeterministic recursive program.
• Figure 5: $\delta \oplus \mathcal{D} f|_\nu(Y)$ as a tree.

Theorems & Definitions (34)

• definition 1: ICALP:EKL08JACM:EKL10
• Remark 1
• Remark 2
• Remark 3
• definition 2
• lemma 1
• definition 3
• theorem 4
• definition 4
• lemma 2