Pith. sign in

REVIEW 2 major objections 5 minor 15 references

PPDL: LLM-Based Flows as Probabilistic Programs

T0 review · 2 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

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

Pith's one-line read A flow written once in PPDL compiles to a distribution over outputs that voting, importance sampling, and SMC can all explore.

desk verdict A genuinely useful language contribution undercut by a case-study code/prose mismatch that needs fixing before publication. read the letter →

arxiv 2608.05234 v1 pith:N57C6GEZ submitted 2026-08-05 cs.LG cs.PL

Louis Mandel , Guillaume Baudart , Mandana Vaziri , Martin Hirzel This is my paper · ORCID
classification cs.LGcs.PL
keywords PPDLprobabilisticprogrammingLLM-basedflowsinferencescalingsequentialMonteCarlopromptfactorscoringuncertaintyquantification
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

PPDL is the paper's attempt to bring probabilistic programming to flows of large language model and tool calls. The authors claim that one flow specification, written with the two classic probabilistic constructs — sample, which an LLM call already supplies, and factor, which the language adds — yields a distribution over output values whose quality can be estimated by pluggable inference engines. That decoupling is the point: majority voting, importance sampling, and sequential Monte Carlo become runtime options rather than hand-written search loops inside the program, and the user gets a confidence-bearing distribution instead of a single answer. A formal semantics defines the ideal output distribution as a normalized weighted sum over all execution traces, and experiments across five benchmarks plus a theorem-proving agent for Rocq show accuracy gains and engine-dependent trade-offs. If the claim holds, multi-step LLM applications become testable as probabilistic programs, with uncertainty propagated and reported rather than guessed.

What carries the argument

The load-bearing mechanism is the factor block together with the weighted-sampler reduction rules. A factor evaluates its expression and increments the environment variable pdl score, so every completed trace carries weight $\exp(\texttt{pdl score})$; the model rule samples from an LLM distribution, and the function-call rule propagates pdl context and pdl score so that scoring accumulates across calls. These rules define both the single-trace sampler and the ideal distribution, and the factor points double as resampling points for sequential Monte Carlo, which is what lets computation be redirected toward promising partial traces instead of only reweighting finished ones.

What would settle it

Take one PPDL benchmark flow, keep the program fixed, and re-scale a single factor source — for instance, multiply every flake8-derived penalty by a constant or change the LLM judge's score formula — then re-run the inference engines. If the normalized probabilities, the top-output ranking, or the relative ordering of majority voting, IS, and SMC changes materially under such re-scaling, the factor combination itself, not the flow logic, is carrying the result, and the distribution PPDL returns is not a well-defined object until calibration is settled.

Watch

Extended reading notes

Core claim

The central discovery, on the paper's own terms, is that the two primitives that define probabilistic programming are already nearly present in LLM flows and can be completed with one construct. PDL supplies sample in the form of a model call; PPDL adds factor, a statement that adds a real-valued score to the current trace's log-weight. The ideal semantics then normalizes the exponentials of trace scores over all possible executions to define a categorical distribution over output values, and the language's operational semantics is a weighted sampler that any approximate inference engine can drive. The same program can therefore be executed once for a single answer or under majority voting, importance sampling, or sequential Monte Carlo, with resampling occurring exactly at factor points, and the experiments show that this lets users pick the best scaling strategy per task and model — with SMC outperforming IS in the Rocq proof-repair loop where intermediate verifier feedback carries useful signal.

Load-bearing premise

Everything the language promises depends on the assumption that the numbers different constraints write into factor — an LLM judge's log-odds, a linter's warnings, a proof checker's errors — are on a common scale, so that adding them and normalizing produces a probability distribution that actually tracks how good a trace is; the paper does not calibrate these scales and lists doing so as future work.

Editorial extensions

If this is right

  • One flow specification supports every inference-scaling strategy the runtime offers, so comparing majority voting, importance sampling, and SMC across tasks and models becomes a configuration change rather than a rewrite.
  • The output of a PPDL program is a distribution, giving end users a visible confidence signal and letting developers pick the probability-maximal answer rather than the majority answer, which can win even when it comes from a minority of particles.
  • SMC's resample-at-factor design makes it the preferred engine for long, deep flows with informative intermediate constraints, as in the Rocq theorem-proving agent where SMC@40 solves 95 of 244 problems versus 87.7 for IS@40 at the same token budget.
  • Because the semantics defines the target distribution precisely, any new inference algorithm can be added as a runtime plug-in and evaluated by how well it approximates that target.
  • Hard and soft constraints from heterogeneous sources — LLM judges, linters, verifiers — are unified under a single factor construct, so flows can mix cheap rule-based checks with expensive model-based judges.

