Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

A probabilistic program with while loops and user-labelled sample statements has a density that factors into finitely many statically computable pieces — one per sample statement.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Even probabilistic programs with while loops and dynamic sample labels factor into one density term per labelled sample statement, and this static factorization accelerates three Bayesian inference algorithms.

T0 review reviewed 2026-08-05 challenge →

load-bearing objection Main factorisation theorem is a genuine advance and likely sound; the optimisation corollaries are conditional on an unverified address-uniqueness assumption that should be fixed or clearly scoped before publication. the 3 major comments →

arxiv 2508.20922 v2 pith:JAVSRWGR submitted 2025-08-28 cs.PL

Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops

Markus B\"ock , J\"urgen Cito This is my paper
classification cs.PL
keywords probabilistic programmingstatic factorisationcontrol-flow graphsprovenance analysisprogram slicingMetropolis Hastingsvariational inferencesequential Monte Carlo
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper answers an open question in probabilistic programming: to what extent can a program with while loops and user-labelled sample statements — features that let a single program define an unbounded number of random variables — be represented graphically? The authors prove that the density of any such program factorises into exactly K factors, one per sample statement, where each factor depends only on address sets computed statically from the program's control-flow graph. For loop-free programs with constant labels the factorisation recovers the familiar Bayesian network form; for loops and dynamic labels it is new, and the resulting graphical object is a Markov network that may contain cycles and infinitely many nodes. The authors further prove that slicing the program along this factor structure is sound, giving provably correct speed-ups for three standard inference algorithms: single-site Metropolis Hastings, black-box variational inference, and sequential Monte Carlo. On 16 benchmark programs the sliced versions match or beat existing methods, with the largest gains on mixture and topic models whose latent variables only affect independent data variables.

Core claim

The central claim, Theorem 2: for any program in the paper's language — while loops and sample statements with runtime-evaluated string addresses included — the trace density factorises into a product of K functions, one per labelled sample node. Each factor depends only on addresses a static analysis computes at compile time: the sample's own address set, the addresses feeding its distribution arguments, and the addresses of branch conditions deciding whether the node runs. The factorisation is finite even when execution touches infinitely many addresses. The companion claim is soundness of slicing: a sub-program per factor reproduces exactly the log-density differences inference needs, whi

What carries the argument

The load-bearing construction is the static provenance analysis prov(N, x) running on a control-flow graph whose while loops are first unrolled into an infinite directed acyclic graph. It uses standard reaching-definitions and branch-parent reasoning to compute the set of trace addresses that can influence variable x at node N; for loops, the finite CFG version over-approximates the unrolled one. Each factor p_k is built from the address set A_k = addresses(N_k) plus the provenance of the sample's expressions plus the provenance of its branch-parent conditions, with an indicator b_k that is 1 exactly when that sample node executes on the trace. The same analysis, read backwards, generates th

Load-bearing premise

The optimisation half of the paper rests on uniqueness of addresses on a trace: for every trace, at most one executed sample statement may evaluate to a given address. If a while loop resamples the same address, or two sample statements produce the same dynamic label on one run, the sliced-program equalities behind the Metropolis Hastings and variational-inference speed-ups are not guaranteed. The K-factor factorisation theorem itself does not need this condition.

What would settle it

