pith. sign in

arxiv: 2606.24514 · v1 · pith:VMNIUCOPnew · submitted 2026-06-23 · 💻 cs.SC · math.PR

Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition

Fredrik Dahlqvist , Mohamed Hamza Bandukara , Niki Omidvari This is my paper

Pith reviewed 2026-06-25 21:44 UTC · model grok-4.3

classification 💻 cs.SC math.PR
keywords probabilistic programscylindrical algebraic decompositionexact output distributionsensor data processingsymbolic integrationsemi-algebraic sets
0
0 comments X

The pith

A cylindrical algebraic decomposition method computes the exact output distribution of small programs with random inputs.

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

The paper shows how to obtain exact probability distributions for outputs of small programs processing random sensor data such as GPS or inertial measurements. These programs use few variables along with arithmetic operations, square roots, and if-else statements. The approach recasts the distribution task as a cylindrical algebraic decomposition of semi-algebraic sets, followed by symbolic or numerical integration over the resulting cells. A reader would care because the method replaces sampling approximations with precise results for programs where errors matter. Two prototypes confirm the technique works on floating-point benchmarks and open-source sensor code.

Core claim

We present a method for computing the exact output distribution of small programs with random inputs by recasting the problem as a cylindrical algebraic decomposition problem followed by symbolic and/or numerical integration. The method applies to programs whose syntax is limited to arithmetic, square roots, and conditionals over a modest number of variables, allowing the output probabilities to be recovered exactly rather than approximated.

What carries the argument

Cylindrical algebraic decomposition of the semi-algebraic sets defined by the program's arithmetic operations and conditional branches, followed by integration over the cells to recover the output density or cumulative distribution.

If this is right

  • Exact rather than approximate distributions become available for verification of small sensor-processing code.
  • Floating-point effects in probabilistic programs can be analyzed with symbolic precision on feasible instances.
  • Integration over CAD cells yields both densities and cumulative probabilities without Monte Carlo error.
  • The technique extends directly to programs drawn from open sensor libraries when variable counts stay low.

Where Pith is reading between the lines

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

  • Combining the method with program slicing could handle somewhat larger programs by isolating independent subexpressions.
  • The resulting exact distributions could serve as oracles to validate sampling-based probabilistic programming systems.
  • Extending the integration step to produce closed-form expressions where possible would increase usability for downstream analysis.

Load-bearing premise

The programs contain only a small number of variables and basic operations including square roots and conditionals, keeping the decomposition computationally feasible.

What would settle it

Apply the method to a program whose output distribution is known in closed form, such as the absolute value of a standard normal random variable, and check whether the computed distribution matches the folded normal exactly.

Figures

Figures reproduced from arXiv: 2606.24514 by Fredrik Dahlqvist, Mohamed Hamza Bandukara, Niki Omidvari.

