LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs

C.-H. Luke Ong; Maria-Nicoleta Cr\u{a}ciun; Sam Staton; Tom Schrijvers

REVIEW 3 major objections 4 minor 33 references

LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read The paper proves that Hamiltonian Monte Carlo can be applied directly to lazy, infinite-dimensional probabilistic programs, because the likelihood gradient is finitely supported and the infinite acceptance-ratio product collapses to a…

desk verdict Genuinely new and mostly sound: lazy HMC over rose-tree seed spaces with PACAP smoothness and finite acceptance products, but the flagship random walk experiment lacks the direct PACAP verification the paper promises. read the letter →

arxiv 2608.08588 v1 pith:EEL37SGN submitted 2026-08-09 stat.ML cs.LGcs.PLstat.CO

Maria-Nicoleta Crăciun , C.-H. Luke Ong , Tom Schrijvers , Sam Staton This is my paper · ORCID

classification stat.MLcs.LGcs.PLstat.CO

keywords probabilisticprogrammingHamiltonianMonteCarlolazyevaluationautomaticdifferentiationmeasure-theoreticsemanticsnon-parametricBayesianinferenceNo-U-TurnSamplerpiecewiseanalyticfunctions

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Ordinary HMC needs a finite parameter space and gradients; non-parametric Bayesian models, such as random walks or clustering with an unknown number of components, live on infinite-dimensional spaces. This paper shows that if the probabilistic program is evaluated lazily, HMC still works: the likelihood functions that arise are PACAP, meaning that at almost every point they are analytic in only finitely many coordinates, so their gradient has finite support. The authors structure the HMC proposal so that the acceptance ratio, formally an infinite product over all dimensions, reduces to a finite product over the sites a trajectory actually visits. They implement three lazy HMC variants and a lazy No-U-Turn Sampler, and report posterior samples for geometric, random walk, clustering, step regression, and polynomial models.

What carries the argument

The load-bearing object is PACAP (piecewise analytic under cylindrical analytic partition): a function on an infinite product space whose domain is a countable union of cylinder sets defined by finitely many analytic inequalities, and which is analytic in finitely many coordinates on each piece. PACAP guarantees that the gradient is defined almost everywhere and finitely supported. The companion mechanism is Framework A, which specifies three conditions under which the iMCMC acceptance ratio collapses: the visited set $v(\mathbf{q},\mathbf{p})$ is a cylinder, the involution acts as an independent site-wise map outside $v$, and that map preserves the site density. The implementation uses sparse-map Nagata numbers for automatic differentiation, which returns the full gradient in one pass and reveals which of the infinitely many coordinates matter.

What would settle it

Look for a PACAP likelihood with two adjacent analytic pieces where two states agree on a finite coordinate set $T$ but one lies in a piece whose support exceeds $T$; run the leapfrog trajectory from both states and check whether the visited sets differ. If they differ, the visited set $v(\mathbf{q},\mathbf{p})$ is not a cylinder, Condition A1 fails, and the cancellation in Theorem 3 does not apply; the proof in Section C.4 would need an explicit argument ruling out exactly this case, and the direct PACAP verification in Section B covers the geometric distribution but not the random walk's asserted case.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is Theorem 3: a Markov kernel built on rose-tree states is stationary for the target measure if its involution satisfies three conditions—the visited-site set is a cylinder, the involution decomposes into a finite-dimensional map on visited sites plus independent site maps elsewhere, and the map on unvisited sites preserves the site density—and the acceptance ratio is $\alpha(\mathbf{q},\mathbf{p}) = \ell(\mathbf{q}')/\ell(\mathbf{q})$ times the finite ratio of site densities over the visited set. Together with Theorem 2, which states that every function definable in the paper's core calculus is PACAP, this gives a general route from a lazy probabilistic program to a correct gradient-based sampler. The paper further verifies PACAP directly for unbounded-search programs such as the geometric distribution and uses it in the random-walk model. Three instantiations handle the unvisited dimensions differently: rotations, a different Hamiltonian splitting, or the standard leapfrog with a separate measure-preserving map and full visited-set bookkeeping; a lazy NUTS version adapts trajectory length.