Run a two-statement program in which a while loop resamples the same fixed address twice on one trace, apply the paper's sliced single-site Metropolis Hastings to it, and compare the acceptance ratio computed from the sliced sub-program against the ratio from the full density p_G. Any mismatch would demonstrate that Corollary 2 fails beyond the single-address assumption. As a lighter check of Corollary 1, compute Δ_α(tr) = log p_G(tr) − log p_α(tr) for two different addresses α in a loop that shares labels and verify whether it is actually independent of α.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Loop-free programs with constant unique labels reduce to the standard Bayesian network factorisation, so the theorem subsumes the known equivalence for that class.
  • Dynamic labels and while loops push the graphical representation to Markov networks with possibly cyclic dependencies and infinitely many nodes; the paper's hurricane example shows a dependency cycle arising from nine sample statements.
  • Single-site Metropolis Hastings can compute acceptance ratios by summing only the factors whose address sets contain the resampled address; on the benchmark models this shortens per-iteration runtime by up to an order of magnitude.
  • Black-box variational inference gains the variance reduction of a Markov-blanket estimator without dynamic tracing: gradient variance drops by orders of magnitude on models with data dependencies and control flow.
  • Sequential Monte Carlo can be run iteratively by chaining the per-factor sub-programs, updating particle weights between consecutive sample statements rather than recomputing from scratch; the paper measures 3-10x speed-ups.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The single-address uniqueness assumption is a real boundary on the optimisations: while loops that deliberately resample one fixed address (a common pattern for latent-variable updates) fall outside the correctness guarantee of Corollaries 1-3, even though Theorem 2 itself still holds. Splitting addresses by loop iteration in the provenance analysis is a natural testable extension that might resto
  • The deltas Δ_α that Corollary 1 isolates are effectively a static approximation of each variable's Markov blanket; comparing their quality against dynamic blanket tracking on re-entrant or nested-loop programs would be a direct empirical next step.
  • The proof device of unrolling loops into an infinite DAG suggests a route to recursive programs: recursive calls could be handled as dynamically unrolled graphs with finite call-site signatures, extending the same K-factor statement beyond while loops.
  • The over-approximation cost is visible in the paper's HMM experiments, where loop-carried dependencies are declared for all future iterations; a loop-iteration-sensitive refinement of the provenance analysis would be a concrete improvement direction, and the paper's own unrolling result shows the gain available.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a static factorisation of the density of probabilistic programs with user-labelled sample statements and while loops. It extends address-based operational semantics, translates programs to CFGs (and unrolled CFGs for loops), and develops a static provenance analysis. The central result, Theorem 2, states that for a program with K sample statements, the density factorises into K factors, each depending only on the provenance of one sample node, even for programs with unbounded loops and dynamic addresses. The paper then derives a slicing transformation from this factorisation and uses it to optimise three inference algorithms: single-site Metropolis Hastings (LMH), black-box variational inference (BBVI), and sequential Monte Carlo (SMC). The contributions are supported by paper-and-pencil proofs in appendices, an open-source implementation, and empirical evaluation on 16 benchmarks with comparisons to Gen combinators, C3/WebPPL, and Pyro.

Significance. If the main theorem is correct, it is a substantial advance: it gives a finite static factorisation for a universal PPL class whose density is otherwise defined only operationally over traces. The unrolled-CFG construction and the well-founded induction in Proposition 4 provide a plausible route to this result, and the authors are careful to separate the over-approximation of the static analysis from the exact factorisation. The paper also ships reproducible code and reports detailed comparisons against established systems, which strengthens the empirical half. However, the applied claims in Sections 5.2--5.3 are narrower than stated: Corollaries 1--3 all rely on an address-uniqueness condition that is not guaranteed by the semantics and is not statically checked. The central factorisation theorem itself does not need this condition, but the LMH and BBVI speed-ups do. Because this condition is load-bearing for the paper's practical contribution and is left unverified, the paper requires revision before the optimisation claims can be accepted as stated.