Reading between the lines

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

  • The meaningfulness of the returned distribution rests on an unstated calibration assumption: scores from an LLM judge's log-odds, a linter's warning count, and a proof checker's errors are added as if on one scale, so the reported probabilities should not be read as calibrated confidences until factor calibration is validated.
  • The paper's own LiveCodeBench numbers already hint at the limits of that assumption — importance sampling underperforms majority voting for gpt-oss-20b — so a natural extension is to test whether reweighting the factor scales changes the engine rankings.
  • In the Rocq case study, the stated mechanism (scoring particles by the number of errors per attempt) is not what the provided program implements: Figure 24 applies a constant factor of -1 to every failed attempt, so the reported SMC advantage is evidence for resampling with a binary score, not for error-count scoring.
  • The same factor-based interface could generalize to process reward models and other learned verifiers with no language change, since factor is agnostic to where its score comes from.
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.

Referee Report

2 major / 5 minor

Summary. The paper introduces PPDL, an extension of the prompt programming language PDL with a single probabilistic primitive, `factor`. This turns an LLM-based flow into a probabilistic program whose execution yields a weighted distribution over traces and output values. The authors formalize a weighted-sampler semantics, define three inference engines (majority voting, importance sampling, and sequential Monte Carlo) as approximations of an ideal semantics, and describe a parallelized interpreter. The empirical evaluation compares these engines across five benchmarks (GSM8k, Math500, MBPP, LiveCodeBench, FEVER) with six LLMs, and presents a theorem-proving case study on MiniF2F-Rocq. The central claims are that PPDL is the first probabilistic programming language for LLM-based flows and that it lets developers quantify and propagate uncertainty and compare inference scaling strategies without modifying flow logic.

Significance. If the central claims hold, PPDL is a genuinely useful contribution: it brings the decoupling of program logic from inference strategy, familiar from classic PPLs, to LLM and tool flows. The formal semantics in Section 3 is a solid basis for implementation and further reasoning, and the open-source release is a concrete strength. The evaluation is broad and the same programs are used across inference engines, which supports the claim of orthogonality. However, the significance is substantially tempered by two issues: the theorem-proving case study's stated SMC mechanism is not implemented in the provided code, and the uncertainty-quantification claim relies on uncalibrated factor scores, which the paper itself acknowledges as future work.

major comments (2)
  1. [§4.2, Table 3, Figure 24] The description of the SMC@k strategy in §4.2 and Appendix E.6 is inconsistent with the implementation in Figure 24: the text says that the number of errors at each attempt scores the particles, but Line 39 of Figure 24 applies a constant factor of -1 for any failed verification, regardless of the number of errors in result['error']. Consequently, all failed particles receive identical weight at each resampling point, making the resampling step uniform with replacement and incapable of prioritizing fewer-error proofs; the +7.0 to +7.3 SMC-over-IS deltas in Table 3 therefore cannot be attributed to the described mechanism. The authors should either implement error-count-based scoring or revise the text and reinterpret the results.
  2. [Abstract, §3, §6 Limitations] The abstract and introduction claim that PPDL enables developers to 'quantify and propagate uncertainty,' but the distribution returned by PPDL is a function of user-supplied factor scores, which the Limitations section acknowledges are uncalibrated. Without calibration or an analysis of how the posterior probabilities relate to empirical frequencies, the numerical probabilities produced by PPDL (e.g., Table 1) are not validated as uncertainty estimates. The authors should either temper the uncertainty-quantification claim or provide calibration experiments.
minor comments (5)
  1. [§2, Eq. (1)] The scoring formula `score = log(exp(lpt)/(exp(lpt)+exp(lpf)))` is a log-softmax, but the function `utils.llm_judge` is not defined in the paper; consider adding its definition or a reference to the released code.
  2. [Appendix B, Figure 8] In Figure 8, the `Categorical` constructor is passed log-scores directly; if `Categorical` expects unnormalized weights, the scores should be exponentiated. This pseudocode should be aligned with the formal semantics.
  3. [§3.2] The notation `D_p,S` and `D_v,S'` in the SMC rule is confusing because the subscripts mix programs and values; consider using a clearer notation to distinguish distributions over states from distributions over values.
  4. [Table 1] The third row of the right-hand panel of Table 1 appears to have a truncated probability and a missing count; please fix the typesetting.
  5. [§4.1] Since all comparisons use only 5 particles and 3 runs, many differences in Table 2 fall within one standard deviation; the conclusions about which algorithm is best for each task should be phrased as observations rather than statistically significant findings.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: PPDL's semantics and benchmark results are not derived from the paper's own inputs; the only self-referential elements are disclosed and non-load-bearing.

