Pith. sign in

REVIEW 1 major objections 4 minor 79 references

Random Variate Generation with Formal Guarantees

T0 review · 1 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Any finite-precision CDF program can be turned into an exact random variate generator that consumes the minimum expected number of input bits and uses only fixed-width integer arithmetic.

desk verdict A genuinely new method for exact finite-precision random variate generation, with a real but fixable gap between the formal theorem and the advertised GSL interop. read the letter →

arxiv 2507.13494 v1 pith:NOCWGRS2 submitted 2025-07-17 cs.PL stat.CO

Feras A. Saad , Wonyeol Lee This is my paper · ORCID
classification cs.PLstat.CO MSC 65C1068W20
keywords randomvariategenerationentropy-optimalsamplingDDGtreesfinite-precisionCDFbinarynumberformatslazypathrefinementformalguaranteescumulativedistributionfunction
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

Standard random-variate libraries operate under an idealized model in which a computer can draw a perfectly uniform real number and compute with infinite precision; on actual hardware, the distribution actually produced by such a generator is generally unknown, inconsistent with the library's own distribution functions, and unreliable in the tails. The paper replaces this pipeline with a formal one: the user supplies a finite-precision numerical program that computes a cumulative distribution function (CDF), and the method automatically synthesizes a generator that is exact for that CDF. The central claim is that the synthesized generator is entropy-optimal, meaning it uses the fewest expected random bits possible among all exact generators for that distribution, and it does so using only fixed-width integer arithmetic at the same precision as the CDF. A variant that combines the CDF with a survival function widens the support of the generator, especially in the tails, while preserving the same guarantees. If the central claim is right, exact samplers with known output distributions become an automation step rather than a hand-tuned implementation task.

What carries the argument

The load-bearing object is the entropy-optimal discrete distribution generating (DDG) tree: a prefix-free binary decision tree in which the number of leaves labeled with outcome $i$ at depth $j$ equals the $j$-th binary digit of the outcome's probability. Rather than build such a tree, Algorithm 1 performs lazy path refinement, expanding only the leaf reached on the current execution and using two classification theorems about binary expansions to know, at each level, whether the next bit is forced, whether a coin flip suffices, or whether the tree must be refined further. The finite-precision engine is a tuple-based bit extraction procedure that encodes the exact difference $x -_{\mathbb{R}} x'$ of two floats as bit counts and integer tails and recovers any requested binary digit with integer shifts and masks; all intermediate values are representable in a single machine word.

What would settle it

Enumerate all CDFs over a tiny binary format, such as a format with $1+E+m = 3$ bits, run the synthesized generator on every random-bit prefix up to a fixed depth, and compare the empirical output frequencies with $F(b)-F(\operatorname{pred}(b))$ over the format's values; any mismatch would falsify the exactness part of Theorem 5.17. For entropy optimality, compute the average number of bits consumed per output over the same enumeration and check it against the binary-expansion leaf-count sum $\sum_i \sum_j j\,2^{-j}\,[p_i]_j$; a measured cost below the lower bound is impossible and a cost above it would violate optimality.

Watch

Extended reading notes

Core claim

The paper's central discovery is that entropy-optimal generation is feasible for any finite-precision CDF without constructing an exponentially large decision tree. Its Theorem 5.17 states that Algorithm 2, synthesized from a CDF over any binary number format, returns a string $x$ with cumulative probability exactly $F(x)$ and consumes the minimum expected number of input bits among all exact generators, matching the information-theoretic lower bound for random variate generation. The proof works by viewing the CDF as a binary-coded probability distribution and lazily walking a single path through an entropy-optimal discrete distribution generating tree, refining only the leaf reached on the executed path. Two structural theorems about binary expansions of dyadic sums guarantee that at each refinement step there is exactly one relevant leaf, so the walk uses $O(k)$ time and $O(1)$ space per path, an improvement over the original full-tree construction. The finite-precision implementation extracts bits of exact differences of floating-point probabilities directly from their exponent and significand fields, keeping every intermediate value within one machine word.

Load-bearing premise

The guarantee depends on the supplied CDF being a genuine finite-precision specification: it must be monotone nondecreasing, return values in $[0,1]$, and assign cumulative probability $1$ to the largest representable value; if the implementation violates these conditions, or if the specification itself misrepresents the intended distribution, the generator is exact only for that specification and inherits its errors.

Editorial extensions

If this is right

  • Any CDF satisfying the finite-precision definition yields a generator whose output distribution is known explicitly, so the CDF, survival, and quantile operations of a library become mutually consistent by construction.
  • Practitioners can replace hand-written samplers with synthesized ones for the same formal specification, eliminating the gap between the intended distribution and the distribution actually sampled.
  • Because the generator uses only fixed-width integer arithmetic at the CDF's own precision, it cannot overflow, needs no arbitrary-precision library, and has a predictable per-variate memory cost.
  • Combining a CDF with a survival function at the median cutoff doubles the number of representable outcomes and restores symmetry for symmetric distributions, at negligible entropy and runtime overhead in the reported evaluations.

Reading between the lines

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

  • The same synthesis recipe should extend to any piecewise finite-precision specification of a distribution: wherever a monotone endpoint-correct function is supplied, the DDG machinery applies, so users could define a CDF that switches approximations by region to obtain arbitrarily shaped tail policies. This is an extension the paper does not develop.
  • In settings where finite-precision sampling errors erase formal guarantees, such as differential privacy and lattice-based cryptography, the natural next experiment is to swap the affected sampler for a generator synthesized from a carefully debugged CDF and re-run the privacy or security evaluation; the exactness guarantee would then transfer to the application.
  • Because the expected bit cost of the optimal generator is bounded by a closed form in the format parameters, the measured bits-per-variate of a synthesized generator can serve as a diagnostic for how close a given CDF implementation is to a maximum-entropy distribution over the format.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 4 minor