major comments (3)
  1. [§5.1, Corollary 1; §5.2, Corollary 2; §5.3, Corollary 3] The address-uniqueness assumption is load-bearing and unverified. Corollary 1 assumes 'for each trace tr there is at most one sample node M_alpha in its execution sequences such that the address expression of M_alpha evaluates to alpha'. This condition is not implied by the language semantics: a loop whose body contains `x = sample("x", Bernoulli(0.5))` resamples the same address in every iteration, and two sequential sample statements with the same constant label also violate it. Under such violations, Lemma 6 (Appendix D.1) fails in Case 3: a later sample node also reading alpha contributes to the density difference, so the equality in Theorem 3, log p_G(tr1) - log p_G(tr2) = log p_Gk(tr1,sigma) - log p_Gk(tr2,sigma), does not hold. Consequently the LMH acceptance-ratio computation (Corollary 2) and the BBVI variance-reduction identity (Corollary 3) are not proven correct for programs
  2. [§5.3, Corollary 3; Appendix D.5] The correctness of the BBVI estimator is conditional on measure-theoretic assumptions that are only sketched. Corollary 3 says 'Under measurability assumptions given in Appendix D.5', but Appendix D.5 defines a sigma-algebra on traces and assumes that the set Tminimal is measurable without proving it for the programs considered. The proof also interchanges a sum over all finite address subsets with an integral; this is justified heuristically by minimality, but not rigorously. This is a load-bearing gap for the BBVI claim, because the variance-reduction identity is an equality of expectations. The authors explicitly state that a full measure-theoretic treatment is beyond scope, which is acceptable, but the theorem should be presented as conditional on these assumptions rather than as a fully established result.
  3. [§4.2, Theorem 2 proof] The proof groups sample nodes in the unrolled CFG by their image under iota_cfg and defines p_k as an infinite product over j with iota_cfg(M_j)=N_k. For a terminating trace only finitely many factors differ from 1, so the product is pointwise well-defined, but this should be stated explicitly. Without it, the reader cannot immediately see why the infinite product is finite for the traces for which p_S is defined. This is a minor technical point in an otherwise sound argument.
minor comments (5)
  1. [§3.2, Algorithm 1] The global marking of pairs (N',y) in Algorithm 1 is not explicitly reset per top-level invocation. As written, a second call to prov(N,x) could skip work due to marks left by a previous call. This is a presentation issue; adding 'fresh marking for each call' would clarify.
  2. [§5.2, Corollary 2] The text says 'the first and only sample node whose address expression evaluates to alpha'. Since the assumption already guarantees at most one such node, 'first' is redundant and slightly confusing. Consider rewording to 'the (unique) sample node'.
  3. [§2, Listing 2 discussion] The sentence 'most formal PPLs ... cannot interpret a program with three sample statements as a four-dimensional joint density' is slightly imprecise: the program has three sample statements but the density ranges over four addresses because one of the two branch addresses is never sampled. This is understandable from context but could be clarified.
  4. [§5.2.1, Table 1] The 'Fixed-Finite' baseline is described only as representative of PPLs with explicit graphical models; the exact factorisation used and how it is derived from the program is not described. Since this baseline is used to claim that the static approach approaches hand-written factorisations, a few more details would help.
  5. [Throughout] Several typos: 'probabilisitic' in Listing 5, 'This work is to first' in Section 7, 'proof correctness' in Section 5.2, and an unbalanced parenthesis in Definition 9 of Appendix D.1. Minor editorial fixes.

Circularity Check

0 steps flagged

No significant circularity: the factorisation theorem is derived self-containedly from the operational semantics and CFG construction; the optimization corollaries rest on an explicit uniqueness assumption that is a scope limitation, not a circular step.

full rationale

The paper's central contribution, Theorem 2, is a direct proof from the operational semantics of the language and the unrolled CFG construction. The factors p_k are constructed in the proof of Theorem 1 (and extended in Theorem 2) by grouping the per-sample density contributions of the unrolled CFG; the non-trivial content is the provenance soundness statements (Propositions 2 and 4, Lemma 3), which are proven by structural/well-founded induction and do not assume the factorisation. No parameter is fitted to data, and no external result is imported as a load-bearing premise: the cited Bayesian-network equivalence is presented as a special case of Theorem 1, not used to prove it. Self-citations (to the authors' earlier static-analysis framework [7] and replication package [10]) are contextual and do not carry the theorem. The applied half (Corollaries 1–3) does rely on an explicit address-uniqueness assumption, and the paper states this assumption before each corollary; this is an acknowledged limitation of the optimisation guarantees, not a reduction of the conclusion to the premises. No step in the derivation chain equates the output to an input by construction, renames a known result as new, or imports a uniqueness claim from the authors' prior work. The main theoretical result is self-contained and the circularity score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

The central theorem is a derivation from the stated operational semantics and CFG construction; it introduces no fitted constants. The main assumptions are the trace/soft-constraint model, total pdfs, termination for defined densities, and, for the optimization results, an address-uniqueness condition plus measure-theoretic regularity for BBVI.