full rationale

PPDL's central contribution is a language design plus a formal semantics (Section 3.1) defining a weighted sampler and an ideal categorical distribution by normalizing exp(pdl score). That is a definition of the semantics, not a derivation that presupposes the paper's empirical claims. The inference engines (majority voting, IS, SMC) in Section 3.2 are presented as finite approximations of this same semantics, and Table 2 evaluates them on external benchmarks (GSM8k, Math500, MBPP, LiveCodeBench, Fever). No model parameter or factor weight is fitted to benchmark answers; factor scores come from the LLM-as-judge log-probability formula and rule-based checkers. The Limitations section explicitly lists calibrating factors as future work, confirming that no calibration loop was used. The MiniF2F case study contains a genuine code/prose mismatch: Section 4.2 attributes SMC's advantage to scoring particles by number of errors, while Figure 24 applies a constant factor of -1 on any verifier error. That is a correctness/reproducibility concern, not a circularity, because the advantage is an empirical outcome rather than a quantity defined by the factor. PPDL is based on PDL (Vaziri et al. 2024) and cites AutoPDL, DeepStan, and pipeline combinators by overlapping authors, but none of these citations supplies a load-bearing theorem or uniqueness result; the base language is described in the paper and the probabilistic contribution is formalized independently. The use of IBM's Granite models is disclosed in the Conflict of Interest statement. Overall, no prediction or claimed result reduces by construction to a fitted input or to a self-citation.

Assumptions & free parameters 4 free parameters · 3 assumptions · 0 invented entities

The central claim is a language design plus an empirical demonstration. The language rests on standard PPL assumptions about weighted sampling, and on domain assumptions about the informativeness of hand-written factors. No target-fitting or circular reuse of the experimental results appears in the derivation.

free parameters (4)
  • Factor weights and score magnitudes = e.g., -1 per proof error, -100 fallback, log-odds from LLM judge
    The relative weights of soft constraints are chosen by hand for each benchmark; the paper's Limitations section says factors are not calibrated.
  • Number of particles = 5 in main experiments; 1 to 40 in case study
    Particle count is a user-selected inference scaling budget, not derived from any principle.
  • Sampling temperature = 0.8 in main experiments; 1.0 in case study
    Model temperature is chosen by the authors and affects output diversity and downstream accuracy.
  • Token budget = 1,000,000 tokens in case study
    The budget defines the trade-off between sequential repair and parallel particle exploration.
assumptions (3)
  • domain assumption LLM outputs can be treated as samples from a proposal distribution, and factor scores as unnormalized likelihoods; the weighted sampler is a valid basis for IS and SMC.
    This is the core probabilistic-programming assumption in Sections 3.1 and 3.2; it is standard for PPLs but is not proven for black-box LLMs whose internal distributions are unknown.
  • domain assumption LLM-as-a-judge responses, converted via the stated log-prob formula, provide meaningful constraint signals.
    Used in Section 2 and all benchmark programs; no calibration or validation is provided, and the Limitations section lists calibration as future work.
  • domain assumption The Rocq prover is a perfect verifier for theorem attempts, so early stopping on verification success is sound.
    Used in Section 4.2 to equate IS@k with pass@k and to terminate all particles on success.

how reviews work

0 comments
Cite this review

Pith. "Pith review of PPDL: LLM-Based Flows as Probabilistic Programs." pith.science (2026). https://pith.science/paper/N57C6GEZ

@misc{pith2026260805234,
  author       = {Pith},
  title        = {Pith review of: PPDL: LLM-Based Flows as Probabilistic Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/N57C6GEZ}},
  note         = {Machine review of arXiv:2608.05234}
}
read the original abstract