Summary. The paper proposes a finite-precision approach to random variate generation. The user supplies a cumulative distribution function (CDF) implemented as a program over a binary number format; the method automatically synthesizes a generator that is exact for that finite-precision CDF and consumes the information-theoretically minimal expected number of random bits. The theoretical core is a lazy, space-time optimal extension of Knuth-Yao discrete distribution generating trees (Algorithm 1, Theorem 4.6), specialized to finite-precision CDFs via an exact bit-extraction procedure using only fixed-width integer arithmetic (Algorithms 2-4, Theorems 5.16-5.18). A further extension combines a CDF and a survival function into a dual distribution function for wider tail coverage (Section 6, Theorem 6.3). The paper also reports a C implementation and an empirical comparison against the GNU Scientific Library. The central theorem is supported by detailed proofs in the appendices.

Significance. If the central theorem holds, this is a significant advance: it replaces ad-hoc, Real-RAM-based samplers with automatically synthesized generators that are exact for a formally specified finite-precision distribution, entropy-optimal in the Knuth-Yao sense, and implemented with fixed-width integer arithmetic only. The paper provides detailed proofs for the bit-extraction correctness (Theorem 5.16) and the entropy-optimality of the finite-precision algorithm (Theorem 5.17), and it ships a C library and reproduction package. The extension to dual distribution functions is well motivated and also proved (Theorem 6.3). The main caveat is that the advertised reuse of existing GSL CDFs in the paper's examples is, as written, outside the formal contract of Definition 5.10, which requires a wrapper or explicit user guidance; this does not invalidate the theorem but does affect the practical claims.

major comments (1)
  1. [Section 5.2 / Listing 2 / Theorem 5.17] Theorem 5.17 is conditional on Definition 5.10, which requires F(phi_B(1^n)) = 1. For IEEE-754 formats, Example 5.6 maps the maximal bit string 1^n to the NaN pattern (the extended-real top element of Definition 5.1), not to +infinity. Standard implementations such as gsl_cdf_gaussian_P return NaN for a NaN input, so they do not satisfy the condition F(phi_B(1^n)) = 1. Algorithm 2 sets the initial upper cumulative probability to f1 = 1 and never evaluates F at phi_B(1^n); it thereby assigns the top interval probability 1 - F(pred_B(1^n)) to an output whose claimed cumulative probability F(x) is, under the user-supplied GSL CDF, NaN rather than 1. Consequently, the direct usage advertised in Listing 2 (GENERATE_FROM_CDF(gsl_cdf_gaussian_P, 5.0)) does not meet the theorem's preconditions, and the paper's statement that existing GSL CDFs can be reused as-is is unsupported as written. This is not a flaw in the proof for compliant CDFs, but it is a load-bearing gap between the formal theorem and the advertised practical interface. The paper should explicitly state that user CDFs must satisfy Definition 5.10, provide a wrapper that clamps the NaN (top) input to 1 (and, for survival functions, clamps the top input to 0), or clearly restrict the direct-reuse claims to CDFs that already satisfy the contract.
minor comments (4)
  1. [Abstract / Section 7] The abstract and Section 7 use the word 'accuracy' (e.g., 'delivering higher accuracy'), but the evaluation in Table 2 measures output range coverage, not a statistical accuracy metric such as total variation distance or a tail-precision measure. A wider output range does not by itself establish higher accuracy; please rephrase the claim as 'wider output range coverage' or add distributional-distance measurements.
  2. [Figure 5 and Algorithm 1] The trace in Figure 5b and the tree explanation in Figure 5c are dense; the roles of gray, blue, yellow, and pink bits are explained in the caption, but the correspondence between the trace and the recursion levels would be easier to follow if the recursion levels were explicitly numbered in both the figure and the pseudocode.
  3. [Section 4.2, Algorithm 1] For a general binary-coded probability distribution (Definition 4.1), the while loop in Algorithm 1 terminates almost surely but not necessarily in bounded time unless the probabilities are dyadic rationals. The paper states this for Algorithm 2 in Section 5.3, but an explicit remark near Algorithm 1 would avoid confusion for readers who apply the algorithm to arbitrary real-valued binary-coded distributions.
  4. [Section 7.1, Table 1] The text reports that GSL generators are 2.6x-142x more expensive in bits/variate than OPT, but for Pascal(1,5) the OPT value is 0.00 bits; the ratio is then undefined or infinite. Consider reporting this case separately or using a non-ratio statement for zero-entropy cases.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the central optimality claim is proved against the external Knuth–Yao lower bound, the output distribution is the input CDF by explicit specification, and self-citations are confined to related work.

full rationale