axioms (6)
  • domain assumption Trace semantics with soft constraints: each sample statement reads its value from the trace and multiplies a total pdf into the reserved density variable p; conditioning is only by fixing trace values.
    Definition 1 and Theorem 2 use this density-on-traces model; the paper does not define a fully normalised posterior (Section 2.3).
  • domain assumption Address expressions evaluate to strings, and pdf_f are total functions into R>=0.
    Used in the sample-statement rule (1) and in defining p_k in Eq. (5).
  • domain assumption Programs are considered only on traces for which the density is defined, i.e. terminating executions; non-termination gives undefined density.
    The factorisation equality in Theorems 1 and 2 is conditional on p_S(tr) not being undefined.
  • standard math The unrolled CFG admits well-founded induction because it has no infinite descending chains.
    Proposition 4 and Theorem 2 rely on this to define evaluation functions over a countable DAG.
  • ad hoc to paper For the optimisation results, at most one sample node in an execution can evaluate a given address alpha.
    Assumption stated before Corollary 1; it restricts the class of programs for LMH/BBVI and is not needed for the factorisation theorem.
  • domain assumption For BBVI, measurability of T_minimal and differentiability of q_alpha with respect to phi_alpha are assumed.
    Explicitly stated in Corollary 3 and Appendix D.5; the paper does not prove these regularity conditions.

reviewed 2026-08-05 · how reviews work

0 comments
Cite this review

Pith. "Pith review of Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops." pith.science (2026). https://pith.science/paper/JAVSRWGR

@misc{pith2026250820922,
  author       = {Pith},
  title        = {Pith review of: Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JAVSRWGR}},
  note         = {Machine review of arXiv:2508.20922}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

It is commonly known that any Bayesian network can be implemented as a probabilistic program, but the reverse direction is not so clear. In this work, we address the open question to what extent a probabilistic program with user-labelled sample statements and while loops - features found in languages like Gen, Turing, and Pyro - can be represented graphically. To this end, we extend existing operational semantics to support these language features. By translating a program to its control-flow graph, we define a sound static analysis that approximates the dependency structure of the random variables in the program. As a result, we obtain a static factorisation of the implicitly defined program density, which is equivalent to the known Bayesian network factorisation for programs without loops and constant labels, but constitutes a novel graphical representation for programs that define an unbounded number of random variables via loops or dynamic labels. We further develop a sound program slicing technique to leverage this structure to statically enable three well-known optimisations for the considered program class: we reduce the variance of gradient estimates in variational inference and we speed up both single-site Metropolis Hastings and sequential Monte Carlo. These optimisations are proven correct and empirically shown to match or outperform existing techniques.

Figures

Figures reproduced from arXiv: 2508.20922 by J\"urgen Cito, Markus B\"ock.

