REVIEW 4 major objections 6 minor 26 references
StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis
T0 review · 4 major / 6 minor · reviewed 2026-08-02 · deepseek-v4-flash
Pith's one-line read An open-source toolbox synthesizes stochastic barrier functions orders of magnitude faster than existing tools, with tighter safety bounds and support for higher-dimensional systems.
desk verdict A useful SBF synthesis toolbox whose headline performance claims are plausible, but the PWC guarantees rest on unverified transition-kernel bound computations. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
A stochastic barrier function (SBF) is a nonnegative function B satisfying three conditions: B(x) >= 1 outside the safe set, B(x) <= eta on the initial set, and E[B(f(x)+w)] <= B(x) + beta inside the safe set; these conditions guarantee safety probability P_s >= 1 - (eta + N*beta). The toolbox computes such a B via two routes: (i) sum-of-squares (SOS) optimization, where B is a polynomial and the conditions are enforced through semidefinite programming (Theorems 2.1 and 2.2); and (ii) piecewise-constant (PWC) synthesis, where the state space is partitioned into hyperrectangles, lower and upper bounds on the transition kernel between cells are computed (Eq. 7), and the cell values b_i are fou
What would settle it
For a simple 1D linear system with Gaussian noise, compute the exact transition probability from each grid cell to every other cell using numerical quadrature, and compare with the toolbox's reported lower and upper bounds; any violation invalidates the piecewise-constant safety guarantee.
Extended reading notes
Core claim
The paper presents StochasticBarrier.jl, a toolbox for synthesizing stochastic barrier functions for discrete-time stochastic systems with additive Gaussian noise. It implements two families of synthesis methods: sum-of-squares optimization for linear, polynomial, and piecewise-affine-bounded dynamics, and piecewise-constant barrier synthesis via dual linear programming, counterexample-guided inductive synthesis, and projected gradient descent. The central claim is empirical: across more than 30 benchmarks spanning systems of dimension one to six, the toolbox reports beating the two existing SBF-synthesis tools in computation time by up to four orders of magnitude, producing safety-probabili
Load-bearing premise
The piecewise-constant safety certificates rest entirely on the correctness of the computed lower and upper bounds on the transition kernel over each grid cell; if those bounds are not rigorous, the reported safety probability can be overestimated.
Editorial extensions
If this is right
- SBF synthesis becomes practical for higher-dimensional systems (up to six dimensions demonstrated) and for high-degree polynomial barriers, where prior tools ran out of memory or failed.
- Piecewise-constant synthesis provides non-trivial safety guarantees for non-polynomial systems such as a hybrid unicycle, where sum-of-squares methods return only a trivial safety probability of 0.
- Users can choose among engines: dual LP and CEGIS give the tightest probability bounds, while gradient descent scales to large partition counts while still returning sound (though not globally optimal) eta/beta values.
- The ability to save and load precomputed transition bounds lets users amortize the cost of probability computation across repeated safety analyses.
- If the reported speedups reproduce on other hardware, SBF-based verification can be embedded in interactive design loops or online monitoring for autonomous systems.
Reading between the lines
- In our reading, the soundness of the piecewise-constant certificates hinges on the transition kernel bound computation, which the paper does not independently verify; a formal proof or high-precision check of those bounds would close the main gap.
- The benchmark comparisons inherit differences in problem formulation across tools (for instance, how the safety probability is defined), so the reported margins may not hold on every problem instance; a neutral reimplementation would quantify that.
- The piecewise-constant machinery is, in principle, agnostic to the noise distribution, suggesting a natural extension beyond Gaussian additive noise to data-driven or non-Gaussian settings.
- The modular design—separate transition-bound computation and barrier-synthesis engines—should make the toolbox a convenient substrate for future SBF research, such as control synthesis or falsification.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents StochasticBarrier.jl, an open-source Julia toolbox for synthesizing stochastic barrier functions (SBFs) for discrete-time stochastic systems with additive Gaussian noise. The toolbox supports three classes of dynamics — linear, polynomial, and piecewise affine (PWA) inclusion — and three classes of barrier functions: SOS polynomials, piecewise constant (PWC) functions via dual linear programming, CEGIS, and gradient descent, and SOS for PWA inclusions. The authors benchmark against PRoTECT and StochasticBarrierFunctions across over 30 case studies, claiming orders-of-magnitude speedups, tighter safety probability bounds, and scalability to higher dimensions and higher-degree SOS barriers. The central claim is the engineering value of the toolbox rather than a new mathematical theorem; the theory is drawn from prior work [13, 14, 23].
Significance. If the claimed performance and correctness hold, StochasticBarrier.jl would be a valuable contribution: it is open-source, provides multiple synthesis engines, includes convenient NetCDF storage for transition probabilities, and appears to handle PWC barriers for nonlinear systems where SOS-based tools fail (e.g., the unicycle example in Fig. 2c). The paper explicitly positions itself as a toolbox paper, so the lack of new theorems is appropriate. However, the most load-bearing component — the computation of guaranteed interval bounds on the transition kernel in Eq. (7) — is not described, proved, or externally validated in this manuscript. The correctness of all PWC certificates, and hence the claimed safety-probability improvements, rests on this unverified step. The benchmark comparisons also contain unexplained numerical coincidences and lack variance information, which weakens the strength of the speed/scalability claims. These issues are fixable within the scope of a toolbox paper, but they must be addressed before the central claims can be accepted.
major comments (4)
- [§2.2.2 (Eq. 7) and §3.1.1] The PWC safety certificate in Theorem 2.3 depends on the values p_ij and p_ij_bar defined in Eq. (7) as exact infimum and supremum of the transition kernel over each partition cell. Section 3.1.1 states that transition_probabilities() computes these bounds, but no algorithm, numerical integration scheme, or error analysis is provided. For additive Gaussian noise and hyperrectangle partitions, the extrema of a Gaussian CDF over a box are not generally obtained by evaluating at corners; a naive sampling or interval-arithmetic implementation may fail to enclose the true range. If the bounds are not guaranteed, the LP/GD constraints in Theorem 2.3 are solved with invalid data, and the resulting P_s lower bound in Eq. (3) is not sound. This directly affects the headline advantages of the PWC engines, including the unicycle case where SOS returns zero. Please provide the precise algorithm used
- [Table 3 and Fig. 1] Several rows of Table 3 report numerically identical η, β, and P_s values for StochasticBarrier.jl and PRoTECT (e.g., Contraction Map 1 at degrees 2, 4, 8, 12: both give η=1.7e-2, β=1.8e-2, P_s=0.80; similar at degrees 24/30, and for Two Tank at degree 10/12). Given that PRoTECT is a separate Python implementation and the paper states its results are averaged over 10 random runs and that its P_s definition was adjusted, exact equality to the precision shown is implausible unless the two tools solve a mathematically identical program to machine precision. If the values are truly identical because the problem formulations coincide, state this explicitly; otherwise, the reported numbers may contain an error. This is load-bearing because the comparison is the evidence for the 'tightness of safety probability' claim. Please clarify the adjustment procedure for PRoTECT's P_s and provide the ac
- [§4 (Benchmark Studies) and §3.2.2] The runtime claims ('up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems') are based on single-run experiments, except for PRoTECT which is averaged over 10 runs. No confidence intervals, standard deviations, or multiple-seed results are reported for StochasticBarrier.jl's own methods, including the GD engine whose hyperparameters (initial_lr, decay, momentum, num_iterations) are user-specified and whose convergence is not guaranteed to a certified optimum. The comparison would be more convincing with repeated runs (at least for the GD and CEGIS methods) and a sensitivity analysis of the GD hyperparameters. Without this, the quantitative speedup factors in the abstract are not statistically supported.
- [§3.2.2 (Gradient Descent)] The text states that for the GD method, 'at termination, the values for η, β are guaranteed to be sound with respect to the returned barrier, although not absolutely optimal in the sense of Theorem 2.3.' This soundness claim is not proven here and is not obvious from the described minimax formulation: projected gradient descent converges to a stationary point under convexity, but the returned η and β must be verified to satisfy the safety constraints for the returned barrier over the continuous state space. Since the GD engine is one of the three PWC engines and is the fastest, the validity of its safety certificate is a load-bearing property. Please provide the verification step or a formal theorem (with proof or citation to a machine-checked proof) that the GD output constitutes a valid SBF.
minor comments (6)
- [References] Reference [15] (Data-Driven Permissible Safe Control) is listed with the same arXiv identifier (2404.16986) as reference [13] (Piecewise Stochastic Barrier Functions). This appears to be a citation error; please correct.
- [§3.1.3] The generation of PWA bounds using 'Linear Bound Propagation [29]' is mentioned but no details are given on how a user produces the NetCDF file. Since this is a required input for PWA systems, a brief description or a pointer to the associated script would improve usability.
- [Fig. 2] The legend ordering in some subfigures (e.g., (b) Pendulum) makes it hard to map colors to the PWC methods; consider using consistent line styles and adding markers or a table of values for clarity.
- [§4 and Appendix D] The sentence 'All methods use Mosek as the underlying SDP solver' is ambiguous for the LP-based PWC methods, which by default use HiGHS. Clarify that Mosek is used for SOS/SDP and HiGHS for LP.
- [Appendix B.1] In the 'Contraction Map 2' description, 'using the same distribution w ∼ N(0, 10^-2 I)' is unclear because the preceding contraction map also uses 10^-2. Specify whether the noise variance is identical or reduced.
- [Eq. (3)] The displayed lower bound after condition (2c) is not numbered in the text, yet later references to 'Eq. (3)' appear. Please add the equation number.
Circularity Check
No significant circularity: the toolbox's performance claims are empirical and benchmarked against external tools; the only notable dependency is unverified numerical bound computation, which is a soundness risk rather than a definitional circularity.
full rationale
The paper's central claims are engineering/empirical: it benchmarks StochasticBarrier.jl against the external tools PRoTECT [28] and StochasticBarrierFunctions [23], so the reported speedups and safety-probability improvements are measured against independent implementations, not derived from the paper's own assumptions. The theoretical backbone (SBF conditions Eq. (2)–(3), SOS reductions Theorem 2.1, and PWC optimization Theorem 2.3) is imported from published sources [23] and the authors' own prior work [13,14]; these citations are load-bearing for soundness but are not circular because the toolbox does not define the safety probability to be the optimization objective—it solves the stated feasibility conditions and reports the resulting bound. The most notable unverified dependency is in Section 3.1.1/Eq. (7): transition_probabilities() is said to compute infimum/supremum transition-kernel bounds, but no algorithm, proof, or external verification is provided. If those bounds are not rigorous, Theorem 2.3's certificates would be unsound; this is a correctness risk, not a circularity. No equation reduces to its own input, no fitted parameter is renamed as a prediction, and no uniqueness argument is imported from the authors' prior work. The self-citation cluster is real but does not force the benchmark conclusions.
Assumptions & free parameters
free parameters (3)
- PWC grid half-width / partition count |Q| =
Examples: 640, 225, 289, 361 (Contraction Map 2); 120/240/480 (Pendulum); 1250/1800 (Unicycle)
- GD hyperparameters (initial_lr=1e-2, decay=0.9999, momentum=0.9, num_iterations=10000) =
1e-2, 0.9999, 0.9, 10000
- SOS barrier/lagrange degrees =
barrier_degree 2-30; lagrange_degree=2
assumptions (5)
- standard math Theorem 2.1 (SOS-SBF for polynomial systems) from [23] is correct.
- domain assumption Theorem 2.2 (SOS-SBF for PWA inclusion dynamics) from [14] is correct.
- domain assumption Theorem 2.3 (PWC-SBF) from [13] is correct.
- domain assumption transition_probabilities() computes valid lower/upper bounds of the Gaussian transition kernel over each hyperrectangle (Eq. 7).
- domain assumption PWA inclusion bounds from Linear Bound Propagation [29] bound the true dynamics on each partition.
Cite this review
Pith. "Pith review of StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis." pith.science (2026). https://pith.science/paper/2BD6TJPL
@misc{pith2026260220359,
author = {Pith},
title = {Pith review of: StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis},
year = {2026},
howpublished = {\url{https://pith.science/paper/2BD6TJPL}},
note = {Machine review of arXiv:2602.20359}
}
read the original abstract
We present StochasticBarrier.jl, an open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise. StochasticBarrier.jl certifies linear, polynomial, and piecewise affine (PWA) systems. The latter enables verification for a wide range of system dynamics, including general nonlinear types. The toolbox implements a Sum-of-Squares (SOS) optimization approach, as well as methods based on piecewise constant (PWC) functions. For SOS-based SBFs, StochasticBarrier.jl leverages semi-definite programming solvers, while for PWC SBFs, it offers three engines: two using linear programming (LP) and one based on gradient descent (GD). Benchmarking StochasticBarrier.jl against the state-of-the-art shows that the tool outperforms existing tools in computation time, safety probability bounds, and scalability across over 30 case studies. Compared to its closest competitor, StochasticBarrier.jl is up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems.
Figures
Reference graph
Works this paper leans on
-
[1]
A., Cauchi, N., Delicaris, J., Hartmanns, A., Khaled, M., Lavaei, A., Pilch, C., Remke, A., Schupp, S., et al.Arch-comp20 category report: Stochastic models
Abate, A., Blom, H. A., Cauchi, N., Delicaris, J., Hartmanns, A., Khaled, M., Lavaei, A., Pilch, C., Remke, A., Schupp, S., et al.Arch-comp20 category report: Stochastic models. InARCH(2020)
2020
-
[2]
ApS, M.Mosek optimization toolbox for matlab.User’s Guide and Reference Manual, Version 4, 1 (2019)
2019
-
[3]
P., and Shreve, S
Bertsekas, D. P., and Shreve, S. E.Stochastic Optimal Control: the Discrete-time Case, vol. 5. Athena Scientific, 2004
2004
-
[4]
InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control(2019), pp
Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., and Schilling, C.Ju- liareach: a toolbox for set-based reachability. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control(2019), pp. 39–44
2019
-
[5]
Coleman, C., Lyon, S., Maliar, L., and Maliar, S.Matlab, python, julia: What to choose in economics?Computational Economics 58(2021), 1263–1288
2021
-
[6]
Forets, M., and Schilling, C.LazySets.jl: Scalable Symbolic-Numeric Set Computations.Proceedings of the JuliaCon Conferences 1, 1 (2021), 11
2021
-
[7]
J.Parallelizing the dual revised simplex method
Huangfu, Q., and Hall, J. J.Parallelizing the dual revised simplex method. Mathematical Programming Computation 10, 1 (2018), 119–142
2018
-
[8]
[9]Legat, B.Multivariate polynomials in Julia
Jagtap, P., Soudjani, S., and Zamani, M.Formal synthesis of stochastic systems via control barrier certificates.IEEE Transactions on Automatic Control 66, 7 (2020), 3097–3110. [9]Legat, B.Multivariate polynomials in Julia. InJuliaCon(July 2022)
2020
Show all 26 references
-
[10]
P.JuMP 1.0: Recent improvements to a modeling language for mathematical optimization.Mathematical Programming Computation(2023)
Lubin, M., Dowson, O., Dias Garcia, J., Huchette, J., Legat, B., and Vielma, J. P.JuMP 1.0: Recent improvements to a modeling language for mathematical optimization.Mathematical Programming Computation(2023)
2023
-
[11]
B., Lahijanian, M., and Laurenti, L.IntervalMDP
Mathiesen, F. B., Lahijanian, M., and Laurenti, L.IntervalMDP. jl: Accel- erated Value Iteration for Interval Markov Decision Processes.arXiv preprint arXiv:2401.04068(2024)
2024 arXiv
-
[12]
B., Romao, L., Calvert, S
Mathiesen, F. B., Romao, L., Calvert, S. C., Laurenti, L., and Abate, A.A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution.arXiv preprint arXiv:2410.06662(2024)
2024 arXiv
-
[14]
Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions.Advances in Neural Information Processing Systems(2022)
Mazouz, R., Muvvala, K., Ratheesh, A., Laurenti, L., and Lahijanian, M. Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions.Advances in Neural Information Processing Systems(2022)
2022
-
[15]
B., Frew, E., Laurenti, L., and Lahija- nian, M.Data-Driven Permissible Safe Control with Barrier Certificates.arXiv preprint arXiv:2404.16986(2024)
Mazouz, R., Skovbekk, J., Mathiesen, F. B., Frew, E., Laurenti, L., and Lahija- nian, M.Data-Driven Permissible Safe Control with Barrier Certificates.arXiv preprint arXiv:2404.16986(2024)
2024 arXiv
-
[16]
Nejati, A., Soudjani, S., and Zamani, M.Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems.European Journal of Control 57(2021), 82–94
2021
-
[17]
M., et al.Julia: come for the syntax, stay for the speed.Nature 572, 7767 (2019), 141–142
Perkel, J. M., et al.Julia: come for the syntax, stay for the speed.Nature 572, 7767 (2019), 141–142
2019
-
[18]
Prajna, S.Barrier certificates for nonlinear model validation.Automatica 42, 1 (2006), 117–126
2006
-
[19]
J.A framework for worst-case and stochastic safety verification using barrier certificates.IEEE Transactions on Automatic Control 52, 8 (2007)
Prajna, S., Jadbabaie, A., and Pappas, G. J.A framework for worst-case and stochastic safety verification using barrier certificates.IEEE Transactions on Automatic Control 52, 8 (2007)
2007
-
[20]
A.Introducing SOSTOOLS: A General Purpose Sum of Squares Programming Solver
Prajna, S., Papachristodoulou, A., and Parrilo, P. A.Introducing SOSTOOLS: A General Purpose Sum of Squares Programming Solver. InConference on Decision and Control(2002), vol. 1, IEEE
2002
-
[21]
A., and Dos Santos, P
Ramos, J. A., and Dos Santos, P. L.Mathematical modeling, system identification, and controller design of a two tank system. In2007 46th IEEE Conference on Decision and Control(2007), IEEE
2007
-
[22]
Rew, R., and Davis, G.Netcdf: an interface for scientific data access.IEEE computer graphics and applications 10, 4 (1990)
1990
-
[23]
[24]Schneeberger, M., Dörfler, F., and Mastellone, S.Sos construction of com- patible control lyapunov and barrier functions.IFAC-PapersOnLine 56, 2 (2023), 10428–10434
Santoyo, C., Dutreix, M., and Coogan, S.A barrier function approach to finite-time stochastic system verification and control.Automatica 125(2021). [24]Schneeberger, M., Dörfler, F., and Mastellone, S.Sos construction of com- patible control lyapunov and barrier functions.IFAC...
2021
-
[25]
J., and Lall, S.Satisfiability
Soroka, E., Kochenderfer, M. J., and Lall, S.Satisfiability. jl: Satisfiability modulo theories in julia.preprint arXiv:2309.08778(2023)
2023 arXiv
-
[26]
In2018 Annual American Control Conference (ACC)(2018), IEEE, pp
W ang, L., Han, D., and Egerstedt, M.Permissive barrier certificates for safe stabilization using sum-of-squares. In2018 Annual American Control Conference (ACC)(2018), IEEE, pp. 585–590
2018
-
[27]
S., Hu, H., Niu, P., Luo, X., and Liu, C.Modelveri- fication
Wei, T., Marzari, L., Yun, K. S., Hu, H., Niu, P., Luo, X., and Liu, C.Modelveri- fication. jl: a comprehensive toolbox for formally verifying deep neural networks. arXiv preprint arXiv:2407.01639(2024)
2024 arXiv
-
[28]
Wooding, B., Horbanov, V., and Lavaei, A.Protect: Parallelized construction of safety barrier certificates for nonlinear polynomial systems.arXiv preprint arXiv:2404.14804(2024)
2024 arXiv
-
[29]
linear
Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., and Daniel, L.Efficient neural network robustness certification with general activation functions.Advances in neural information processing systems 31(2018). A Benchmarking Setup StochasticBarrier.jl is also equipped with an i...
2018
Reviewed August 2, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.