{"id":"4f8664a3-1f31-49db-a081-0f4f89459db1","arxiv_id":"2608.08588","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"New lazy HMC algorithms bring gradient-based inference to infinite-dimensional probabilistic programs, with acceptance ratios that collapse to finite products.","lead":"This paper shows how to run Hamiltonian Monte Carlo, a fast gradient-based Bayesian inference method, on probabilistic programs that describe infinite or unbounded random structures. Lazy evaluation makes the method practical because each step only uses finitely many random dimensions, so gradients and acceptance tests stay finite.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Random-walk PACAP verification promised in Sec. B is not delivered, leaving the headline random-walk lazy HMC experiment without a proven correctness guarantee.","rationale":"I stress-tested the reader's flagged Condition A1 (Sec. 4.4/C.4). The induction there is sketchy but seems sound: because each v_l(q(i)) has support inside T=v(q,p), the trajectory's T-coordinates evolve independently of A\\T coordinates, so v^-1(T) is a cylinder; I do not see a concrete failure. The NUTS cap-M issue is explicitly disclosed and analogous to standard max-tree-depth caps. The genuinely undelivered support is the random-walk PACAP verification: Sec. B promises it and provides only the geometric case. This is load-bearing for the paper's own headline model (random walks), since Thm 2 does not cover unbounded search. The gap is concrete and likely closable, so the right verdict remains CONDITIONAL, not REJECT. My recommendation is no change to the reader's verdict, but the requested revision should add the explicit random-walk partition before claiming correctness for that experiment.","tokens_in":45671,"tokens_out":22645,"duration_ms":252316,"concrete_test":"Independently construct the PACAP partition for Listing 2's walkModel: for each n>=1 and each sign pattern sigma in {+,-}^n define the cylinder E_{n,sigma} where the walk has not rested before n, stops at n (splitting the disjuncts), and sign(step_i)=sigma_i for i<=n; include the measure-zero boundaries step_i=0 and d_n=distLim as separate cylinders; verify each E_{n,sigma} is an analytic cylinder with finite support and that the score is analytic there. If the construction succeeds, the gap is closed and the conditional verdict can stand; if a piece fails to be cylindrical, the random-walk experiment lacks a PACAP guarantee.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires PACAP so that Thm 3 can be instantiated. Thm 2 covers only the core calculus; Sec. 3.2 and Sec. B state that the geometric and random-walk models involve unbounded search, but their PACAP property can be verified directly (Sec. B). Sec. B, however, constructs the analytic-cylinder partition only for the geometric distribution. Listing 2's walkModel stops at the first n with x_n<=0 or d_n>=distLim via `find`, and scores normalLogPdf(1.1,0.1,finalDistance). The PACAP partition for this model is not immediate: the disjunctive stopping condition produces overlaps, and the absolute values in the odometer make the score non-analytic at step=0. One must refine by (i) the stopping time n, (ii) the sign pattern of the first n steps, and (iii) splitting the disjunction into x_n<=0 vs d_n>=distLim vs both. On each such piece the score is an analytic function of finitely many seed coordinates, so the partition exists; but the paper never writes it. Without it, the claimed correctness of lazyHMC on the random-walk experiment (Sec. 6, Fig. 3b) is unsupported. This is an explicit missing-support passage, not an internal contradiction.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":1681,"tokens_out":2259,"duration_ms":60602,"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":[{"comment":"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.","section":"§3.2 and Appendix B"},{"comment":"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.","section":"§D.1 (lazyNUTS)"},{"comment":"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.","section":"§4.4 and §C.4 (Condition A1)"}],"minor_comments":[{"comment":"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.","section":"§4.5, Note on K"},{"comment":"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.","section":"§5, PACAP partition for step regression"},{"comment":"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.","section":"§D.1, no-U-turn criterion"},{"comment":"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.","section":"§6, random walk ground truth"}],"recommendation":"major_revision","confidential_remarks":"The paper is a good fit for the venue, and the core calculus result plus the finite-product acceptance derivation are solid. The two main gaps - the missing random-walk PACAP partition and the unproven start-independence in lazyNUTS - are fixable within the manuscript's scope, but they currently leave the two most prominent empirical demonstrations without a proven correctness guarantee. I would advise the editor that the revision should require those two proofs to be written out, not merely promised."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat 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.\n\nNow 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.\n\nSecond, 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.\n\nThird, 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.\n\nMinor: the runtime comparisons are not controlled, and the authors say so.\n\nNet: 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.","headline":"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.","tokens_in":46508,"tokens_out":1795,"would_cite":true,"duration_ms":20789,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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…","keywords":["probabilistic programming","Hamiltonian Monte Carlo","lazy evaluation","automatic differentiation","measure-theoretic semantics","non-parametric Bayesian inference","No-U-Turn Sampler","piecewise analytic functions"],"falsifier":"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.","tokens_in":45439,"feed_emoji":"🎲","tokens_out":8615,"duration_ms":89927,"temperature":0.7,"pith_summary":"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.","feed_headline":"Laziness lets HMC sample infinite-dimensional models","feed_subtitle":"Gradient support and acceptance ratios stay finite even when the parameter space is infinite.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Establishes the lazy evaluation model, the probability and measure monads underlying the infinite-dimensional seed space, and the gradient-free baseline that the new methods improve on.","marker":"[10]"},{"why":"Demonstrates that almost-sure smoothness is not compositional, motivating the decision to work with analytic partitions.","marker":"[15]"},{"why":"Provides the compositional theory of piecewise analytic functions that the PACAP definition extends to infinite-dimensional product spaces.","marker":"[13]"},{"why":"Introduces the sparse-map Nagata-number automatic differentiation that computes the full gradient in one pass and exposes its finite support.","marker":"[28]"},{"why":"Gives the involutive MCMC stationarity theorem that Framework A instantiates to prove stationarity of the lazy HMC kernels.","marker":"[8]"},{"why":"Defines the No-U-Turn Sampler whose doubling procedure and stopping rule the lazy NUTS implementation adapts.","marker":"[12]"}],"fun_headline_variants":["Lazy HMC: gradient support finite, space infinite","Lazy evaluation unlocks HMC for infinite-dimensional models","Infinite-dimensional HMC: lazy eval keeps gradients finite","Lazy HMC: sampling stochastic processes without discretization","HMC on infinite spaces via lazy evaluation"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Lazy HMC: gradient support finite, space infinite","Lazy evaluation unlocks HMC for infinite-dimensional models","Infinite-dimensional HMC: lazy eval keeps gradients finite","Lazy HMC: sampling stochastic processes without discretization","HMC on infinite spaces via lazy evaluation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000277,"raw_usage":{"total_tokens":1644,"prompt_tokens":932,"completion_tokens":712,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":548,"completion_tokens_details":{"reasoning_tokens":635}},"tokens_in":548,"tokens_out":712,"duration_ms":6770,"temperature":1.0,"reasoning_tokens":635,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:31:17.315502+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Demonstrates that almost-sure smoothness is not compositional, motivating the decision to work with analytic partitions."},{"cited_title":"Hoffman and Andrew Gelman","cited_arxiv_id":null,"evidence_quote":"Defines the No-U-Turn Sampler whose doubling procedure and stopping rule the lazy NUTS implementation adapts."}],"review_version":1}