Load-bearing premise

The load-bearing premise is that the set of coordinates a lazy HMC trajectory touches is a cylinder: any two states that agree on those coordinates must touch exactly the same coordinates, so the infinite acceptance-ratio product cancels to a finite one.

Editorial extensions

If this is right

Gradient-based HMC can be used as a generic inference engine for compositional non-parametric models written in a lazy probabilistic programming language, without hand truncation or explicit dimension tracking.
For any program definable in the core calculus—primitive recursion and stream corecursion—the gradient support is finite almost surely, so the leapfrog trajectory touches only finitely many seeds.
The unvisited-coordinate cancellation means the stationary distribution is exact, not an approximation by a finite-dimensional cut-off, whenever the three conditions of Framework A hold.
A lazy No-U-Turn Sampler can set trajectory lengths adaptively, and in the reported experiments it achieves larger effective sample sizes than the fixed-length variants, at lower wall-clock efficiency.
The direct PACAP verification for the geometric distribution shows that unbounded-search programs can also be handled, although they fall outside the general definability theorem.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A testable extension is to instrument the sampled program to detect when a proposed move crosses a boundary between PACAP pieces, and to enlarge the visited set at the boundary: this could turn Condition A1 into a runtime check rather than an unverified proof obligation.
If the cylinder condition holds for all PACAP likelihoods, the same Framework A likely applies to other proposal families—Langevin dynamics, Gibbs-style splits, or particle proposals—as long as the unvisited-site map preserves the prior density.
The sketchiness of the A1 induction suggests a concrete stress test: search, for a simple PACAP likelihood with two adjacent pieces, whether two states agreeing on a candidate visited set can land in different pieces; if so, the visited set $v$ is not a cylinder and Theorem 3 may not apply to that program.
Because lazyNUTS's practical cap on proposed states is not proven to preserve start-independence of the proposed set, one could compare its output distribution under different caps on a model where many visited sites have zero gradient; a cap-dependent drift would indicate a broken detailed balance.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Worth reading. The HMC-over-lazy-rose-trees idea is genuinely new, and for the core calculus it is sold. But the random walk, their flagship demonstration of an infinite stochastic process, is presented with a missing PACAP proof, so the central claim is one verified experiment short of what it promises.

What is new: the PACAP condition, forward-mode AD via sparse Nagata numbers on infinite seed spaces, finite acceptance via the visited-set cylinder condition, and three lazy HMC variants plus lazyNUTS. Framework A's conditions A1-A3 and Theorem 3 give a clean way to make the infinite product in the acceptance ratio collapse. Theorem 2 for the core calculus is a substantial compositional smoothness result, and the logical-relations proof sketched in the appendix is plausible. The step regression example is worked in detail and actually explains how dimension changes happen during a trajectory. Code is on GitHub, and the experiments compare against NP-HMC and lazyLMH with reasonable posterior matching.

Now the soft spots, in proportion. The stress-test note is right: Section 3.2 says the geometric and random walk models involve unbounded search but their PACAP property can be verified directly, and Section B only verifies the geometric distribution. The walkModel in Listing 2 uses find with a disjunctive stopping condition and absolute values, so its PACAP partition is more subtle than the geometric case: you need to split by first stopping point, sign pattern, and which branch fired. That partition is never written down. Without it, the random walk experiment in Figure 3b has correctness claimed but not established. This is a specific, addressable gap, not a fundamental flaw.

Second, lazyNUTS: the paper explicitly says the cap M on proposed states is not shown to preserve the start-independence assumption used in the acceptance-ratio-is-1 proof. That is honest, and it matches what Stan does with max tree depth, so I read it as a minor blemish rather than a new sin.

Third, the proof of Condition A1 in C.4 is an induction sketch. I think it is correct for the stated integrators, but if the cylinder condition is the load-bearing part of the finite-product collapse, a full proof would be appropriate.

Minor: the runtime comparisons are not controlled, and the authors say so.

Net: the paper deserves a serious referee. The gaps are specific and fixable: write the PACAP partition for the random walk, tighten the A1 proof, and state exactly what lazyNUTS claims when M binds. I would bring it to a reading group and would cite it for the PACAP machinery and the lazy HMC framework.