Figure 1
Figure 1. Figure 1: Cylindrical Algebraic Decomposition (CAD) adapted to the unit disk. [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
read the original abstract

We present a method for computing the exact output distribution of small programs with random inputs. Specifically, we are interested in inline programs manipulating sensor data such as \eg GPS or inertial measurement sensors whose inputs have a known or well-modelled distribution. These programs typically only include relatively few variables, arithmetic operations, square roots and if-else statements. This small syntax allows us to recast the problem of computing the exact output distribution as a cylindrical algebraic decomposition problem followed by symbolic and/or numerical integration. We present this method in detail and show with two prototypes that it can successfully be applied to benchmarks from the literature on floating-point arithmetic and small programs from open-source sensor libraries.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims a method for exact output distribution computation of small probabilistic programs (few variables, arithmetic ops, square roots, if-else) by recasting program semantics as semi-algebraic sets, applying cylindrical algebraic decomposition (CAD) to decompose the input space, and then performing symbolic or numerical integration over the cells. Two prototypes are reported to succeed on literature benchmarks from floating-point analysis and open-source sensor libraries.

Significance. If the reduction holds, the work provides a sound exact alternative to Monte Carlo methods for a restricted but relevant class of programs arising in sensor data processing. It correctly exploits that the semantics induce semi-algebraic sets (after auxiliary variables for square roots), for which CAD yields an exact cell decomposition. Credit is due for the direct algorithmic reduction without fitted parameters and for the empirical demonstration on real benchmarks exercising the targeted size regime.

minor comments (2)
  1. The abstract and introduction would benefit from explicit mention of the number of variables and operations in the benchmark programs to substantiate the 'few variables' feasibility claim for CAD.
  2. Notation for the integration step over CAD cells could be clarified with a small worked example early in the method description.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; direct algorithmic reduction

full rationale

The paper's core claim is an algorithmic reduction: program semantics with arithmetic, square roots and conditionals induce semi-algebraic sets that CAD decomposes exactly, after which integration yields the output distribution. This is presented as a first-principles recasting rather than a fitted or self-referential construction. No equations define a quantity in terms of itself, no parameters are fitted on a subset and then relabeled as predictions, and no load-bearing uniqueness theorems or ansatzes are imported via self-citation. The prototypes exercise the method on external benchmarks, confirming the reduction is independently verifiable. The derivation chain therefore remains self-contained against external mathematical facts about CAD and semi-algebraic geometry.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract introduces no free parameters, no additional axioms beyond standard CAD theory, and no invented entities.

pith-pipeline@v0.9.1-grok · 5637 in / 1032 out tokens · 15015 ms · 2026-06-25T21:44:40.812444+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

40 extracted references · 6 canonical work pages

  1. [1]

    SIAM Journal on Computing13(4), 865–877 (1984)

    Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition i: The basic algorithm. SIAM Journal on Computing13(4), 865–877 (1984)

    1984

  2. [2]

    Springer (2006)

    Basu, S., Pollack, R., Roy, M.F.: Algorithms in real algebraic geometry. Springer (2006)

    2006

  3. [3]

    In: Proceedings of the 19th in- ternational conference on Tools and Algorithms for the Construction and Analysis of Systems

    Bhat, S., Borgström, J., Gordon, A.D., Russo, C.: Deriving probability density functions from probabilistic functional programs. In: Proceedings of the 19th in- ternational conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 508–522 (2013)

    2013

  4. [4]

    Computing94(2), 189–201 (2012)

    Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing94(2), 189–201 (2012)

    2012

  5. [5]

    In: International conference on tools and algorithms for the construc- tion and analysis of systems

    Bouissou, O., Goubault, E., Putot, S., Chakarov, A., Sankaranarayanan, S.: Uncer- tainty propagation using probabilistic affine forms and concentration of measure inequalities. In: International conference on tools and algorithms for the construc- tion and analysis of systems. pp. 225–243. Springer (2016)

    2016

  6. [6]

    SIGSAM Bull.37(4), 97–108 (Dec 2003)

    Brown, C.W.: Qepcad b: a program for computing with semi- algebraic sets using cads. SIGSAM Bull.37(4), 97–108 (Dec 2003). https://doi.org/10.1145/968708.968710, https://doi.org/10.1145/968708.968710

    work page doi:10.1145/968708.968710 2003

  7. [7]

    Presented at ISSAC 2004 (2004), available from https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf

    Brown, C.W.: Companion to the tutorial: Cylindrical Algebraic Decomposition. Presented at ISSAC 2004 (2004), available from https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf

    2004

  8. [8]

    In: International Symposium on Practical Aspects of Declarative Languages

    Carette, J., Shan, C.c.: Simplifying probabilistic programs using computer algebra. In: International Symposium on Practical Aspects of Declarative Languages. pp. 135–152. Springer (2016)

    2016

  9. [9]

    Choi, Y., Vergari, A., Van den Broeck, G.: Probabilistic circuits: A unifying frame- work for tractable probabilistic models. UCLA. URL: http://starai. cs. ucla. edu/- papers/ProbCirc20. pdf6(2020)

    2020

  10. [10]

    ACM SIGSAM Bulletin10(1), 10–12 (1976)

    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. ACM SIGSAM Bulletin10(1), 10–12 (1976)

    1976

  11. [11]

    Journal of Symbolic Computation12(3), 299–328 (1991)

    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation12(3), 299–328 (1991)

    1991

  12. [12]

    In: International Con- ference on Computer Aided Verification

    Constantinides, G., Dahlqvist, F., Rakamarić, Z., Salvia, R.: Rigorous roundoff error analysis of probabilistic floating-point computations. In: International Con- ference on Computer Aided Verification. pp. 626–650. Springer (2021)

    2021

  13. [13]

    ACM Transactions on Probabilistic Machine Learning1(3), 1–35 (2025)

    Constantinides, G., Dahlqvist, F., Rakamarić, Z., Salvia, R.: Automated roundoff error analysis of probabilistic floating-point computations. ACM Transactions on Probabilistic Machine Learning1(3), 1–35 (2025)

    2025

  14. [14]

    Naval Institute Press Annapolis (2004)

    Cutler, T.J.: Dutton’s Nautical Navigation. Naval Institute Press Annapolis (2004)

    2004

  15. [15]

    (2020) Exact Evaluation of Probabilistic Programs with CAD 21

    Dahlqvist, F., Silva, A., Kozen, D.: Semantics of probabilistic programming: A gentle introduction. (2020) Exact Evaluation of Probabilistic Programs with CAD 21

    2020

  16. [16]

    Damouche, N., Martel, M., Panchekha, P., Qiu, J., Sanchez-Stern, A., Tatlock, Z.: Toward a standard benchmark format and suite for floating-point analysis (July 2016)

    2016

  17. [17]

    Journal of the ACM (JACM)50(3), 280–305 (2003)

    Darwiche, A.: A differential approach to inference in bayesian networks. Journal of the ACM (JACM)50(3), 280–305 (2003)

    2003

  18. [18]

    Ferrenberg, A.M., Landau, D.P., Wong, Y.J.: Monte carlo simulations: Hidden errors from “good” random number generators. Phys. Rev. Lett. 69, 3382–3384 (Dec 1992). https://doi.org/10.1103/PhysRevLett.69.3382, https://link.aps.org/doi/10.1103/PhysRevLett.69.3382

    work page doi:10.1103/physrevlett.69.3382 1992

  19. [19]

    Proceedings of the ACM on Programming Languages8(PLDI), 865–888 (2024)

    Garg, P., Holtzen, S., Van den Broeck, G., Millstein, T.: Bit blasting probabilistic programs. Proceedings of the ACM on Programming Languages8(PLDI), 865–888 (2024)

    2024

  20. [20]

    In: International Conference on Computer Aided Verification

    Gehr, T., Misailovic, S., Vechev, M.: Psi: Exact symbolic inference for probabilistic programs. In: International Conference on Computer Aided Verification. pp. 62–83. Springer (2016)

    2016

  21. [21]

    In: Proceedings of the 41st acm sigplan conference on programming language design and implementation

    Gehr, T., Steffen, S., Vechev, M.:λpsi: exact inference for higher-order probabilistic programs. In: Proceedings of the 41st acm sigplan conference on programming language design and implementation. pp. 883–897 (2020)

    2020

  22. [22]

    Springer Science & Business Media (2003)

    Hofmann-Wellenhof, B., Legat, K., Wieser, M.: Navigation. Springer Science & Business Media (2003)

    2003

  23. [23]

    Proceedings of the ACM on Programming Languages 4(OOPSLA), 1–31 (2020)

    Holtzen, S., Van den Broeck, G., Millstein, T.: Scaling exact inference for dis- crete probabilistic programs. Proceedings of the ACM on Programming Languages 4(OOPSLA), 1–31 (2020)

    2020

  24. [24]

    SIAM Journal on Scientific Computing34(3), A1241–A1265 (Jan 2012)

    Jaroszewicz, S., Korzeń, M.: Arithmetic Operations on Independent Random Vari- ables: A Numerical Approach. SIAM Journal on Scientific Computing34(3), A1241–A1265 (Jan 2012). https://doi.org/10.1137/110839680

    work page doi:10.1137/110839680 2012

  25. [25]

    Journal of Statistical Software57, 1–34 (2014)

    Korzeń, M., Jaroszewicz, S.: Pacal: A python package for arithmetic computations with random variables. Journal of Statistical Software57, 1–34 (2014)

    2014

  26. [26]

    In: 20th Annual Symposium on Foundations of Computer Science (sfcs 1979)

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

    1979

  27. [27]

    In: International Conference on Integrated Formal Methods

    Lohar, D., Prokop, M., Darulova, E.: Sound probabilistic numerical error analysis. In: International Conference on Integrated Formal Methods. pp. 322–340. Springer (2019)

    2019

  28. [28]

    ACM Transactions on Mod- eling and Computer Simulation (TOMACS)8(1), 3–30 (1998)

    Matsumoto, M., Nishimura, T.: Mersenne twister: a 623-dimensionally equidis- tributed uniform pseudo-random number generator. ACM Transactions on Mod- eling and Computer Simulation (TOMACS)8(1), 3–30 (1998)

    1998

  29. [29]

    Chatterjee, T

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedi...

    work page doi:10.1007/978-3-540- 2008

  30. [30]

    In: International Symposium on Functional and Logic Programming

    Narayanan, P., Carette, J., Romano, W., Shan, C.c., Zinkov, R.: Probabilistic infer- ence by program transformation in hakaru (system description). In: International Symposium on Functional and Logic Programming. pp. 62–79. Springer (2016)

    2016

  31. [31]

    In: 2011 IEEE International Conference on Computer Vision Workshops (ICCV Work- shops)

    Poon, H., Domingos, P.: Sum-product networks: A new deep architecture. In: 2011 IEEE International Conference on Computer Vision Workshops (ICCV Work- shops). pp. 689–690. IEEE (2011) 22 Bandukara, Dahlqvist and Omidvari

    2011

  32. [32]

    In: Computer Algebra in Scientific Computing (CASC 2022)

    del Río, T., England, M.: New heuristic to choose a cylindrical algebraic decompo- sition variable ordering motivated by complexity analysis. In: Computer Algebra in Scientific Computing (CASC 2022). LNCS, vol. 13366, pp. 300–321. Springer (2022). https://doi.org/10.1007/978-3-031-14788-3_17

    work page doi:10.1007/978-3-031-14788-3_17 2022

  33. [33]

    In: Proceedings of the 42nd acm sigplan in- ternational conference on programming language design and implementation

    Saad, F.A., Rinard, M.C., Mansinghka, V.K.: Sppl: probabilistic programming with fast exact symbolic inference. In: Proceedings of the 42nd acm sigplan in- ternational conference on programming language design and implementation. pp. 804–819 (2021)

    2021

  34. [34]

    IEEE Transactions on Pattern Analysis and Machine Intelligence44(7), 3821–3839 (2021)

    Sánchez-Cauce, R., Paris, I., Díez, F.J.: Sum-product networks: A survey. IEEE Transactions on Pattern Analysis and Machine Intelligence44(7), 3821–3839 (2021)

    2021

  35. [35]

    Advances in Neural Information Processing Systems33, 17502–17513 (2020)

    Sankaranarayanan, S., Chou, Y., Goubault, E., Putot, S.: Reasoning about uncer- tainties in discrete-time dynamical systems using polynomial forms. Advances in Neural Information Processing Systems33, 17502–17513 (2020)

    2020

  36. [36]

    Journal of Navigation74(6), 1201–1218 (2021)

    Specht, M.: Consistency analysis of global positioning system position errors with typical statistical distributions. Journal of Navigation74(6), 1201–1218 (2021). https://doi.org/10.1017/S0373463321000485

    work page doi:10.1017/s0373463321000485 2021

  37. [37]

    New York: Wiley, (1979)

    Springer, M.D.: The algebra of random variables. New York: Wiley, (1979)

    1979

  38. [38]

    Journal of Sym- bolic Computation29(3), 471–480 (2000)

    Strzeboński, A.: Solving systems of strict polynomial inequalities. Journal of Sym- bolic Computation29(3), 471–480 (2000)

    2000

  39. [39]

    IEEE Transactions on Control Systems Technology26(2), 716–723 (2017)

    Wu,Y.,Zou,D.,Liu,P.,Yu,W.:Dynamicmagnetometercalibrationandalignment to inertial sensors by kalman filtering. IEEE Transactions on Control Systems Technology26(2), 716–723 (2017)

    2017

  40. [40]

    Electronics12(11) (2023) Exact Evaluation of Probabilistic Programs with CAD 23 Appendix Table 3: CDF and PDF of benchmarks vs

    Zheng, T., Xu, A., Xu, X., Liu, M.: Modeling and compensation of inertial sensor errors in measurement systems. Electronics12(11) (2023) Exact Evaluation of Probabilistic Programs with CAD 23 Appendix Table 3: CDF and PDF of benchmarks vs. empirical distribution (106 samples) T aylor approximations with uniform inputs CDF PDF ks=0.000965831 1.5 2.0 2.50.0...

    2023