Building reliable applications that leverage large language models (LLMs) remains a significant challenge. While LLMs offer impressive capabilities across diverse tasks, their outputs often lack accuracy and provide no clear measure of confidence. This uncertainty compounds in flows of multiple calls to LLMs and other tools, making it difficult for developers and end-users to trust the results. This paper introduces a probabilistic language for programming LLM-based flows. It enables developers to quantify and propagate uncertainty throughout the application's flow, and experiment with different inference scaling techniques without adding a single line of code beyond the flow's logic. We present an experimental study to demonstrate this capability, and a case study building a theorem proving agent for the Rocq theorem prover.

Figures

Figures reproduced from arXiv: 2608.05234 by the authors.

Figure 1
Figure 1. Executing LLM-based flows with or without probabilis￾tic programming. Each circle represents an execution state, with darker shades indicating higher normalized probability. either independently or with feedback between attempts, hoping that one of the outputs is correct. Inference scal￾ing usually leverages constraints to refine or select out￾puts, including soft constraints from models and hard con￾straints from r… view at source ↗
Figure 2
Figure 2. PDL program generating a Python function [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 4
Figure 4. Syntax of PPDL (using the flow-style of YAML). Section 2 can be compiled into this kernel. For instance, blocks without an explicit defs clause can be compiled to use an empty defs, and a model block without an input clause can be compiled to use pdl context as input. The top rule of [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figures from the paper (19 more)
Figure 5
Figure 5. Figure 5: Key reduction rules for blocks (p/S ⇒ p or v/S′ ) and block-bodies (b/S → b or v/S′ ). The reduction S ⊢ e ⇓ v represents the evaluation of an expression e into a value v in the environment S. The full semantics is provided in Appendix C. of program states (pairs of pr…
Figure 6
Figure 6. Figure 6: Number of MiniF2F-Rocq problems solved as a func￾tion of proof/repair steps. Each curve shows the mean over three runs, with shaded regions indicating one standard deviation. having more particles since larger particle populations help preserve diversity during resampl…
Figure 7
Figure 7. Figure 7: Implementation in Python using LiteLLM of [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 8
Figure 8. Figure 8: Implementation in Python using LiteLLM of [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 10
Figure 10. Figure 10: Implementation in Python using LangChain of Fig￾ure 3 with SMC probabilistic inference. 17 [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]
Figure 11
Figure 11. Figure 11: Semantics of a block {}/S defs −−→ {}/S pdl1 /S ⇒ pdl′ 1 /S1 {x1:pdl1 ,x2:pdl2 , . . . ,xn:pdln }/S defs −−→ {x1:pdl′ 1 ,x2:pdl2 , . . . ,xn:pdln }/S1 pdl1 /S ⇒ v1/S1 {x2:pdl2 , . . . ,xn:pdln }/S1[x1 ← v1] defs −−→ defs/S′ {x1:pdl1 ,x2:pdl2 , . . . ,xn:pdln }/S defs …
Figure 12
Figure 12. Figure 12: Semantics of defs field. E.3. MBPP The MBPP program ( [PITH_FULL_IMAGE:figures/full_fig_p019_12.png]
Figure 13
Figure 13. Figure 13: Semantics of block bodies. c ∈ (null ∪ bool ∪ number string) S ⊢ c ⇓ c S ⊢ e ⇓ jinja v S ⊢ ${e} ⇓ v {S ⊢ ei ⇓ vi}1≤i≤N S ⊢ [e1, . . . ,en] ⇓ [v1, . . . ,vn] {S ⊢ ei ⇓ vi}1≤i≤N S ⊢ {x1:e1, . . . ,xn:en} ⇓ {x1:v1, . . . ,xn:vn} [PITH_FULL_IMAGE:figures/full_fig_p020_13.png]
Figure 14
Figure 14. Figure 14: Semantics of expressions. S, v, [] contrib −−−−→ S ctx = S[pdl context] + [{content:v}] S ′ = S[pdl context ← ctx ] S, v, [pdl context] contrib −−−−→ S ′ [PITH_FULL_IMAGE:figures/full_fig_p020_14.png]
Figure 15
Figure 15. Figure 15: Semantics of contribute field. 20 [PITH_FULL_IMAGE:figures/full_fig_p020_15.png]
Figure 17
Figure 17. Figure 17: PPDL program for Math500 benchmark. is found or the token budget is exhausted (Line 53), with a maximum iteration limit (Line 54) [PITH_FULL_IMAGE:figures/full_fig_p021_17.png]
Figure 19
Figure 19. Figure 19: PPDL program for LiveCodeBench benchmark. 22 [PITH_FULL_IMAGE:figures/full_fig_p022_19.png]
Figure 20
Figure 20. Figure 20: PPDL program for Fever benchmark (Part 1: tool def￾inition). 1 lastOf: 2 - ${ problem } 3 - model: ${ model } 4 def: response 5 modelResponse: action 6 parameters: ${ dict(parameters, tools=tools)} 7 parser: json 8 - def: evidence 9 for: 10 tool_call: ${ action.choice…
Figure 21
Figure 21. Figure 21: PPDL program for Fever benchmark (Part 2: evidence gathering). 23 [PITH_FULL_IMAGE:figures/full_fig_p023_21.png]
Figure 22
Figure 22. Figure 22: PPDL program for Fever benchmark (Part 3: final verification). 1 defs: 2 logger: 3 aggregator: 4 file: 5 ${ logdir }/logs_${name}_${pdl_particle_id}.txt 6 flush: true 7 mode: w 8 checker: 9 lang: python 10 code: | 11 from proof_checker import Checker 12 workspace=agen…
Figure 23
Figure 23. Figure 23: PPDL program for MiniF2F benchmark (Part 1: ini￾tialization and prompt). 24 [PITH_FULL_IMAGE:figures/full_fig_p024_23.png]
Figure 25
Figure 25. Figure 25: PPDL program for MiniF2F benchmark (Part 3: veri￾fication and result collection). 0 10 20 30 40 50 60 70 80 0 20 40 60 80 Number of Steps Number of Theorems Solved IS@40 IS@20 IS@10 IS@5 IS@1 [PITH_FULL_IMAGE:figures/full_fig_p025_25.png]
Figure 24
Figure 24. Figure 24: PPDL program for MiniF2F benchmark (Part 2: proof/repair loop). 1 - text: | 2 3 Double-checking proof correctness for ${name}... 4 Current status: ${ result["status"] } 5 6 contribute: [logger, stdout] 7 - defs: 8 verification: 9 lang: python 10 code: result = checker…
Figure 27
Figure 27. Figure 27: Number of MiniF2F-Rocq problems solved as a func￾tion of the number of tokens. 26 [PITH_FULL_IMAGE:figures/full_fig_p026_27.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 10 canonical work pages

  1. [1]

    The for- mula to calculate the nth centered hexagonal number is given by:1+6+ 12 +...+ 6(n− 1), which simpli- fies to3n 2 −3n+

    By substitut- ing the sum of the first (n-1) natural numbers into the expression, we get ‘1 + 6*((n- 1)*n/2)‘, which simplifies to ‘1 + 3*n*(n-1)‘. . . . . . . The for- mula to calculate the nth centered hexagonal number is given by:1+6+ 12 +...+ 6(n− 1), which simpli- fies to3n 2 −3n+

    work page

  2. [5]

    watsonx / meta - llama / llama -4 - maverick -

    URLhttp://arxiv.org/abs/2410.19135. Viennot, J., Baudart, G., Arias, E. J. G., and Lelarge, M. Minif2f in rocq: Automatic translation between proof assistants - a case study.CoRR, abs/2503.04763, 2025. Wang, H., Xin, H., Liu, Z., Li, W., Huang, Y ., Lu, J., Yang, Z., Tang, J., Yin, J., Li, Z., et al. Proving theorems re- cursively.arXiv preprint arXiv:240...

    arXiv 2025

  3. [9]

    Substituting the sum of the first ‘n‘ natural num- bers into the for- mula for the nth centered hexago- nal number gives ‘1 + 6 * (n * (n +

    work page

  4. [10]

    "" ... "

    / 2)‘. . . . . . . The formula can be simplified to 1 + 6(n(n+1)/2). . . . score −10.75 −0.000 000 002 −0.000 000 009 −15.99 −18.75 (prob) 0.000 010 723 0.499 994 610 0.499 994 607 0.000 000 057 0.000 000 004 solution def centered hex... """ ... """ if not isinstance(n, int) or n <= 0: raise ValueError("n must be a positive integer") return 1 + 3*n*(n-1) ...

    work page

  5. [12]

    role " :

    , 13" role " : " user " , 14} 15] 16response = completion ( model = llm , messages = messages ) 17plan = response . choices [0]. message 18messages = messages + [ plan ] 19messages = messages + [ 20{ 21" content " : ( 22" Generate a complete executable Python function " 23" definition corresponding to the above plan and " 24" problem . Generate only a sin...

    work page

  6. [15]

    role " :

    , 16" role " : " user " , 17} 18] 19response = completion ( model = llm , messages = messages ) 20plan = response . choices [0]. message 21messages = messages + [ plan ] 22constraint = ( 23" This plan for the following problem is correct .\ n " 24f " { p rob le m_ st ate me nt }\ n " 25) 26score = score + utils . llm_judge ( llm , plan , constraint ) 27me...

    work page

  7. [16]

    role " :

    , 17" role " : " user " , 18} 19] 20response = completion ( model = llm , messages = messages ) 21plan = response . choices [0]. message 22messages = messages + [ plan ] 23constraint = ( 24" This plan for the following problem is correct .\ n " 25f " { p rob le m_ st ate me nt }\ n " 26) 27score = score + utils . llm_judge ( llm , plan , constraint ) 28st...

    work page

  8. [25]

    role " :

    , 26" role " : " user " , 27} 28] 29response = completion ( model = llm , messages = messages ) 30solution_str = response . choices [0]. message [ " content " ] 31solution_match = re . fullmatch ( 32r " (.|\ n ) *‘ ‘ ‘ python \ n (? P < code >(.|\ n )*?) ‘ ‘ ‘(.|\ n )*" , 33solution_str , flags = re . M 34) 35solution = solution_match . group ( " code " )...

    work page

Show all 15 references
  1. [28]

    Problem: $ { problem }

    to score the solution’s correctness (Lines 18-28). The fallbackattribute (Lines 30-31) assigns a large negative score if an error occurs, effectively filtering out malformed responses during inference. E.2. Math500 The Math500 program (Figure 17) follows a similar struc- ture ...

  2. [33]

    role " :

    , 34" role " : " user " , 35} 36] 37response = completion ( model = llm , messages = messages ) 38solution_str = response . choices [0]. message [ " content " ] 39solution_match = re . fullmatch ( 40r " (.|\ n ) *‘ ‘ ‘ python \ n (? P < code >(.|\ n )*?) ‘ ‘ ‘(.|\ n )*" , 41so...

  3. [42]

    role " :

    , 43" role " : " user " , 44} 45] 46response = completion ( model = llm , messages = messages ) 47solution_str = response . choices [0]. message [ " content " ] 48solution_match = re . fullmatch ( 49r " (.|\ n ) *‘ ‘ ‘ python \ n (? P < code >(.|\ n )*?) ‘ ‘ ‘(.|\ n )*" , 50so...

  4. [2021]

    Jain, N., Han, K., Gu, A., Li, W.-D., Yan, F., Zhang, T., Wang, S., Solar-Lezama, A., Sen, K., and Stoica, I

    URLhttps://openreview.net/forum?id=7Bywt2mQsCe. Jain, N., Han, K., Gu, A., Li, W.-D., Yan, F., Zhang, T., Wang, S., Solar-Lezama, A., Sen, K., and Stoica, I. Live- CodeBench: Holistic and contamination free evaluation of large language models for code. InInternational Con- fer...

    2025

  5. [2023]

    Bingham, E., Chen, J

    URLhttps://doi.org/10.1145/3591300. Bingham, E., Chen, J. P., Jankowiak, M., Obermeyer, F., Pradhan, N., Karaletsos, T., Singh, R., Szerlip, P., Hors- fall, P., and Goodman, N. D. Pyro: Deep universal prob- abilistic programming.Journal of Machine Learning Re- search (JMLR), 2...

    doi

  6. [2024]

    Carpenter, B., Gelman, A., Hoffman, M., Lee, D., Goodrich, B., Betancourt, M., Brubaker, M

    URLhttps://arxiv.org/abs/2407.21787. Carpenter, B., Gelman, A., Hoffman, M., Lee, D., Goodrich, B., Betancourt, M., Brubaker, M. A., Guo, J., Li, P., and Riddell, A. Stan: A probabilistic pro- gramming language.Journal of Statistical Software, 76 (1):1–37, 2017. URLhttps://www...

    2017 arXiv

  7. [2025]

    Mikuła, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A

    URLhttps://doi.org/10.1145/3763143. Mikuła, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A. Q., Zhou, J. P., Szegedy, C., Kuci ´nski, Ł., Miło´s, P., and Wu, Y . Magnushammer: A transformer- based approach to premise selection.arXiv preprint arXiv:2303.04488, 2023....

    arXiv

Pith tools

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