The load-bearing chain is self-contained and terminates at an external benchmark. Theorem 5.17 is proved by combining (i) Algorithm 1's correctness and entropy-optimality for binary-coded distributions (Theorem 4.6), established in Appendix C through Corollaries C.5–C.6, which identify the generator's expected cost with the Knuth–Yao lower bound E[C_n] = sum_b sum_l l*2^{-l}[p(b)]_l (Theorem 3.9, an external result); (ii) the number-theoretic structure theorems 4.2 and 4.4, proved from first principles about binary addition; (iii) Theorem 5.16, proved in Appendix D, showing Algorithms 3–4 extract the exact binary digits of float differences using representable integer arithmetic; and (iv) Prop. 5.13 plus Props. 5.14 and Cor. 5.15, which transport a finite-precision CDF F over any binary format B to a binary-coded distribution over U_n. Nothing is fitted: no parameter is learned from data, the generator takes only the CDF as input, and the entropy bound of Theorem 5.18 is a closed-form maximum derived from Theorem D.2 and Prop. D.3. The one self-referential element is that the target distribution is defined as the distribution of the input CDF ('generate exact random variates according to this CDF'; Theorem 5.17: 'returns a string x ... with cumulative probability F(x)'). That is the explicit specification of the problem, not a concealed input–output equivalence, and it is flagged by the authors throughout. Self-citations [16, 52–55] appear only in related work, the artifact statement, and acknowledgments; none is load-bearing for Theorem 5.17, and no uniqueness theorem is imported from the authors' own prior work. The skeptical concern that IEEE-754 CDFs may violate Def. 5.10's requirement F(phi_B(1^n))=1 (returning NaN instead of 1) is a gap between the theorem's hypotheses and the advertised GSL examples — a correctness risk, not circularity, since the theorem is explicitly conditional on Def. 5.10. Score 1 reflects only the benign definitional self-reference and the presence of non-load-bearing self-citations.

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

The central mechanism adds no fitted constants. It assumes an unbiased random-bit source and a CDF that meets the finite-precision contract. The entropy-optimality benchmark is the external Knuth-Yao theorem, and the bit-extraction proof is self-contained. The DDF extension introduces a deterministic cutoff at the median plus a representation pair, but no parameter is fit to evaluation data.

assumptions (4)
  • domain assumption Random bits from the entropy source are independent Bernoulli(1/2) draws.
    Definition 3.5 and Figure 1 model the input as an i.i.d. unbiased bit stream; entropy-optimality is measured with respect to this source, so biased or correlated bits would invalidate the bit-consumption guarantees.
  • domain assumption The input CDF is a finite-precision CDF: monotone nondecreasing, F(phi_B(1^n))=1, and all outputs in F^E_m intersected with [0,1].
    Definition 5.10 and Theorem 5.17; arbitrary C programs are outside the guarantee unless they satisfy this contract.
  • standard math Knuth and Yao's characterization of entropy-optimal DDG trees.
    Theorem 3.9 is used as the external benchmark for optimal expected bit consumption in Theorem 4.6 and Corollary C.6.
  • domain assumption The ordering bijection phi_B makes the chosen binary format monotone with respect to the extended reals.
    Definition 5.2 and Proposition 5.8; this is how generation over unsigned integers is transplanted back to formats such as IEEE-754 and posits.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Random Variate Generation with Formal Guarantees." pith.science (2026). https://pith.science/paper/NOCWGRS2

@misc{pith2026250713494,
  author       = {Pith},
  title        = {Pith review of: Random Variate Generation with Formal Guarantees},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NOCWGRS2}},
  note         = {Machine review of arXiv:2507.13494}
}
read the original abstract

This article introduces a new approach to principled and practical random variate generation with formal guarantees. The key idea is to first specify the desired probability distribution in terms of a finite-precision numerical program that defines its cumulative distribution function (CDF), and then generate exact random variates according to this CDF. We present a universal and fully automated method to synthesize exact random variate generators given any numerical CDF implemented in any binary number format, such as floating-point, fixed-point, and posits. The method is guaranteed to operate with the same precision used to specify the CDF, does not overflow, avoids expensive arbitrary-precision arithmetic, and exposes a consistent API. The method rests on a novel space-time optimal implementation for the class of generators that attain the information-theoretically optimal Knuth and Yao entropy rate, consuming the least possible number of input random bits per output variate. We develop a random variate generation library using our method in C and evaluate it on a diverse set of ``continuous'' and ``discrete'' distributions, showing competitive runtime with the state-of-the-art GNU Scientific Library while delivering higher accuracy, entropy efficiency, and automation.

Figures

Figures reproduced from arXiv: 2507.13494 by the authors.