Referee Report

3 major / 4 minor

Summary. The paper proposes HMC-style inference for probabilistic programs with infinite-dimensional, lazily evaluated seed spaces. It introduces PACAP (piecewise analytic under cylindrical analytic partition) as a smoothness condition guaranteeing that definable likelihood functions are locally dependent on finitely many coordinates, so their gradients are finitely supported. A core calculus is shown to yield only PACAP functions (Theorem 2). The paper then formulates a general framework (Framework A) for HMC on rose trees, with an acceptance ratio that collapses to a finite product over visited sites, and proves stationarity of the resulting kernel (Theorem 3). Three HMC variants and a lazy NUTS are derived from this framework, with a step-regression worked example and experiments on geometric distributions, random walks, Gaussian mixtures, and polynomial regression. The paper claims the lazy, infinite-dimensional setting can therefore support gradient-based HMC without truncation or dynamic dimension tracking.

Significance. If the central correctness claims hold, this is a substantial step for probabilistic programming: it provides a compositional, purely declarative route to gradient-based inference over infinite-dimensional parameter spaces, complementing truncation and dynamic-dimension approaches. The paper gives a genuinely new syntactic/analytic criterion (PACAP), a nontrivial measure-theoretic reduction of the acceptance ratio to a finite product, detailed proofs in the appendix, and a public implementation. The core calculus theorem and the finite-product reduction are credible as far as they go, and the experiments illustrate real behaviour on non-parametric models. The gaps identified below concern missing support for two flagship pieces: the random-walk model's PACAP verification and lazyNUTS's start-independence assumption.

major comments (3)

[§3.2 and Appendix B] The paper repeatedly states that the random-walk model of Listing 2 is PACAP and that this can be verified directly, referring to Sec. B; however, Sec. B constructs the analytic-cylinder partition only for the geometric distribution and ends with the remark that 'the geometric distribution and random walk involve unbounded search and require the direct cylinder partition verification illustrated above.' The random-walk likelihood in Listing 2 is not analysed: its stopping condition is a disjunction (x_n <= 0 or d_n >= distLim) with overlapping cases, and the odometer uses absolute values, so the score is not analytic at step boundaries. A PACAP partition would need to refine by stopping index, sign pattern of the first n steps, and the two disjuncts, and none of this is supplied. Since the random-walk experiment in Sec. 6 (Fig. 3b) is presented as evidence that lazy HMC works on an infinite-dimensional model, the missing verification is load-bearing for that claim; it should be written out before the paper can be accepted.
[§D.1 (lazyNUTS)] Proposition 11 derives the acceptance ratio 1 from the assumption that the stopping rule is start-independent, i.e. C_s' = C_s for every s' in C_s. The text immediately concedes that the implementation checks the no-U-turn criterion only on sites with non-zero gradient and additionally caps the number of proposed states at M, and that 'the cap M is not guaranteed to preserve it.' No proof is given that the gradient-restricted U-turn check preserves start-independence. Consequently the correctness argument for lazyNUTS is not established as written: it holds only modulo an unverified property that the implementation may violate. This is a second load-bearing gap, though it may be fixable by either proving start-independence for the restricted check or explicitly scoping the theorem to the uncapped, fully visited case.
[§4.4 and §C.4 (Condition A1)] The proof of Condition A1 in Prop. 5 and Sec. C.4 is sketched: it says that by induction the trajectory coordinates on T depend only on (q_T, p_T), so v^{-1}(T) is a cylinder set. The missing step is to rule out the possibility that a perturbed state (x, y) agreeing with (q, p) on T crosses, along the trajectory, into a PACAP partition piece whose support is not contained in T, which would change the visited set and break the cancellation in Prop. 12. The gap is repairable because if v(q, p) = T then each v_l(q^(i)) is a subset of T, and since the perturbed trajectory agrees with the original on all supports T_i, each position stays in the same local partition piece; but this argument needs to be stated explicitly. As written, the cylinder-set claim is asserted rather than demonstrated, and Condition A1 is the key hypothesis behind Theorem 3.

minor comments (4)