Figure 1
Figure 1. Figure 1: Reaching definitions, branch parents, and the provenance set for a simple example. The evaluation [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: CFG and unrolled CFG for program (x = 10; while (x < 10) do (x = x - 1)) and their connection via the map 𝜄cfg shown with red edges. The following lemma states that we can over-approximate the provenance set for variable 𝑥 at node 𝑀 in the unrolled CFG 𝐻 by applying Algorithm 1 to the corresponding node 𝜄cfg (𝑀) in 𝐺. Lemma 3. Let 𝐺 be the CFG and 𝐻 the unrolled CFG of program 𝑆. For each node 𝑀 ∈ 𝐻 follow… view at source ↗
Figure 3
Figure 3. Figure 3: Example Julia sub-programs generated from the static factorisation (with short-hands [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Incremental Computation for Efficient Programmable Inference in Probabilistic Programs

    cs.PL 2026-06 unverdicted novelty 7.0

    Develops compositional incrementalization of density functions for probabilistic programs to accelerate Monte Carlo inference algorithms.

Reference graph

Works this paper leans on

65 extracted references · 60 canonical work pages · cited by 1 Pith paper · 1 internal anchor

  1. [1]

    George K Baah, Andy Podgurski, and Mary Jean Harrold. 2008. The probabilistic program dependence graph and its application to fault diagnosis. In Proceedings of the 2008 international symposium on Software testing and analysis . 189–200

    work page 2008

  2. [2]

    Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020. Foundations of probabilistic programming. Cambridge University Press

    work page 2020

  3. [3]

    Ryan Bernstein. 2019. Static analysis for probabilistic programs. arXiv preprint arXiv:1909.05076 (2019)

    work page internal anchor Pith review Pith/arXiv arXiv 2019

  4. [4]

    Ryan Bernstein. 2023. Abstractions for Probabilistic Programming to Support Model Development . Ph. D. Dissertation. Columbia University

    work page 2023

  5. [5]

    Ryan Bernstein, Matthijs Vákár, and Jeannette Wing. 2020. Transforming probabilistic programs for model checking. In Proceedings of the 2020 ACM-IMS on Foundations of Data Science Conference . 149–159

    work page 2020

  6. [6]

    Eli Bingham, Jonathan P Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul Szerlip, Paul Horsfall, and Noah D Goodman. 2019. Pyro: Deep universal probabilistic programming. The Journal of Machine Learning Research 20, 1 (2019), 973–978

    work page 2019

  7. [7]

    Markus Böck, Michael Schröder, and Jürgen Cito. 2024. Language-Agnostic Static Analysis of Probabilistic Programs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering . 78–90

    work page 2024

  8. [8]

    Johannes Borgström, Ugo Dal Lago, Andrew D Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. ACM SIGPLAN Notices 51, 9 (2016), 33–46

    work page 2016

  9. [9]

    Johannes Borgström, Andrew D Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. 2011. Mea- sure transformer semantics for Bayesian machine learning. In Programming Languages and Systems: 20th European Symposium on Programming, ESOP 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings 20. Springer, 77–96

    work page 2011

  10. [10]

    Markus Böck. 2025. Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops . https://doi.org/10.5281/zenodo.16900539

    work page doi:10.5281/zenodo.16900539 2025

  11. [11]

    Simon Castellan and Hugo Paquet. 2019. Probabilistic programming inference via intensional semantics. InProgramming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings 28. Springer, 322–349

    work page 2019

  12. [12]

    Yutian Chen, Vikash Mansinghka, and Zoubin Ghahramani. 2014. Sublinear approximate inference for probabilistic programs. stat 1050 (2014), 6

    work page 2014

  13. [13]

    Nicolas Chopin, Omiros Papaspiliopoulos, et al. 2020. An introduction to sequential Monte Carlo . Vol. 4. Springer

    work page 2020

  14. [14]

    Keith D Cooper and Linda Torczon. 2011. Engineering a compiler. Elsevier

    work page 2011

  15. [15]

    Marco Cusumano-Towner, Alexander K Lew, and Vikash K Mansinghka. 2020. Automating involutive MCMC using probabilistic and differentiable programming. arXiv preprint arXiv:2007.09871 (2020)

    Pith/arXiv arXiv 2020

  16. [16]

    Marco Francis Cusumano-Towner. 2020. Gen: a high-level programming platform for probabilistic inference . Ph. D. Dissertation. Massachusetts Institute of Technology

    work page 2020

  17. [17]

    Marco F Cusumano-Towner, Feras A Saad, Alexander K Lew, and Vikash K Mansinghka. 2019. Gen: a general-purpose probabilistic programming system with programmable inference. In Proceedings of the 40th acm sigplan conference on programming language design and implementation . 221–236

    work page 2019

  18. [18]

    Fredrik Dahlqvist and Dexter Kozen. 2019. Semantics of higher-order probabilistic programs with conditioning. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–29

    work page 2019

  19. [19]

    Claudia Faggian, Daniele Pautasso, and Gabriele Vanoni. 2024. Higher Order Bayesian Networks, Exactly. Proceedings of the ACM on Programming Languages 8, POPL (2024), 2514–2546

    work page 2024

  20. [20]

    Hong Ge, Kai Xu, and Zoubin Ghahramani. 2018. Turing: a language for flexible probabilistic inference. InInternational conference on artificial intelligence and statistics . PMLR, 1682–1690

    work page 2018

  21. [21]

    Noah Goodman, Vikash Mansinghka, Daniel M Roy, Keith Bonawitz, and Joshua B Tenenbaum. 2012. Church: a language for generative models. arXiv preprint arXiv:1206.3255 (2012). , Vol. 1, No. 1, Article . Publication date: September 2025. Static Factorisation of Probabilistic Programs 27

    Pith/arXiv arXiv 2012

  22. [22]

    Noah D Goodman and Andreas Stuhlmüller. 2014. The Design and Implementation of Probabilistic Programming Languages. http://dippl.org. Accessed: 2025-3-20

    work page 2014

  23. [23]

    Andrew D Gordon, Thomas A Henzinger, Aditya V Nori, and Sriram K Rajamani. 2014. Probabilistic programming. In Future of software engineering proceedings . 167–181

    work page 2014

  24. [24]

    Maria I Gorinova, Andrew D Gordon, and Charles Sutton. 2019. Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–30

    work page 2019

  25. [25]

    Maria I Gorinova, Andrew D Gordon, Charles Sutton, and Matthijs Vákár. 2021. Conditional independence by typing. ACM Transactions on Programming Languages and Systems (TOPLAS) 44, 1 (2021), 1–54

    work page 2021

  26. [26]

    John L Hennessy and David A Patterson. 2011. Computer architecture: a quantitative approach . Elsevier

    work page 2011

  27. [27]

    Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . IEEE, 1–12

    work page 2017

  28. [28]

    Steven Holtzen, Guy Van den Broeck, and Todd Millstein. 2020. Scaling exact inference for discrete probabilistic programs. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–31

    work page 2020

  29. [29]

    Chung-Kil Hur, Aditya V Nori, Sriram K Rajamani, and Selva Samuel. 2014. Slicing probabilistic programs. ACM SIGPLAN Notices 49, 6 (2014), 133–144

    work page 2014

  30. [30]

    Chung-Kil Hur, Aditya V Nori, Sriram K Rajamani, and Selva Samuel. 2015. A provably correct sampler for probabilistic programs. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik

    work page 2015

  31. [31]

    Daphne Koller and Nir Friedman. 2009. Probabilistic graphical models: principles and techniques . MIT press

    work page 2009

  32. [32]

    Dexter Kozen. 1979. Semantics of probabilistic programs. In 20th Annual Symposium on Foundations of Computer Science (sfcs 1979). IEEE, 101–114

    work page 1979

  33. [33]

    Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2019. Towards verified stochastic variational inference for probabilistic programs. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–33

    work page 2019

  34. [34]

    Alexander K Lew, Marco F Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K Mansinghka. 2019. Trace types and denotational semantics for sound programmable inference in probabilistic languages. Proceedings of the ACM on Programming Languages 4, POPL (2019), 1–32

    work page 2019

  35. [35]

    Alexander K Lew, Matin Ghavamizadeh, Martin C Rinard, and Vikash K Mansinghka. 2023. Probabilistic Programming with Stochastic Probabilities. Proceedings of the ACM on Programming Languages 7, PLDI (2023), 1708–1732

    work page 2023

  36. [36]

    Daniel Lundén, Johannes Borgström, and David Broman. 2021. Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages.. In ESOP. 404–431

    work page 2021

  37. [37]

    David J Lunn, Andrew Thomas, Nicky Best, and David Spiegelhalter. 2000. WinBUGS-a Bayesian modelling framework: concepts, structure, and extensibility. Statistics and computing 10 (2000), 325–337

    work page 2000

  38. [38]

    Carol Mak, C-H Luke Ong, Hugo Paquet, and Dominik Wagner. 2021. Densities of almost surely terminating probabilistic programs are differentiable almost everywhere. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings 30 . Springer International Publishing, 432–461

    work page 2021

  39. [39]

    Vikash K Mansinghka, Ulrich Schaechtle, Shivam Handa, Alexey Radul, Yutian Chen, and Martin Rinard. 2018. Probabilistic programming with programmable inference. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation . 603–616

    work page 2018

  40. [40]

    Andrew McCallum, Karl Schultz, and Sameer Singh. 2009. Factorie: Probabilistic programming via imperatively defined factor graphs. Advances in Neural Information Processing Systems 22 (2009)

    work page 2009

  41. [41]

    Brian Milch, Bhaskara Marthi, Stuart Russell, David Sontag, Daniel L Ong, and Andrey Kolobov. 2007. BLOG: Probabilistic models with unknown objects. (2007)

    work page 2007

  42. [42]

    Brian Milch, Bhaskara Marthi, David Sontag, Stuart Russell, Daniel L Ong, and Andrey Kolobov. 2005. Approximate inference for infinite contingent Bayesian networks. In International Workshop on Artificial Intelligence and Statistics . PMLR, 238–245

    work page 2005

  43. [43]

    Tom Minka. 2012. Infer. NET 2.5. http://research. microsoft. com/infernet (2012)

    work page 2012

  44. [44]

    Lawrence M Murray and Thomas B Schön. 2018. Automated learning with a probabilistic programming language: Birch. Annual Reviews in Control 46 (2018), 29–43

    work page 2018

  45. [45]

    John Paisley, David Blei, and Michael Jordan. 2012. Variational Bayesian inference with stochastic search. arXiv preprint arXiv:1206.6430 (2012)

    Pith/arXiv arXiv 2012

  46. [46]

    Hugo Paquet. 2021. Bayesian strategies: probabilistic programs as generalised graphical models. In Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27–April 1, 2021, Proceedings 30 . Springer International Publishing, 519–547

    work page 2021

  47. [47]

    Rajesh Ranganath, Sean Gerrish, and David Blei. 2014. Black box variational inference. In Artificial intelligence and statistics. PMLR, 814–822. , Vol. 1, No. 1, Article . Publication date: September 2025. 28 Markus Böck and Jürgen Cito

    work page 2014

  48. [48]

    Daniel Ritchie, Andreas Stuhlmüller, and Noah Goodman. 2016. C3: Lightweight incrementalized MCMC for proba- bilistic programs using continuations and callsite caching. In Artificial Intelligence and Statistics. PMLR, 28–37

    work page 2016

  49. [49]

    Geoffrey Roeder, Yuhuai Wu, and David K Duvenaud. 2017. Sticking the landing: Simple, lower-variance gradient estimators for variational inference. Advances in Neural Information Processing Systems 30 (2017)

    work page 2017

  50. [50]

    Feras A Saad, Martin C Rinard, and Vikash K Mansinghka. 2021. SPPL: probabilistic programming with fast exact symbolic inference. In Proceedings of the 42nd acm sigplan international conference on programming language design and implementation. 804–819

    work page 2021

  51. [51]

    John Salvatier, Thomas V Wiecki, and Christopher Fonnesbeck. 2016. Probabilistic programming in Python using PyMC3. PeerJ Computer Science 2 (2016), e55

    work page 2016

  52. [52]

    Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S McKinley, Dan Grossman, and Luis Ceze. 2014. Expressing and verifying probabilistic assertions. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation . 112–122

    work page 2014

  53. [53]

    John Schulman, Nicolas Heess, Theophane Weber, and Pieter Abbeel. 2015. Gradient estimation using stochastic computation graphs. Advances in neural information processing systems 28 (2015)

    work page 2015

  54. [54]

    Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science . 525–534

    work page 2016

  55. [55]

    David Tolpin, Jan-Willem van de Meent, and Frank Wood. 2015. Probabilistic programming in Anglican. In Machine Learning and Knowledge Discovery in Databases: European Conference, ECML PKDD 2015, Porto, Portugal, September 7-11, 2015, Proceedings, Part III 15 . Springer, 308–311. https://probprog.github.io/anglican/

    work page 2015

  56. [56]

    Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–29

    work page 2019

  57. [57]

    Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An introduction to probabilistic programming. arXiv preprint arXiv:1809.10756 (2018)

    Pith/arXiv arXiv 2018

  58. [58]

    David Wingate, Andreas Stuhlmüller, and Noah Goodman. 2011. Lightweight implementations of probabilistic programming languages via transformational compilation. In Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics. JMLR Workshop and Conference Proceedings, 770–778

    work page 2011

  59. [59]

    Yi Wu, Lei Li, Stuart Russell, and Rastislav Bodik. 2016. Swift: Compiled inference for probabilistic programming languages. arXiv preprint arXiv:1606.09242 (2016)

    Pith/arXiv arXiv 2016

  60. [60]

    Lingfeng Yang, Patrick Hanrahan, and Noah Goodman. 2014. Generating efficient MCMC kernels from probabilistic programs. In Artificial Intelligence and Statistics. PMLR, 1068–1076

    work page 2014

  61. [61]

    stitching together

    Cheng Zhang, Judith Bütepage, Hedvig Kjellström, and Stephan Mandt. 2018. Advances in variational inference. IEEE transactions on pattern analysis and machine intelligence 41, 8 (2018), 2008–2026. , Vol. 1, No. 1, Article . Publication date: September 2025. Static Factorisation of Probabilistic Programs 29 A Control-Flow Graph Construction Definition 8. A...

    work page 2018

  62. [62]

    x " , Bernoulli ( p )) if x == 1 then y = sample (

    If there is a node𝑁′ between𝑁𝑗 and𝑁𝑖+1 in the execution sequence that assigns𝑥,𝑁′∈ RD(𝑁𝑖+1,𝑥), then by definitions of𝑉 1 𝑥 ,𝑉 2 𝑥 , and𝑉𝑁𝑖+1 𝑥 we have 𝜎𝑖+1(𝑥) = ife(𝑉𝐵 𝐸(tr),𝑉 1 𝑥(tr),𝑉 2 𝑥(tr)) =𝑉𝑁𝑖+1 𝑥 (tr). If there is no such𝑁′, then 𝜎𝑖+1(𝑥) =𝜎𝑗(𝑥) =𝑉𝑁𝑗 𝑥 (tr) =𝑉𝑁𝑖+1 𝑥 (tr). □ B.3 Proof of Proposition 3 Statement. For all program𝑆 with CFG𝐺 and unroll...

    work page 2025

  63. [63]

    key errors

    in both execution sequences that evaluates differently, 𝑉𝐵 𝐸(tr1) ≠𝑉𝐵 𝐸(tr2) for𝐸 = condexp(𝐵). By induction assumption, 𝑀𝛼 ∈ provnode(𝐵,𝐸) and Equation (21) implies𝑀𝛼∈ provnode(𝑀,𝑥). • Case 2.𝑀′ B 𝑀′ 1 =𝑀′ 2 = Assign(𝑥 =𝐸): It holds that𝑉𝑀′ 𝐸 (tr1) =𝑉𝑀 𝑥 (tr1) ≠𝑉𝑀 𝑥 (tr2) = 𝑉𝑀′ 𝐸 (tr2). By induction assumption, we have 𝑀𝛼 ∈ provnode(𝑀′,𝐸) and Equation (1...

    work page 2025

  64. [64]

    be a sub-sequence such that 𝜄cfg(𝑀′

    work page

  65. [65]

    Then, the execution sequence in the unrolled version of the sliced CFG 𝐺 SMC 𝑘 matches the sub-sequence:(𝜎′ 1, START) tr −→(𝜎′ 1,𝑀′ 1) tr −→··· tr −→(𝜎′ 2,𝑀′ 2) tr −→(𝜎′ 2, END)

    =𝑁𝑗 are the only sample nodes. Then, the execution sequence in the unrolled version of the sliced CFG 𝐺 SMC 𝑘 matches the sub-sequence:(𝜎′ 1, START) tr −→(𝜎′ 1,𝑀′ 1) tr −→··· tr −→(𝜎′ 2,𝑀′ 2) tr −→(𝜎′ 2, END). Proof. Follows directly from Definition 15. □ , Vol. 1, No. 1, Article . Publication date: September 2025

    work page 2025

This paper was first reviewed by deepseek-v4-flash on August 5, 2026.