Figure 1
Figure 1. Random variate generation with infinite-precision (Real-RAM) and finite-precision computation. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Overview of the standard and proposed approaches to random variate generation software libraries. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Three random variate generators represented as discrete distribution generating (DDG) trees. The 0/1 [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Dynamically refining the leaves of an optimal DDG tree for lazy random variate generation. [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Entropy-optimal generation for a binary-coded probability distribution [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Three possible DDG tree refinements for outcome [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: A dual distribution function 𝐺 combines a finite-precision cumulative distribution 𝐹 and survival function 𝑆 to represent probabilities in the left tail (blue; below the median cutoff ) and right tail (red; above the median cutoff ), respectively. This combination ensu…
Figure 8
Figure 8. Figure 8: Ratio of bits/variate (lower=better) and variates/sec (higher=better) using the DDF specification ( [PITH_FULL_IMAGE:figures/full_fig_p022_8.png]
Figure 9
Figure 9. Figure 9: DDG trees of random variate generators for the discrete distribution [PITH_FULL_IMAGE:figures/full_fig_p028_9.png]
Figure 10
Figure 10. Figure 10: Conditional bit sampling algorithm for any binary-coded probability distribution [PITH_FULL_IMAGE:figures/full_fig_p029_10.png]
Figure 11
Figure 11. Figure 11: DDG tree for a maximum entropy distribution with cumulative probabilities in [PITH_FULL_IMAGE:figures/full_fig_p044_11.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

79 extracted references · 54 canonical work pages

  1. [1]

    Abowd et al

    John M. Abowd et al. 2022. The 2020 Census Disclosure Avoidance System TopDown Algorithm.Harvard Data Science ReviewSpecial Issue 2 (June 2022), 77 pages.https://doi.org/10.1162/99608f92.529e3cb9

    doi:10.1162/99608f92.529e3cb9 2022

  2. [2]

    Alexander Bagnall, Gordon Stewart, and Anindya Banerjee. 2023. Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning.Proc. ACM Program. Lang.7, PLDI, Article 106 (2023), 24 pages.https: //doi.org/10.1145/3591220

    doi:10.1145/3591220 2023

  3. [3]

    2020.Foundations of Probabilistic Programming

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

    doi:10.1017/9781108770750 2020

  4. [4]

    Vaishak Belle, Andrea Passerini, and Guy Van den Broeck. 2015. Probabilistic Inference in Hybrid Domains by Weighted Model Integration. InProceedings of the 24th International Joint Conference on Artificial Intelligence. AAAI Press, Palo Alto, 2770–2776

    work page 2015

  5. [5]

    1986.Probability and Measure(2nd ed.)

    Patrick Billingsley. 1986.Probability and Measure(2nd ed.). John Wiley & Sons, New York

    work page 1986

  6. [6]

    Bogachev

    Vladimir I. Bogachev. 2007.Measure Theory. Vol. 2. Springer, Berlin.https://doi.org/10.1007/978-3-540-34514-5

    doi:10.1007/978-3-540-34514-5 2007

  7. [7]

    Ian Briggs, Yash Lad, and Pavel Panchekha. 2024. Implementation and Synthesis of Math Library Functions.Proc. ACM Program. Lang.8, POPL, Article 32 (Jan. 2024), 28 pages.https://doi.org/10.1145/3632874

    doi:10.1145/3632874 2024

  8. [8]

    Campbell

    Taylor R. Campbell. 2014. Uniform Random Floats.https://prng.di.unimi.it/random_real.c

    work page 2014

Show all 79 references
  1. [9]

    Clément L Canonne, Gautam Kamath, and Thomas Steinke. 2020. The Discrete Gaussian for Differential Privacy. In Proceedings of the 34 International Conference on Neural Information Processing Systems (Advances in Neural Information Processing Systems, Vol. 33). Curran Associate...

    2020 doi

  2. [10]

    2006.CR-LIBM: A Library of Correctly Rounded Elementary Functions in Double-Precision

    Catherine Daramy-Loirat, David Defour, Florent de Dinechin, Matthieu Gallet, Nicolas Gast, Christoph Lauter, and Jean-Michel Muller. 2006.CR-LIBM: A Library of Correctly Rounded Elementary Functions in Double-Precision. Research Report ensl-01529804. Laboratoire de l’Informati...

    2006

  3. [11]

    Christian de Schryver, Daniel Schmidt, Norbert Wehn, Elke Korn, Henning Marxen, Anton Kostiuk, and Ralf Korn. 2012. A Hardware Efficient Random Number Generator for Nonuniform Distributions with Arbitrary Precision.International Journal of Reconfigurable Computing2012, Article...

    2012 doi

  4. [12]

    Gerhard Derflinger, Wolfgang Hörmann, and Josef Leydold. 2010. Random Variate Generation by Numerical Inversion when Only the Density is Known.ACM Transactions on Modeling and Computer Simulation20, 4, Article 18 (Oct. 2010), 25 pages.https://doi.org/10.1145/1842722.1842723

    2010

  5. [13]

    1986.Non-Uniform Random Variate Generation

    Luc Devroye. 1986.Non-Uniform Random Variate Generation. Springer-Verlag, New York

    1986

  6. [14]

    Luc Devroye and Claude Gravel. 2015. Sampling with Arbitrary Precision. arXiv:1502.02539v1

    2015 arXiv

  7. [15]

    Allen B. Downey. 2007. Generating Pseudo-random Floating-Point Values.https://allendowney.com/research/rand/ downey07randfloat.pdf

    2007

  8. [16]

    Draper and Feras A

    Thomas L. Draper and Feras A. Saad. 2025. Efficient Rejection Sampling in the Entropy-Optimal Range. arXiv:2504.04267

    2025 arXiv

  9. [17]

    Chaohui Du and Guoqiang Bai. 2015. Towards Efficient Discrete Gaussian Sampling For Lattice-Based Cryptography. InProceedings of the 25th International Conference on Field Programmable Logic and Applications. IEEE Press, Piscataway, 1–6.https://doi.org/10.1109/FPL.2015.7293949

    2015

  10. [18]

    Yusong Du, Baoying Fan, and Baodian Wei. 2022. An Improved Exact Sampling Algorithm for the Standard Normal Distribution.Computational Statistics37 (2022), 721–737.https://doi.org/10.1007/s00180-021-01136-w

    2022 doi

  11. [19]

    Léo Ducas and Phong Q. Nguyen. 2012. Faster Gaussian Lattice Sampling Using Lazy Floating-Point Arithmetic. In Proceedings of the 18th International Conference on the Theory and Application of Cryptology and Information Security (Lecture Notes in Computer Science, Vol. 7658). ...

    2012 doi

  12. [20]

    Dwarakanath and Steven D

    Nagarjun C. Dwarakanath and Steven D. Galbraith. 2014. Sampling from Discrete Gaussians for Lattice-Based Cryptography On a Constrained Device.Applicable Algebra in Engineering, Communication and Computing25, 3 (June 2014), 159–180.https://doi.org/10.1007/s00200-014-0218-3

    2014 doi

  13. [21]

    Cynthia Dwork. 2006. Differential Privacy. InProceedings of the 33rd International Colloquium on Automata, Languages, and Programming. Springer, Berlin, Heidelberg, 1–12.https://doi.org/10.1007/11787006_1

    2006 doi

  14. [22]

    János Folláth. 2014. Gaussian Sampling in Lattice Based Cryptography.Tatra Mountains Mathematical Publications60, 1 (Sept. 2014), 1–23.https://doi.org/10.2478/tmmp-2014-0022

    2014 doi

  15. [23]

    Laurent Fousse, Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. 2007. MPFR: A Multiple- Precision Binary Floating-Point Library with Correct Rounding.ACM Trans. Math. Software33, 2 (June 2007), 15 pages. https://doi.org/10.1145/1236463.1236468

    2007

  16. [24]

    2009.GNU Scientific Library Reference Manual(3rd ed.)

    Mark Galassi, Jim Davies, James Theiler, Brian Gough, Gerard Jungman, Patrick Alken, Michael Booth, and Fabrice Rossi. 2009.GNU Scientific Library Reference Manual(3rd ed.). Network Theory Ltd., Surrey.http://www.gnu.org/software/gsl/

    2009

  17. [25]

    Poorva Garg, Steven Holtzen, Guy Van den Broeck, and Millstein Todd. 2024. Bit Blasting Probabilistic Programs.Proc. ACM Program. Lang.8, PLDI, Article 182 (2024), 24 pages.https://doi.org/10.1145/3656412

    2024 doi

  18. [26]

    Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. 2016. Preserving Differential Privacy Under Finite-Precision Semantics.Theoretical Computer Science655 (Dec. 2016), 92–108.https://doi.org/10.1016/j.tcs.2016.01.015

    2016 doi

  19. [27]

    Michael Giles and Oliver Sheridan-Methven. 2023. Approximating Inverse Cumulative Distribution Functions to Produce Approximate Random Variables.ACM Trans. Math. Software49, 3, Article 26 (Sept. 2023), 29 pages.https: //doi.org/10.1145/3604935

    2023 doi

  20. [28]

    Frédéric Goualard. 2020. Generating Random Floating-Point Numbers by Dividing Integers: A Case Study. InCom- putational Science (Lecture Notes in Computer Science, Vol. 12138). Springer International Publishing, Cham, 15–28. https://doi.org/10.1007/978-3-030-50417-5_2

    2020 doi

  21. [29]

    Frédéric Goualard. 2022. Drawing Random Floating-Point Numbers from an Interval.ACM Transactions on Modeling and Computer Simulation32, 3, Article 16 (April 2022), 24 pages.https://doi.org/10.1145/3503512

    2022 doi

  22. [30]

    Artur Grabowski. 2015. Generating Random Doubles.https://github.com/art4711/random-double/blob/master/rd.c

    2015

  23. [31]

    2023.GNU MP: The GNU Multiple Precision Arithmetic Library(6.3.0 ed.)

    Torbjörn Granlund. 2023.GNU MP: The GNU Multiple Precision Arithmetic Library(6.3.0 ed.). Free Software Foundation, Inc, Boston.https://gmplib.org/gmp-man-6.3.0.pdf

    2023

  24. [32]

    Te Sun Han and Mamoru Hoshi. 1997. Interval Algorithm for Random Number Generation.IEEE Transactions on Information Theory43, 2 (March 1997), 599–611.https://doi.org/10.1109/18.556116

    1997 doi

  25. [33]

    Charles R Harris et al. 2020. Array Programming with NumPy.Nature585 (Sept. 2020), 357–362.https://doi.org/10. 1038/s41586-020-2649-2

    2020

  26. [34]

    2019.IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2019)

    Institute of Electrical and Electronics Engineers. 2019.IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2019). IEEE Press, Piscataway.https://doi.org/10.1109/IEEESTD.2019.8766229

    2019

  27. [35]

    Angshuman Karmakar, Sujoy Sinha Roy, Oscar Reparaz, Frederik Vercauteren, and Ingrid Verbauwhede. 2018. Constant- Time Discrete Gaussian Sampling.IEEE Trans. Comput.67, 11 (2018), 1561–1571.https://doi.org/10.1109/TC.2018. 2814587

    2018 doi

  28. [36]

    Charles F. F. Karney. 2016. Sampling Exactly from the Normal Distribution.ACM Trans. Math. Software42, 1, Article 3 (Jan. 2016), 14 pages.https://doi.org/10.1145/2710016

    2016 doi

  29. [37]

    Knuth and Andrew C

    Donald E. Knuth and Andrew C. Yao. 1976. The Complexity of Nonuniform Random Number Generation. InAlgorithms and Complexity: New Directions and Recent Results, Joseph F. Traub (Ed.). Academic Press, Inc., Orlando, FL, 357–428. Proc. ACM Program. Lang., Vol. 9, No. PLDI, Articl...

    1976

  30. [38]

    Daniel Lemire. 2019. Fast Random Integer Generation in an Interval.ACM Transactions on Modeling and Computer Simulation29, 1, Article 3 (Jan. 2019), 12 pages.https://doi.org/10.1145/3230636

    2019 doi

  31. [40]

    Lim and Santosh Nagarakatte

    Jay P. Lim and Santosh Nagarakatte. 2022. One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes.Proc. ACM Program. Lang.6, POPL, Article 3 (Jan. 2022), 28 pages.https://doi.org/10.1145/3498664

    2022 doi

  32. [41]

    Jérémie Lumbroso. 2013. Optimal Discrete Uniform Generation from Coin Flips, and Applications. arXiv:1304.1916

    2013 arXiv

  33. [42]

    Ilya Mironov. 2012. On Significance of the Least Significant Bits for Differential Privacy. InProceedings of the 2012 ACM Conference on Computer and Communications Security. Association for Computing Machinery, New York, 650–661. https://doi.org/10.1145/2382196.2382264

    2012

  34. [43]

    2017.Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis(second ed.)

    Michael Mitzenmacher and Upfal Eli. 2017.Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis(second ed.). Cambridge University Press, Cambridge, UK

    2017

  35. [44]

    Oller Møller. 1965. Quasi Double-Precision in Floating Point Addition.BIT Numerical Mathematics5, 1 (1965), 37–50. https://doi.org/10.1007/BF01975722

    1965 doi

  36. [45]

    Peter Occil. 2023. More Random Sampling Methods.https://peteroupc.github.io/randomnotes.pdf

    2023

  37. [46]

    Peter Occil. 2023. Partially-Sampled Random Numbers for Accurate Sampling of Continuous Distributions.https: //peteroupc.github.io/exporand.pdf

    2023

  38. [47]

    Peter Occil. 2024. Randomization and Sampling Methods.https://peteroupc.github.io/randomfunc.pdf

    2024

  39. [48]

    Adam Paszke et al. 2019. PyTorch: An Imperative Style, High-Performance Deep Learning Library. InProceedings of the 33rd International Conference on Neural Information Processing Systems (Advances in Neural Information Processing Systems, Vol. 32). Curran Associates, Inc., Red...

    2019

  40. [49]

    2022.Standard for Posit ™ Arithmetic

    Posit Working Group. 2022.Standard for Posit ™ Arithmetic. National Supercomputing Centre, A*STAR, Singapore. https://posithub.org/docs/posit_standard-2.pdf

    2022

  41. [50]

    Press, Saul A

    William H. Press, Saul A. Teukolsky, William T. Vetterling, and Brian P. Flannery. 1992.Numerical Recipes in C(2nd ed.). Cambridge University Press, Cambridge, UK

    1992

  42. [51]

    Roy, Frederik Vercauteren, and Ingrid Verbauwhede

    Sinha S. Roy, Frederik Vercauteren, and Ingrid Verbauwhede. 2013. High Precision Discrete Gaussian Sampling on FPGAs. InProceedings of the 20th International Conference on Selected Areas in Cryptography (Lecture Notes in Computer Science, Vol. 8282). Springer, Berlin, 383–401....

    2013 doi

  43. [52]

    2025.librvg: C Library for Random Variate Generation with Formal Guarantees

    Feras Saad and Wonyeol Lee. 2025.librvg: C Library for Random Variate Generation with Formal Guarantees. Zenodo. https://doi.org/10.5281/zenodo.15243770

    2025 doi

  44. [53]

    Saad, Cameron E

    Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka. 2020. The Fast Loaded Dice Roller: A Near-optimal Exact Sampler for Discrete Probability Distributions. InProceedings of the 23rd International Conference on Artificial Intelligence and Statistics (Pr...

    2020

  45. [54]

    Saad, Cameron E

    Feras A. Saad, Cameron E. Freer, Martin C. Rinard, and Vikash K. Mansinghka. 2020. Optimal Approximate Sampling from Discrete Probability Distributions.Proceedings of the ACM on Programming Languages4, POPL, Article 36 (Jan. 2020), 31 pages.https://doi.org/10.1145/3371104

    2020 doi

  46. [55]

    Saad, Martin C

    Feras A. Saad, Martin C. Rinard, and Vikash K. Mansinghka. 2021. SPPL: Probabilistic Programming with Fast Exact Symbolic Inference. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, New York, 804–819.https:/...

    2021

  47. [56]

    1978.Computational Geometry

    Michael Ian Shamos. 1978.Computational Geometry. Ph. D. Dissertation. Yale University

    1978

  48. [57]

    Alexei Sibidanov, Paul Zimmermann, and Stéphane Glondu. 2022. The CORE-MATH Project. InProceedings of the 2022 IEEE 29th Symposium on Computer Arithmetic. IEEE Press, Piscataway, 26–34.https://doi.org/10.1109/ARITH54963. 2022.00014

    2022

  49. [58]

    Sobolewski and W

    John S. Sobolewski and W. H. Payne. 1972. Pseudonoise with Arbitrary Amplitude Distribution–Part I: Theory.IEEE Trans. Comput.C-21, 4 (1972), 337–345.https://doi.org/10.1109/TC.1972.5008973

    1972

  50. [59]

    Jason Stover. 2003. GNU Scientific Library: Gamma Cumulative Distribution Function.https://github.com/ampl/gsl/ blob/v2.7.0/cdf/gamma.c

    2003

  51. [60]

    The MathWorks, Inc. 2024. Probability Distributions - MATLAB & Simulink.https://www.mathworks.com/help/ stats/probability-distributions-1.html

    2024

  52. [61]

    James Theiler and Brian Gough. 2007. GNU Scientific Library: Gamma Random Variate Generator.https://github. com/ampl/gsl/blob/v2.7.0/randist/gamma.c

    2007

  53. [62]

    Thomas and Wayne Luk

    David B. Thomas and Wayne Luk. 2008. Sampling from the Exponential Distribution Using Independent Bernoulli Variates. InProceedings of the 2008 International Conference on Field Programmable Logic and Applications. IEEE Press, Piscataway, 239–244.https://doi.org/10.1109/FPL.20...

    2008

  54. [63]

    Tomohiko Uyematsu and Yuan Li. 2003. Two Algorithms for Random Number Generation Implemented by Using Arithmetic of Limited Precision.IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences86, 10 (Oct. 2003), 2542–2551

    2003

  55. [64]

    Pauli Virtanen et al. 2020. SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python.Nature Methods17, 3 (Feb. 2020), 261–272.https://doi.org/10.1038/s41592-019-0686-2

    2020 doi

  56. [65]

    John von Neumann. 1951. Various Techniques Used in Connection with Random Digits. InMonte Carlo Method, A. S. Householder, G. E. Forsythe, and H. H. Germond (Eds.). National Bureau of Standards Applied Mathematics Series, Vol. 12. U. S. Government Printing Office, Washington, ...

    1951

  57. [66]

    Alistair J. Walker. 1974. Fast Generation of Uniformly Distributed Pseudorandom Numbers with Floating-Point Representation.Electronics Letters10, 25 (Dec. 1974), 533–534.https://doi.org/10.1049/el:19740423

    1974 doi

  58. [67]

    Michael Walter. 2019. Sampling the Integers with Low Relative Error. InProceedings of the 11th International Conference on Cryptology in Africa (Lecture Notes in Computer Science, Vol. 11627). Springer, Cham, 157–180.https://doi.org/10. 1007/978-3-030-23696-0_9

    2019

  59. [68]

    Abraham Ziv, Moshe Olshansky, Ealan Henis, and Anna Retiman. 2001. IBM Accurate Portable Mathlib.https: //github.com/dreal-deps/mathlib

    2001

  60. [69]

    midpoint

    Pedro Zuidberg Dos Martires, Anton Dries, and Luc De Raedt. 2019. Exact and Approximate Weighted Model Integration with Probability Density Functions Using Knowledge Compilation. InProceedings of the 23rd AAAI Conference on Artificial Intelligence. AAAI Press, Palo Alto, 7825–...

    2019 doi

  61. [70]

    Since 𝑧𝑗 = 0for all ℓ<𝑗<ℓ ′, we can apply Theorem 4.2 to ( ˆ𝑧, ˆ𝑥, ˆ𝑦,ℓ)

    This implies ˆ𝑧= ˆ𝑥+ ˆ𝑦 for ˆ𝑧 :=(𝑧 0.𝑧1...𝑧 ℓ′−10...) 2, ˆ𝑥 :=(𝑥 0.𝑥1...𝑥 ℓ′−10...) 2, and ˆ𝑦 := (𝑦0.𝑦1...𝑦 ℓ′−10...) 2. Since 𝑧𝑗 = 0for all ℓ<𝑗<ℓ ′, we can apply Theorem 4.2 to ( ˆ𝑧, ˆ𝑥, ˆ𝑦,ℓ) . In the theorem, only Pattern 4.2.1 matches because 𝑥ℓ𝑦ℓ𝑧ℓ∈{ 011, 101}. This yiel...

  62. [71]

    Also, all intermediate values appearing in both algorithms are representable as(1+𝐸+𝑚)-bit signed integers.« Proof.We prove the claims for𝑥<1and𝑥=1separately

    𝑏1...𝑏 1 𝑛1 bits 𝑔hi 𝑛hi bits 𝑏2...𝑏 2 𝑛2 bits 𝑔lo 𝑛lo bits 2 (5.9) and𝑏′ is theℓ-th digit of 𝑥− R𝑥′ in binary expansion. Also, all intermediate values appearing in both algorithms are representable as(1+𝐸+𝑚)-bit signed integers.« Proof.We prove the claims for𝑥<1and𝑥=1separate...

    2025

  63. [72]

    0 ... 0 𝑥 𝑥′ 𝑥−𝑥 ′ = 𝑓−𝑓 ′ hi 0 if𝑓 ′ lo =0 𝑓−𝑓 ′ hi−1 2 ˆ𝑒− ˆ𝑒′ −𝑓 ′ lo if𝑓 ′ lo >0 − ˆ𝑒−1bits z }| { 𝑓∈Z 𝑚+1bits z }| { | {z } − ˆ𝑒′−1bits | {z } (𝑚+1)−( ˆ𝑒− ˆ𝑒′)bits 𝑓′ hi∈Z | {z } ˆ𝑒− ˆ𝑒′ bits 𝑓′ lo∈Z | {z } − ˆ𝑒−1bits | {z } 𝑚+1bits | {z } ˆ𝑒− ˆ𝑒′ bits (D.8) Here, the equ...

  64. [73]

    0 ... 0 1 ... 1 𝑥 𝑥′ 𝑥−𝑥 ′ = 𝑓 0 if𝑓 ′ lo =0 𝑓−1 2𝑚+1−𝑓 ′ lo if𝑓 ′ lo >0 − ˆ𝑒−1bits z }| { 𝑓∈Z 𝑚+1bits z }| { | {z } − ˆ𝑒′−1bits | {z } 𝑚+1bits 𝑓′ lo∈Z | {z } − ˆ𝑒−1bits | {z } 𝑚+1bits | {z } ( ˆ𝑒− ˆ𝑒′)−(𝑚+1)bits | {z } 𝑚+1bits (D.9) Here, the equalities on𝑥,𝑥′,𝑓 is by the sam...

    2025

  65. [74]

    𝑔 hi 𝑛hi bits 𝑏2...𝑏 2 𝑛2 bits 𝑔lo 𝑛lo bits 2 (D.13) Since Algorithms 3–3 of Algorithm 3 compute(𝑛1,𝑛 hi)=( 0,𝑚) , the output of Algorithm 3 corre- sponds to the above equation. This implies that all the claims still hold for𝑥=1.□ Proposition D.1.If 𝑝 :=(𝑝 1,...,𝑝 𝑛−1,𝑝𝑛) and𝑝...

    2025

  66. [75]

    Also, all intermediate values appearing in both algorithms are representable as(1+𝐸+𝑚)-bit (signed or unsigned) integers.« Proof

    𝑏1...𝑏 1 | {z } 𝑛1 𝑔hi | {z } 𝑛hi 𝑏2...𝑏 2 | {z } 𝑛2 𝑔lo | {z } 𝑛lo 2 (E.9) and𝑏′ is theℓ-th digit of1 −(𝑥+𝑥 ′) in binary expansion. Also, all intermediate values appearing in both algorithms are representable as(1+𝐸+𝑚)-bit (signed or unsigned) integers.« Proof. By Algorithm E...

  67. [76]

    Here, the first inequality is by𝑥,𝑥′∈[ 0, 1 2), and we have the remaining equalities as in the proof of Theorem 5.16

    Then,( ˆ𝑒,𝑓) and( ˆ𝑒′,𝑓 ′) computed in Algorithms E11–E11 of Algorithm E11 satisfy ˆ𝑒, ˆ𝑒′≤−2, 𝑓=(𝑓 0...𝑓 𝑚)2, 𝑓 ′ =(𝑓 ′ 0 ...𝑓 ′ 𝑚)2, 𝑥=2 ˆ𝑒·(𝑓/2 𝑚), 𝑥 ′ =2 ˆ𝑒′ ·(𝑓 ′/2𝑚),(E.10) where𝑓0 := 1[𝑒> 0] and𝑓′ 0 := 1[𝑒′ > 0]. Here, the first inequality is by𝑥,𝑥′∈[ 0, 1 2), and we ha...

  68. [77]

    1 1 𝑥+𝑥 ′ 𝑓+𝑓 ′ hi 𝑓′ lo 1−(𝑥+𝑥 ′) = 2𝑚+2−(𝑓+𝑓 ′ hi) 0 if𝑓 ′ lo =0 2𝑚+2−(𝑓+𝑓 ′ hi)−1 2 ˆ𝑒− ˆ𝑒′ −𝑓 ′ lo if𝑓 ′ lo >0 | {z } − ˆ𝑒−2bits | {z } 𝑚+2bits | {z } ˆ𝑒− ˆ𝑒′ bits (E.12) Proc

    1 ... 1 1 𝑥+𝑥 ′ 𝑓+𝑓 ′ hi 𝑓′ lo 1−(𝑥+𝑥 ′) = 2𝑚+2−(𝑓+𝑓 ′ hi) 0 if𝑓 ′ lo =0 2𝑚+2−(𝑓+𝑓 ′ hi)−1 2 ˆ𝑒− ˆ𝑒′ −𝑓 ′ lo if𝑓 ′ lo >0 | {z } − ˆ𝑒−2bits | {z } 𝑚+2bits | {z } ˆ𝑒− ˆ𝑒′ bits (E.12) Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article 152. Publication date: June 2025. 152:48 Fer...

    2025

  69. [78]

    1 ... 1 1 ... 1 1 𝑥+𝑥 ′ 1−(𝑥+𝑥 ′) = 2𝑚+2−𝑓 0 if𝑓 ′ lo =0 2𝑚+2−𝑓−1 2𝑚+1−𝑓 ′ lo if𝑓 ′ lo >0 | {z } − ˆ𝑒−1bits | {z } 𝑚+1bits 𝑓∈Z | {z } ( ˆ𝑒− ˆ𝑒′)−(𝑚+1)bits | {z } 𝑚+1bits 𝑓′ lo∈Z | {z } − ˆ𝑒−2bits | {z } 𝑚+2bits | {z } ( ˆ𝑒− ˆ𝑒′)−(𝑚+1)bits | {z } 𝑚+1bits (E.13) Here, the equali...

  70. [79]

    Thus, 1−(𝑥+𝑥 ′)=0

    In this case, (E.12) and (E.13) still hold except that −ˆ𝑒− 2 =− 1is now less than0; and 𝑔hi < 2𝑚+1 holds since1−(𝑥+𝑥 ′)< 1(by assumption). Thus, 1−(𝑥+𝑥 ′)=0. 𝑔 hi | {z } 𝑚+1bits 𝑏2...𝑏 2 | {z } 𝑛2 bits 𝑔lo | {z } 𝑛lo bits .(E.14) Since Algorithms E11–E11 of Algorithm E11 comp...

  71. [80]

    ACM Program

    □ Proc. ACM Program. Lang., Vol. 9, No. PLDI, Article 152. Publication date: June 2025. Random Variate Generation with Formal Guarantees 152:49 Algorithm E9Quantile of a Finite-Precision CDF Input:CDF𝐹:{0,1} 𝑛→F 𝐸 𝑚∩[0,1]over number formatB=(𝑛,𝛾 B,𝜙 B) Float𝑞∈F 𝐸 𝑚∩[0,1] Outpu...

    2025

Pith tools

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