[§4.5, Note on K] The definition of K and the claim that K is an involution are made on the domain S without the restricted set S minus (F composed with psi^L)^{-1}(X times Y minus S) being made explicit in the main text; the parenthetical domain appears only in the sentence after the definition, which is easy to miss.
[§5, PACAP partition for step regression] The partition U_(n_1,...,n_6) is defined using weak monotonicity n_1 <= ... <= n_6 and the constraints t_(n_i-1)(q) < x_i <= t_(n_i)(q); it would be clearer to state explicitly why ties in changepoints (t_j = x_i) are handled or excluded, since such boundaries are measure zero but affect the claimed disjointness.
[§D.1, no-U-turn criterion] The displayed U-turn condition uses a sign convention that may be inconsistent with the standard NUTS criterion; the authors should verify the signs against the cited reference, since the lazy version checks this only on a finite set of coordinates.
[§6, random walk ground truth] The random-walk experiment uses 10^6 importance samples as ground truth, but the text does not state how the importance sampler was constructed; a sentence describing the proposal and the effective sample size of the importance estimate would strengthen the empirical comparison.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: Theorem 3 is a conditional iMCMC result proved from Conditions A1–A3 and the PACAP analysis; self-citations are prior work and the missing random-walk PACAP verification is a completeness gap, not a circular reduction.

full rationale

The central derivation (Sec. 4.4, Thm. 3) is not circular: it takes the iMCMC stationarity theorem (Prop. 1, attributed to Cusumano-Towner et al. [8]) and proves that, under Conditions A1–A3, the Radon–Nikodym derivative is the finite product over the visited set (Prop. 4; proof in Sec. E, Prop. 12). The conditions are verified for the proposed integrators (Prop. 5 and Secs. 4.6–4.7) rather than assumed to contain the conclusion. The finite-support gradient property follows from the definition of PACAP, but the load-bearing content is Thm. 2, which proves definable functions are PACAP by a logical-relations argument carried out in App. A; it is not imported from the authors' prior work. Self-citations ([10], [13], [19], [20]) appear as background, implementation details, or external comparison baselines; none is load-bearing for the stationarity proof. No fitted parameter is relabelled as a prediction: experiments compare against external baselines (NP-HMC, lazyLMH) and ground truth computed by importance sampling. Two admitted gaps are flagged as completeness/correctness issues, not circularity: (i) Sec. 3.2 promises that the random walk model (Listing 2) is PACAP by direct verification in Sec. B, but Sec. B only constructs the cylinder partition for the geometric distribution; the disjunctive stopping condition and odometer absolute values of Listing 2 require an additional, unwritten refinement. (ii) Sec. D.1 admits that the cap M in lazyNUTS is a practical termination 'we do not show to preserve' start-independence, so the acceptance-ratio-1 argument for lazyNUTS is conditional on M not binding. These weaken the paper's completeness but do not make any derivation equal to its inputs by construction.

Assumptions & free parameters 1 free parameters · 6 assumptions · 1 invented entities

The central claim rests on standard measure theory (product measures, Radon-Nikodym, iMCMC), on the PACAP theorem, and on two domain-specific assumptions: the random walk PACAP verification (promised but not shown) and the lazyNUTS start-independence property (broken by the implementation cap M). No physical constants or fitted scientific parameters are involved; the only free parameter is the NUTS cap, which directly affects correctness.

free parameters (1)

M (lazyNUTS proposed-state cap) = 2^6 in experiments
Hand-chosen termination bound for the NUTS doubling procedure. The paper states (Sec. D.1) that this cap is not guaranteed to preserve the start-independent-set property required for stationarity, so correctness of the implemented lazyNUTS depends on M not binding.

assumptions (6)

domain assumption The seed space is R^A with product standard normal measure, constructed via the Kolmogorov extension theorem.
Sec. 2.4.3 and Sec. 4.4 set X = R^A (rose trees) with product N(0,1) measures; all programs are interpreted over this seed space.
standard math The iMCMC stationarity theorem from Cusumano-Towner et al. [8].
Proposition 1 is imported from [8] and used to prove Thm 3 and Framework B.
standard math The HMC leapfrog integrator is reversible and volume-preserving (Prop 2, Neal 2012).
Used to show I_T is a measure-preserving involution in Conditions A2.
domain assumption PACAP partition boundaries form a measure-zero set, so gradients exist almost everywhere.
The paper asserts non-smooth points form a measure-zero set (Sec. 3) but does not give a detailed proof for the general PACAP case; it is standard that analytic zero sets are null.
ad hoc to paper The random walk likelihood is PACAP.
Sec. 3.2 asserts PACAP for the random walk via direct verification (Sec. B), but Sec. B only verifies the geometric distribution; the random walk verification is not shown.
ad hoc to paper For lazyNUTS, the stopping rule is start-independent (Cs' = Cs).
Prop 11 assumes this; the paper admits the implementation's cap M is not guaranteed to preserve it (Sec. D.1).

invented entities (1)

PACAP (piecewise analytic under cylindrical analytic partition) independent evidence
purpose: Smoothness condition on functions X = R^A -> R guaranteeing that the function is locally analytic and depends on only finitely many coordinates, so the gradient is finitely supported (Def. 1, Sec. 3.1).
It is a mathematical definition proved to hold for the core calculus (Thm 2, Sec. A). It is not an unexplained postulate, but a property that is the subject of a proof; independent evidence is the appendix proof, though not machine-checked.

how reviews work

0 comments

Cite this review

Pith. "Pith review of LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs." pith.science (2026). https://pith.science/paper/EEL37SGN

@misc{pith2026260808588,
  author       = {Pith},
  title        = {Pith review of: LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EEL37SGN}},
  note         = {Machine review of arXiv:2608.08588}
}

read the original abstract

Hamiltonian Monte Carlo (HMC) is a successful generic inference method in probabilistic programming, but in its ordinary formulation it needs gradients and finite-dimensional parameter spaces. In Haskell, lazy evaluation lets probabilistic programs express stochastic processes and other non-parametric Bayesian models over implicit infinite-dimensional spaces. This paper develops new formulations of gradient-based HMC for this infinite-dimensional setting, via lazy evaluation. For automatic differentiation, we provide an analysis based on a new notion of "piecewise analytic under cylindrical analytic partition" (PACAP), to show that even if a program is infinite-dimensional and defined lazily, the gradient of the likelihood function is finitely supported. For the Monte Carlo method itself, we develop several HMC variants and a No-U-Turn Sampler that operate over the infinite-dimensional parameter space but are still productive because of lazy evaluation. Experiments cover Gaussian mixture clustering, random walks, and piecewise-constant regression with Poisson-process changepoints.

Figures

Figures reproduced from arXiv: 2608.08588 by the authors.

**Figure 2.** Lazy HMC on the step regression model: (a) an illustrative trajectory, and (b) actual posterior samples. [PITH_FULL_IMAGE:figures/full_fig_p022_2.png] view at source ↗

**Figure 3.** Sampler comparison on the Geometric (left) and random walk (right) models. [PITH_FULL_IMAGE:figures/full_fig_p025_3.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Histogram of the number of components for the GMM, averaged over [PITH_FULL_IMAGE:figures/full_fig_p026_4.png]

**Figure 5.** Figure 5: Histogram of sampled polynomial degrees and posterior fits for the polynomial regression model. [PITH_FULL_IMAGE:figures/full_fig_p026_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 15 canonical work pages

[1]

Christophe Andrieu, Anthony Lee, and Samuel Livingstone. 2020. A general perspective on the Metropolis–Hastings kernel.arXiv preprint arXiv:2012.14881(2020). https://arxiv.org/abs/2012.14881

arXiv 2020
[2]

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo. 2020. On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. InProgramming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Soft...

2020
[3]

2020.Foundations of Probabilistic Programming

Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020.Foundations of Probabilistic Programming. Cambridge University Press. doi:10.1017/9781108770750

doi:10.1017/9781108770750 2020
[4]

Alexandros Beskos, Frank J Pinski, Jesús Marıa Sanz-Serna, and Andrew M Stuart. 2011. Hybrid Monte Carlo on Hilbert spaces.Stochastic Processes and their Applications121, 10 (2011), 2201–2230. doi:10.1016/j.spa.2011.06.003

doi:10.1016/j.spa.2011.06.003 2011
[5]

Michael Betancourt. 2017. A conceptual introduction to Hamiltonian Monte Carlo.arXiv preprint arXiv:1701.02434 (2017)

arXiv 2017
[6]

Nawaf Bou-Rabee, Bob Carpenter, and Milo Marsden. 2024. GIST: Gibbs self-tuning for locally adaptive Hamiltonian Monte Carlo.arXiv preprint arXiv:2404.15253(2024)

arXiv 2024
[7]

Lew, Joshua B

Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, and Vikash K. Mansinghka. 2025. Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs.Proc. ACM Program. Lang.9, PLDI (2025), 1863–1887. doi:10.1145/3729325

work page doi:10.1145/3729325 2025
[8]

Lew, and Vikash K

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). https://arxiv.org/abs/2007.09871

arXiv 2020

Show all 33 references

[9]

Cusumano-Towner, Feras A

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. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, P...

2019
[10]

Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton. 2023. Affine Monads and Lazy Structures for Bayesian Programming.Proc. ACM Program. Lang.7, POPL (2023), 1338–1368. doi:10.1145/3571239

2023 doi
[11]

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 1–12. doi:10.1109/L...

2017
[12]

Hoffman and Andrew Gelman

Matthew D. Hoffman and Andrew Gelman. 2014. The No-U-turn sampler: adaptively setting path lengths in Hamiltonian Monte Carlo.J. Mach. Learn. Res.15, 1 (2014), 1593–1623. http://dl.acm.org/citation.cfm?id=2638586

2014
[13]

Lew, Vikash K

Mathieu Huot, Alexander K. Lew, Vikash K. Mansinghka, and Sam Staton. 2023.𝜔PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs. In38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, ...

2023
[14]

Mathieu Huot, Sam Staton, and Matthijs Vákár. 2020. Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing. InFoundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint ...

2020
[15]

Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2020. On Correctness of Automatic Differentiation for Non-Differentiable Functions. InAdvances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020,...

2020
[16]

2004.Simulating Hamiltonian dynamics

Benedict Leimkuhler and Sebastian Reich. 2004.Simulating Hamiltonian dynamics. Number 14. Cambridge University Press. doi:10.1017/CBO9780511614118

2004 doi
[17]

Samuel Livingstone, Michael Betancourt, Simon Byrne, and Mark Girolami. 2019. On the geometric ergodicity of Hamiltonian Monte Carlo.Bernoulli25, 4A (2019), 3109–3138. doi:10.3150/18-BEJ1083

2019 doi
[18]

2015.Higher-Order Computability

John Longley and Dag Normann. 2015.Higher-Order Computability. Springer, Cham. doi:10.1007/978-3-319-21500-6

2015 doi
[19]

Carol Mak, Fabian Zaiser, and Luke Ong. 2021. Nonparametric Hamiltonian Monte Carlo. InProceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event (Proceedings of Machine Learning Research, Vol. 139), Marina Meila and Tong Zh...

2021
[20]

Carol Mak, Fabian Zaiser, and Luke Ong. 2022. Nonparametric Involutive Markov Chain Monte Carlo. InInternational Conference on Machine Learning, ICML 2022, 17-23 July 2022, Baltimore, Maryland, USA (Proceedings of Machine Learning Research, Vol. 162), Kamalika Chaudhuri, Stefa...

2022
[21]

Radford M. Neal. 2012. MCMC using Hamiltonian dynamics. (6 2012). doi:10.1201/b10905

2012 doi
[22]

Kirill Neklyudov, Max Welling, Evgenii Egorov, and Dmitry P. Vetrov. 2020. Involutive MCMC: a Unifying Framework. InProceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event (Proceedings of Machine Learning Research, Vol. 1...

2020
[23]

Peter Orbanz and Yee Whye Teh. 2010. Bayesian nonparametric models. InEncyclopedia of Machine Learning. Springer, 81–89. doi:10.1007/978-0-387-30164-8_66

2010 doi
[24]

Reynolds

John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. InInformation Processing 83 (IFIP Congress Series, Vol. 9), R.E.A. Mason (Ed.). Elsevier Science Publishers B.V., Amsterdam, The Netherlands, 513–523

1983
[25]

Roy, Vikash K

Daniel M. Roy, Vikash K. Mansinghka, Noah D. Goodman, and Joshua B. Tenenbaum. 2008. A stochastic programming perspective on nonparametric Bayes. InWorkshop on Nonparametric Bayes (ICML 2008). Helsinki, Finland. Filename: RoyManGooTen-ICMLNPB-2008.pdf; MIT. https://danroy.org/...

2008
[26]

Fitzgibbon, Dimitrios Vytiniotis, and Simon Peyton Jones

Amir Shaikhha, Andrew W. Fitzgibbon, Dimitrios Vytiniotis, and Simon Peyton Jones. 2019. Efficient differentiable programming in a functional array-processing language.Proc. ACM Program. Lang.3, ICFP (2019), 97:1–97:30. doi:10.1145/3341701

2019 doi
[27]

Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming.CoRRabs/1809.10756 (2018). arXiv:1809.10756 http://arxiv.org/abs/1809.10756

2018 arXiv
[28]

Birthe van den Berg, Tom Schrijvers, James McKinna, and Alexander Vandenbroucke. 2024. Forward- or Reverse- Mode Automatic Differentiation: What’s the Difference?Science of Computer Programming231 (2024), 103010. doi:10.1016/j.scico.2023.103010

2024
[29]

Aki Vehtari, A Gelman, D Dunson, D Rubin, H Stern, and JB Carlin. 2014. Bayesian data analysis

2014
[30]

David Wingate, Andreas Stuhlmüller, and Noah D. Goodman. 2011. Lightweight Implementations of Probabilistic Programming Languages Via Transformational Compilation. InProceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2011,...

2011
[31]

1993.The formal semantics of programming languages: an introduction

Glynn Winskel. 1993.The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA

1993
[32]

Wood, Jan-Willem van de Meent, and Vikash Mansinghka

Frank D. Wood, Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Pro- gramming Inference. InProceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014, Reykjavik, Iceland, April 22-25, 201...

2014
[33]

Yuan Zhou, Hongseok Yang, Yee Whye Teh, and Tom Rainforth. 2020. Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support. InProceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtu...

2020

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Christophe Andrieu, Anthony Lee, and Samuel Livingstone. 2020. A general perspective on the Metropolis–Hastings kernel.arXiv preprint arXiv:2012.14881(2020). https://arxiv.org/abs/2012.14881

arXiv 2020

[2] [2]

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, and Francesco Gavazzo. 2020. On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. InProgramming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Soft...

2020

[3] [3]

2020.Foundations of Probabilistic Programming

Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020.Foundations of Probabilistic Programming. Cambridge University Press. doi:10.1017/9781108770750

doi:10.1017/9781108770750 2020

[4] [4]

Alexandros Beskos, Frank J Pinski, Jesús Marıa Sanz-Serna, and Andrew M Stuart. 2011. Hybrid Monte Carlo on Hilbert spaces.Stochastic Processes and their Applications121, 10 (2011), 2201–2230. doi:10.1016/j.spa.2011.06.003

doi:10.1016/j.spa.2011.06.003 2011

[5] [5]

Michael Betancourt. 2017. A conceptual introduction to Hamiltonian Monte Carlo.arXiv preprint arXiv:1701.02434 (2017)

arXiv 2017

[6] [6]

Nawaf Bou-Rabee, Bob Carpenter, and Milo Marsden. 2024. GIST: Gibbs self-tuning for locally adaptive Hamiltonian Monte Carlo.arXiv preprint arXiv:2404.15253(2024)

arXiv 2024

[7] [7]

Lew, Joshua B

Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, and Vikash K. Mansinghka. 2025. Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs.Proc. ACM Program. Lang.9, PLDI (2025), 1863–1887. doi:10.1145/3729325

work page doi:10.1145/3729325 2025

[8] [8]

Lew, and Vikash K

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). https://arxiv.org/abs/2007.09871

arXiv 2020