Pith. sign in

REVIEW 2 major objections 5 minor 90 references

Formal Verification of Markov Processes with Learned Parameters

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

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

Pith's one-line read Formal verification of Markov processes with ML-learned parameters reduces to a mixed-integer bilinear program, solvable to global optimality by a decomposition and bound-propagation scheme that is orders of magnitude faster than direct…

desk verdict Useful new problem class and a sound bound-propagation scheme for the exact-MILP core, but the 'formal' guarantee is overclaimed for the logistic/softmax models actually used in the experiments. read the letter →

arxiv 2501.15767 v2 pith:DV6XASYM submitted 2025-01-27 cs.LG cs.AImath.OC

Muhammad Maaz , Timothy C. Y. Chan This is my paper · ORCID
classification cs.LGcs.AImath.OC MSC 90C2690C1160J10
keywords formalverificationMarkovchainsmachinelearningbilinearprogrammingboundpropagationintervalGauss-Seidelglobaloptimizationmarkovml
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

Markov chains used in high-stakes settings increasingly take their transition probabilities and rewards from machine-learning models, but proving worst-case properties of the resulting system has been out of reach. The paper claims that reachability, expected hitting time, and total discounted reward for such chains can be formulated as one mixed-integer bilinear program, and that a decomposition scheme—bound each ML output with small MILPs, propagate bounds through the affine parameter maps, then tighten value-function bounds with interval Gauss-Seidel—makes the program tractable to global optimality. In numerical experiments the method solves instances orders of magnitude faster than direct bilinear solving, with the gap growing with model complexity, and it is packaged in an open-source tool called markovml. If the claim holds, it turns formal verification of ML-parameterized Markov processes from a Monte Carlo approximation into an exact optimization problem.

What carries the argument

The load-bearing mechanism is a four-stage bound-propagation decomposition of the bilinear program. Stage one solves $2\ell$ small MILPs to bound each component of the ML output $\theta$ over the feature set $X$; stage two pushes these intervals through the affine maps $\pi = A_\pi\theta + b_\pi$, $\mathrm{vec}(P) = A_P\theta + b_P$, $r = A_r\theta + b_r$ using Lemma 4.1; stage three exploits the fact that every row of $(I-\lambda P)^{-1}$ sums to $1/(1-\lambda)$ to get initial bounds on the value vector $v$; stage four runs interval Gauss-Seidel on the linear system $(I-\lambda P)v = r$, which is guaranteed by Theorem 4.4 to return the tightest rectangular enclosure (the hull) exactly when the upper-bound transition matrix satisfies $\rho(P_{\max}) \le 1/\lambda$. These bounds are then added as constraints to the original bilinear program, and any out-of-the-box global solver finishes the job.

What would settle it

Run markovml on a two-state Markov reward process whose transition probability is a logistic regression in one feature $x \in [0,1]$ with a fixed reward vector, and compare its claimed global minimum of total discounted reward against an independent dense scan of $x$ using the closed-form value $\pi^\top(I-\lambda P(x))^{-1}r$; if the scan finds a strictly better objective than the certified optimum by more than the solver tolerance, the global-optimality claim for nonlinear models is false.

Watch

Extended reading notes

Core claim

The central claim is that formal verification of Markov processes whose parameters are outputs of ML models is a solvable optimization problem: for linear models, tree ensembles, and ReLU networks, computing the worst- or best-case reachability probability, hitting time, or total reward can be written as a mixed-integer bilinear program. The paper's method solves that program by first bounding each ML output through small MILPs, propagating the resulting intervals through the affine equalities that define $\pi$, $P$, and $r$, deriving initial value-function bounds from the Markov structure via $(I-\lambda P)^{-1}$, and tightening those bounds with interval Gauss-Seidel. The final bilinear program with the propagated bounds is passed to a global solver, so the result is a certificate of the extremal property, not a simulation estimate. The paper reports that this pipeline solves to global optimality with speedups ranging from tens to roughly a thousand times over direct solving, and demonstrates the pipeline on a cardiac-arrest cost-effectiveness model.

Load-bearing premise

Everything stands on the assumption that each ML model's input-output relation can be exactly encoded with linear constraints and binary variables; for logistic and softmax models, which cannot, the paper relies on the numerical global solver's spatial branch-and-bound, so the formal guarantee for those models is only as strong as that numerical solve.

Editorial extensions

If this is right

  • Worst-case and best-case answers to reachability, hitting time, and total discounted reward become provable for Markov chains whose parameters come from linear models, tree ensembles, and small ReLU networks, rather than approximated by Monte Carlo.
  • The same pipeline handles optimization and feasibility versions, so threshold questions—such as whether the worst-case failure probability stays below a bound—become exact yes-or-no checks.
  • The speedup over direct bilinear solving grows with model complexity: about 100x for deep trees, sometimes over 1000x, and neural-network instances that time out for direct solving are solved by the decomposition.
  • Because the final optimization still runs on an out-of-the-box global solver, future improvements in bilinear or MILP solvers should translate directly into faster verification.

Reading between the lines

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

  • The $\theta$-bounding stage is independent of the Markov chain, so plugging in stronger neural-network verifiers—for example, better branch-and-bound for ReLU networks—should tighten bounds and extend scalability to deeper architectures, a direction the paper itself flags.
  • The spectral-radius condition in Theorem 4.4 doubles as a predictability diagnostic: instances with $\rho(P_{\max}) > 1/\lambda$ are exactly the ones where interval Gauss-Seidel may not reach the hull, so users could estimate in advance which verification problems will be hard.
  • For logistic regression and softmax classifiers, the exact MILP-representability assumption is not met; the formal guarantee is then inherited from the numerical global solver, so the strongest formal statement should be scoped to piecewise-linear models, with nonlinear models carrying a numerical-global certificate.
  • The framework suggests a natural extension to subgroup certification: since bounds on $\theta$ and $v$ are cheap, one could search over feature regions to certify performance across a whole subgroup without enumerating patients.
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

2 major / 5 minor

Summary. The paper introduces a framework for formally verifying properties of finite-state Markov chains whose transition probabilities, initial distribution, and rewards are determined by machine learning models. The verification task (reachability, hitting time, total discounted reward) is cast as a mixed-integer bilinear program under an assumption that each ML model is MILP-representable. The paper's main algorithmic contribution is a decomposition and bound-propagation scheme: compute elementwise bounds on the learned outputs by solving small MILPs, propagate these to π, P, and r via affine equalities, derive coarse bounds on the value function v using Markov-chain theory, tighten those bounds with interval Gauss-Seidel, and then solve the original bilinear program with an off-the-shelf global solver, using the propagated bounds as constraints. Experiments on synthetic instances compare this approach with direct solving, reporting large speedups and better scaling with state count, model count, tree depth, and neural-network width, and a case study applies the method to a cardiac-arrest cost-effectiveness model with a tree-based discharge classifier. The paper releases an open-source Python package, markovml, and scripts to reproduce the experiments.

Significance. If scoped appropriately, this is a useful and timely contribution: the idea of embedding learned parameters directly into an optimization formulation for Markov-chain verification is natural but nontrivial, and the decomposition into small MILPs plus interval linear-system tightening is a practically effective way to accelerate global optimization. The theoretical core for exactly MILP-representable models (trees, ReLU networks without softmax, and linear models) is sound: Lemma 4.1 propagates interval bounds correctly, Lemma 4.3 gives valid value-function bounds, and Theorem 4.4 provides a clean condition for the interval-Gauss-Seidel hull property. The reported speedups for decision-tree instances (tens to hundreds of times, with a 1000x speedup on some instances) are substantial, and the ablation in Table 1 isolates the contribution of the v-bounds. The release of documented code (markovml) and reproducible experimental scripts is a genuine strength. However, the paper's headline claims of 'formal verification' and 'global optimality' over 'a broad class of machine learning models, including ...

major comments (2)
  1. [Section 3.1, Section 4, Appendix G] The core theoretical framework is conditional on the assumption that every f_i is MILP-representable, but the experimental evaluation uses logistic regression (Experiments 1 and 2) and softmax-based classifiers (Experiment 4 and the torch support in Section 5), which do not satisfy this assumption. Section 3.1 itself acknowledges that logistic and softmax functions are handled 'using Gurobi’s built-in spatial branch-and-bound techniques for nonlinear functions – essentially dynamic piecewise linear approximations.' A finite MILP cannot exactly encode a transcendental function, and the bounds on θ computed in Section 4 are therefore not certified lower/upper bounds for these models. Consequently, the propagated bounds on π, P, r, and v are not formally valid for these instances, and the abstract's claim that the method 'solves the problem to global optimality' is not established for exactly the model classes used in the headline experiments. The fix is to restrict the formal claims (abstract, introduction, Section 4) to exactly MILP-representable models, and to either re-run the affected experiments with such models, remove them from the formal-claim experiments, or provide a rigorous analysis of the spatial-branch-and-bound tolerances and their effect on the final optimum.
  2. [Appendix F.2, Section 5] The statement that the authors 'implemented the MILP formulation ourselves' for softmax is misleading: a piecewise-linear approximation of softmax encoded with binary variables is not an exact MILP representation. Unless the paper provides a certified error bound for this approximation (e.g., a formal statement of how the piecewise approximation relates to the true softmax, with a guarantee that the final objective value is bracketed within a stated tolerance), the results for softmax-based networks should be presented as numerical or approximate, not as exact formal verification. This is not a mere presentational point; it determines whether the advertised 'formal guarantees' hold for a large portion of the supported model zoo.
minor comments (5)
  1. [Section 3.1] The sentence listing 'linear and logistic regression' among MILP-representable functions is inaccurate, and the paper's own caveat immediately below contradicts it. Rephrase to avoid implying that logistic regression is exactly encoded by a finite MILP.
  2. [Definition 3.2] There is a duplicated phrase: 'from a set T ⊆ [n] of transient states from a set T ⊆ [n] of transient states equal to the complement of S.' Remove the repetition.
  3. [Section 6.1 and Appendix G] The runtime comparison reclassifies suboptimal solver statuses as 'optimal' when the objectives agree to 1e-12. This is disclosed, but it conflates cases where the direct solver proved optimality with cases where it only found a feasible solution with the same objective. Please report the runtime comparison separately for instances where Gurobi proved optimality, and present the reclassified analysis only as a sensitivity check.
  4. [Figure 2] The error bars are described as 'standard deviation' of geometric means, but the multiplier-based display is ambiguous. State explicitly whether the standard deviation is computed on log-transformed runtimes and whether the bars are multiplicative (e.g., geometric mean times division by the geometric standard deviation).
  5. [Checklist, Item 2] The NeurIPS checklist item on Limitations is left as '[TODO]' in the submitted manuscript. Please complete it and include a discussion of the MILP-representability scope in the Limitations section of the main text.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the verification pipeline is self-contained and the claims are conditional on an external global solver.

full rationale

The paper's derivation chain is non-circular. It defines the verification problem as a bilinear program (Section 3), proves valid bound-propagation lemmas for theta, pi, P, r, and v (Section 4 and Appendices B-D), and then delegates the final global-optimality step to an out-of-the-box solver, explicitly stating that the method is exact if the underlying bilinear solver is exact (Section 4.2). The speedup claims are empirical comparisons against direct Gurobi solving on generated instances, not quantities fitted from the target outputs. The only self-citations are [30] in Related Work as context and [59] in the case study as an input model/data source; neither is used to justify the central correctness or performance claims. The acknowledged gap between the MILP-representability assumption and the practical use of Gurobi's spatial branch-and-bound for logistic/softmax functions is a validity or scope limitation for the formal guarantee, not a circular reduction: the paper itself flags the assumption and the approximate numerical handling. The unfinished NeurIPS checklist TODO entries are a completeness artifact rather than evidence of circularity. Overall, no step in the derivation reduces, by construction or by self-citation, to its own inputs.

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

The method is largely self-contained, but it depends on two domain assumptions: exact MILP encodings of the ML models and a global solver as an oracle for the final optimization. The experimental implementation also imports a hand-set epsilon for strict substochasticity and a tolerance for reclassifying direct-solver outcomes. No unobserved physical entities are introduced; markovml is software, not a postulated entity.

free parameters (3)
  • strict substochastic offset epsilon = 1e-6 (software default)
    Chosen by hand to replace strict inequalities in the reachability and hitting time formulations; alpha = 1 - epsilon defines the initial value bounds.
  • discount factor lambda = 0.97 in all reported experiments
    Experiment configuration from Appendix G, not derived; it affects bound tightness and runtime comparisons.
  • optimality tolerance for reclassifying suboptimal runs = 1e-12 objective difference
    Chosen in Appendix G; direct-method suboptimal instances were counted as optimal for runtime statistics when the objective matched the proposed method to this tolerance, which can affect reported speedups.
assumptions (6)
  • standard math The verification properties reachability, hitting time, and discounted total reward are given by the linear-system formulas in Definitions 3.1 through 3.3.
    These are standard Markov chain results and are the foundation of the optimization formulation.
  • domain assumption Each ML model f_i is MILP-representable over the feature set X.
    Stated in Section 3.1; this is what makes the master problem a mixed-integer bilinear program. Logistic and softmax models in the implementation violate exact MILP representability and are handled by Gurobi spatial branch-and-bound.
  • domain assumption The parameters pi, vec(P), and r are affine functions of the model output vector theta.
    Stated in Section 3.1; this restricts the linking layer between ML outputs and Markov parameters.
  • domain assumption The feature set X is a finite union of polyhedra, i.e., MILP-representable.
    Stated in Section 3.1; needed for the bound MILPs over x.
  • standard math Interval Gauss-Seidel returns the hull for interval M-matrices, per the cited interval analysis literature.
    Used in Section 4.1 to tighten value bounds; accepted background result from Neumaier and related references.
  • domain assumption The final global solver, Gurobi in the experiments, proves global optimality of the bounded bilinear program.
    Section 4.2 delegates global optimality to the underlying solver; for nonlinear logistic and softmax constraints this relies on numerical spatial branch-and-bound tolerances.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Verification of Markov Processes with Learned Parameters." pith.science (2026). https://pith.science/paper/DV6XASYM

@misc{pith2026250115767,
  author       = {Pith},
  title        = {Pith review of: Formal Verification of Markov Processes with Learned Parameters},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DV6XASYM}},
  note         = {Machine review of arXiv:2501.15767}
}
read the original abstract

We introduce the problem of formally verifying properties of Markov processes where the parameters are given by the output of machine learning models. For a broad class of machine learning models, including linear models, tree-based models, and neural networks, verifying properties of Markov chains like reachability, hitting time, and total reward can be formulated as a bilinear program. We develop a decomposition and bound propagation scheme for solving the bilinear program and show through computational experiments that our method solves the problem to global optimality up to 100x faster than state-of-the-art solvers. To demonstrate the practical utility of our approach, we apply it to a real-world healthcare case study. Along with the paper, we release markovml, an open-source tool for building Markov processes, integrating pretrained machine learning models, and verifying their properties, available at https://github.com/mmaaz-git/markovml.

Figures

Figures reproduced from arXiv: 2501.15767 by the authors.

Figure 1
Figure 1. Example of our pipeline. A feature vector [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Runtimes of our method versus direct solving. Each panel shows results from experiments [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Proportion (%) of instances categorized as optimal, suboptimal, timed out, or other. Each [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

90 extracted references · 74 canonical work pages

  1. [1]

    Introduction to the numerical solution of markov chains

    William J Stewart. Introduction to the numerical solution of markov chains. 2021

    2021

  2. [2]

    Principles of model checking

    Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008

    2008

  3. [3]

    System reliability theory: models, statistical methods, and applications, volume 396

    Marvin Rausand and Arnljot Hoyland. System reliability theory: models, statistical methods, and applications, volume 396. John Wiley & Sons, 2003

    2003

  4. [4]

    Markov models in medical decision making: a practical guide

    Frank A Sonnenberg and J Robert Beck. Markov models in medical decision making: a practical guide. Medical decision making, 13(4):322–338, 1993

    1993

  5. [5]

    Microsimulation modeling in food policy: A scoping review of methodological aspects

    Elly Mertens, Els Genbrugge, Junior Ocira, and José L Peñalvo. Microsimulation modeling in food policy: A scoping review of methodological aspects. Advances in Nutrition, 13(2): 621–632, 2022

    2022

  6. [6]

    Microsimulation modeling for health decision sciences using r: a tutorial

    Eline M Krijkamp, Fernando Alarid-Escudero, Eva A Enns, Hawre J Jalal, MG Myriam Hunink, and Petros Pechlivanoglou. Microsimulation modeling for health decision sciences using r: a tutorial. Medical Decision Making, 38(3):400–422, 2018

    2018

  7. [7]

    A logic for reasoning about time and reliability

    Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal aspects of computing, 6:512–535, 1994

    1994

  8. [8]

    Prism: Probabilistic symbolic model checker

    Marta Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. In International Conference on Modelling Techniques and Tools for Computer Perfor- mance Evaluation, pages 200–204. Springer, 2002

    2002

Show all 90 references
  1. [9]

    A markov reward model checker

    J-P Katoen, Maneesh Khattri, and IS Zapreevt. A markov reward model checker. In Second International Conference on the Quantitative Evaluation of Systems (QEST’05), pages 243–244. IEEE, 2005

    2005

  2. [10]

    A markov chain model checker

    Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. A markov chain model checker. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 347–362. Springer, 2000

    2000

  3. [11]

    On statistical model checking of stochastic systems

    Koushik Sen, Mahesh Viswanathan, and Gul Agha. On statistical model checking of stochastic systems. In Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings 17, pages 266–280. Springer, 2005

    2005

  4. [12]

    Ymer: A statistical model checker

    Håkan LS Younes. Ymer: A statistical model checker. InInternational Conference on Computer Aided Verification, pages 429–433. Springer, 2005

    2005

  5. [13]

    Approximate verification of probabilistic systems

    Richard Lassaigne and Sylvain Peyronnet. Approximate verification of probabilistic systems. In Joint International Workshop von Process Algebra and Probabilistic Methods, Performance Modeling and Verification, pages 213–214. Springer, 2002

    2002

  6. [14]

    Model-checking markov chains in the presence of uncertainties

    Koushik Sen, Mahesh Viswanathan, and Gul Agha. Model-checking markov chains in the presence of uncertainties. In Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theo...

    2006

  7. [15]

    Parameter synthesis for parametric interval markov chains

    Benoît Delahaye, Didier Lime, and Laure Petrucci. Parameter synthesis for parametric interval markov chains. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 372–390. Springer, 2015

    2015

  8. [16]

    Parameter synthesis algorithms for parametric interval markov chains

    Laure Petrucci and Jaco van De Pol. Parameter synthesis algorithms for parametric interval markov chains. In International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pages 121–140. Springer, 2018

    2018

  9. [17]

    Model repair for markov decision processes

    Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model repair for markov decision processes. In 2013 International Symposium on Theoretical Aspects of Software Engineering, pages 85–92. IEEE, 2013. 10

    2013

  10. [18]

    Parameter synthesis in Markov models

    Sebastian Junges. Parameter synthesis in Markov models. PhD thesis, Dissertation, RWTH Aachen University, 2020, 2020

    2020

  11. [19]

    Parameter synthesis for markov models: covering the parameter space

    Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias V olk. Parameter synthesis for markov models: covering the parameter space. Formal Methods in System Design, 62(1):181–259, 2024

    2024

  12. [20]

    Efficient sensitivity analysis for parametric robust markov chains

    Thom Badings, Sebastian Junges, Ahmadreza Marandi, Ufuk Topcu, and Nils Jansen. Efficient sensitivity analysis for parametric robust markov chains. In International Conference on Computer Aided Verification, pages 62–85. Springer, 2023

    2023

  13. [21]

    On markov chains with uncertain data

    Hans Blanc and Dick Den Hertog. On markov chains with uncertain data. 2008

    2008

  14. [22]

    Sensitivity analysis for finite markov chains in discrete time

    Gert De Cooman, Filip Hermans, and Erik Quaeghebeur. Sensitivity analysis for finite markov chains in discrete time. arXiv preprint arXiv:1408.2029, 2014

    2014 arXiv

  15. [23]

    Simulation-based optimization of markov reward processes

    Peter Marbach and John N Tsitsiklis. Simulation-based optimization of markov reward processes. IEEE Transactions on Automatic Control, 46(2):191–209, 2001

    2001

  16. [24]

    Approximate gradient methods in policy-space optimiza- tion of markov reward processes

    Peter Marbach and John N Tsitsiklis. Approximate gradient methods in policy-space optimiza- tion of markov reward processes. Discrete Event Dynamic Systems, 13:111–148, 2003

    2003

  17. [25]

    Robust solutions to markov decision problems with uncertain transition matrices

    Laurent El Ghaoui and Arnab Nilim. Robust solutions to markov decision problems with uncertain transition matrices. Operations Research, 53(5):780–798, 2005

    2005

  18. [26]

    Robust dynamic programming

    Garud N Iyengar. Robust dynamic programming. Mathematics of Operations Research, 30(2): 257–280, 2005

    2005

  19. [27]

    Robust markov decision processes: Beyond rectangu- larity

    Vineet Goyal and Julien Grand-Clement. Robust markov decision processes: Beyond rectangu- larity. Mathematics of Operations Research, 48(1):203–226, 2023

    2023

  20. [28]

    On the convex formulations of robust markov decision processes

    Julien Grand-Clément and Marek Petrik. On the convex formulations of robust markov decision processes. Mathematics of Operations Research, 2024

    2024

  21. [29]

    Data un- certainty in markov chains: Application to cost-effectiveness analyses of medical innovations

    Joel Goh, Mohsen Bayati, Stefanos A Zenios, Sundeep Singh, and David Moore. Data un- certainty in markov chains: Application to cost-effectiveness analyses of medical innovations. Operations Research, 66(3):697–715, 2018

    2018

  22. [30]

    Exact sensitivity analysis of markov reward processes via algebraic geometry

    Timothy CY Chan and Muhammad Maaz. Exact sensitivity analysis of markov reward processes via algebraic geometry. arXiv preprint arXiv:2410.05471, 2024

    2024 arXiv

  23. [31]

    ACAS Xu: Integrated collision avoidance and detect and avoid capability for uas

    Michael P Owen, Adam Panken, Robert Moss, Luis Alvarez, and Charles Leeper. ACAS Xu: Integrated collision avoidance and detect and avoid capability for uas. In 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), pages 1–10. IEEE, 2019

    2019

  24. [32]

    Reluplex: An efficient smt solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part...

    2017

  25. [33]

    Evaluating robustness of neural networks with mixed integer programming

    Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356, 2017

    2017 arXiv

  26. [34]

    Maximum resilience of artificial neural networks

    Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15 , pages 251–268. Springer, 2017

    2017

  27. [35]

    Strong mixed-integer programming formulations for trained neural networks

    Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, 183(1):3–39, 2020. 11

    2020

  28. [36]

    The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification

    Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Kishor Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems, 33:216...

    2020

  29. [37]

    Between steps: Intermediate relaxations between big-m and convex hull formulations

    Jan Kronqvist, Ruth Misener, and Calvin Tsay. Between steps: Intermediate relaxations between big-m and convex hull formulations. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 299–314. Springer, 2021

    2021

  30. [38]

    Neural network verification as piecewise linear optimization: Formulations for the composition of staircase functions

    Tu Anh-Nguyen and Joey Huchette. Neural network verification as piecewise linear optimization: Formulations for the composition of staircase functions. arXiv preprint arXiv:2211.14706, 2022

    2022 arXiv

  31. [39]

    Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021

    2021

  32. [40]

    A branch and bound framework for stronger adversarial attacks of ReLU networks

    Huan Zhang, Shiqi Wang, Kaidi Xu, Yihan Wang, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. A branch and bound framework for stronger adversarial attacks of ReLU networks. In Proceedings of the 39th International Conference on Machine Learning, volume 162, pages 26591–26604, 2022

    2022

  33. [41]

    General cutting planes for bound-propagation-based neural network verification

    Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. General cutting planes for bound-propagation-based neural network verification. Ad- vances in Neural Information Processing Systems, 2022

    2022

  34. [42]

    Zico Kolter, Krishnamurthy Dvijotham, and Huan Zhang

    Suhas Kotha, Christopher Brix, J. Zico Kolter, Krishnamurthy Dvijotham, and Huan Zhang. Provably bounding neural network preimages. In A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, editors, Advances in Neural Information Processing Systems , vol- ume 36,...

    2023

  35. [43]

    Cost-effectiveness of a us national sugar-sweetened beverage tax with a multistakeholder approach: who pays and who benefits

    Parke Wilde, Yue Huang, Stephen Sy, Shafika Abrahams-Gessel, Thiago Veiga Jardim, Robert Paarlberg, Dariush Mozaffarian, Renata Micha, and Thomas Gaziano. Cost-effectiveness of a us national sugar-sweetened beverage tax with a multistakeholder approach: who pays and who benefi...

    2019

  36. [44]

    Health impact and cost- effectiveness of volume, tiered, and absolute sugar content sugar-sweetened beverage tax policies in the united states: a microsimulation study

    Yujin Lee, Dariush Mozaffarian, Stephen Sy, Junxiu Liu, Parke E Wilde, Matti Marklund, Shafika Abrahams-Gessel, Thomas A Gaziano, and Renata Micha. Health impact and cost- effectiveness of volume, tiered, and absolute sugar content sugar-sweetened beverage tax policies in the ...

    2020

  37. [45]

    Cost-effectiveness of population-based, community, workplace and individual policies for diabetes prevention in the uk

    PR Breeze, C Thomas, H Squires, A Brennan, C Greaves, P Diggle, E Brunner, A Tabak, L Preston, and J Chilcott. Cost-effectiveness of population-based, community, workplace and individual policies for diabetes prevention in the uk. Diabetic Medicine, 34(8):1136–1144, 2017

    2017

  38. [46]

    Handbook of global optimization, volume 2

    Reiner Horst and Panos M Pardalos. Handbook of global optimization, volume 2. Springer Science & Business Media, 2013

    2013

  39. [47]

    Computability of global solutions to factorable nonconvex programs: Part i—convex underestimating problems

    Garth P McCormick. Computability of global solutions to factorable nonconvex programs: Part i—convex underestimating problems. Mathematical programming, 10(1):147–175, 1976

    1976

  40. [48]

    Gurobi Optimizer Reference Manual, 2024

    Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024. URL https://www. gurobi.com

    2024

  41. [49]

    New socp relaxation and branching rule for bipartite bilinear programs

    Santanu S Dey, Asteroide Santana, and Yang Wang. New socp relaxation and branching rule for bipartite bilinear programs. Optimization and Engineering, 20:307–336, 2019

    2019

  42. [50]

    Markov decision processes: discrete stochastic dynamic programming

    Martin L Puterman. Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons, 2014

    2014

  43. [51]

    Mathematical theory of reliability

    Richard E Barlow and Frank Proschan. Mathematical theory of reliability. SIAM, 1996. 12

    1996

  44. [52]

    Determining the acceptance of cadaveric livers using an implicit model of the waiting list

    Oguzhan Alagoz, Lisa M Maillart, Andrew J Schaefer, and Mark S Roberts. Determining the acceptance of cadaveric livers using an implicit model of the waiting list. Operations Research, 55(1):24–36, 2007

    2007

  45. [53]

    R. G. Jeroslow and J. K. Lowe. Modelling with integer variables, pages 167–184. Springer Berlin Heidelberg, Berlin, Heidelberg, 1984

    1984

  46. [54]

    New techniques for the analysis of linear interval equations

    Arnold Neumaier. New techniques for the analysis of linear interval equations. Linear Algebra and its Applications, 58:273–325, 1984

    1984

  47. [55]

    Nonnegative matrices in the mathematical sciences

    Abraham Berman and Robert J Plemmons. Nonnegative matrices in the mathematical sciences. SIAM, 1994

    1994

  48. [56]

    Pedregosa, G

    F. Pedregosa, G. Varoquaux, A. Gramfort, V . Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V . Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-learn: Machine learning in Python. Journal of Machine Learni...

    2011

  49. [57]

    Pytorch: An imperative style, high-performance deep learning library

    Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. Pytorch: An imperative style, high-performance deep learning library. Advances in neural information processing systems, 32, 2019

    2019

  50. [58]

    Gurobi machine learning, 2024

    LLC Gurobi Optimization. Gurobi machine learning, 2024. URL https://pypi.org/ project/gurobi-machinelearning/. Python package for integrating regression models into optimization problems

    2024

  51. [59]

    Cost-effectiveness of drone-delivered automated external defibrillators for cardiac arrest

    Muhammad Maaz, KH Benjamin Leung, Justin J Boutilier, Sze-chuan Suen, Paul Dorian, Lau- rie J Morrison, Damon C Scales, Sheldon Cheskes, and Timothy CY Chan. Cost-effectiveness of drone-delivered automated external defibrillators for cardiac arrest. Resuscitation, 209:110552, 2025

    2025

  52. [60]

    Association between sex and mortality in adults with in-hospital and out-of-hospital cardiac arrest: A systematic review and meta-analysis

    Puja B Parikh, Lukman Hassan, Asem Qadeer, and Jignesh K Patel. Association between sex and mortality in adults with in-hospital and out-of-hospital cardiac arrest: A systematic review and meta-analysis. Resuscitation, 155:119–124, 2020

    2020

  53. [61]

    Interval linear and nonlinear systems

    Jaroslav Horá ˇcek. Interval linear and nonlinear systems . Phd thesis, Univerzita Karlova, Matematicko-fyzikální fakulta, Prague, Czech Republic, 2019. 13 A Formulations of feasibility, reachability, and hitting time A.1 Feasibility of the total infinite-horizon reward The to...

    2019

  54. [62]

    For each variable xi, compute a new enclosure of the solution set as: y(k+1) i = 1 Aii  bi − X j<i Aijx(k+1) j − X j>i Aijx(k) j  

  55. [63]

    Update the enclosure of the solution set: x(k+1) = x(k) ∩ y(k+1)

  56. [64]

    All operations above are interval arithmetic operations

    Repeat steps 1 and 2 until stopping criterion is met (either a maximum number of iterations or the difference in subsequent enclosures is less than some tolerance). All operations above are interval arithmetic operations. For real intervals, we have: [a, b] + [c, d] = [a + c, ...

  57. [65]

    The spectral radius of Q is strictly less than 1

  58. [66]

    The matrix (I − Q) is a (non-singular) M-matrix

  59. [67]

    The matrix (I − Q)−1 has all non-negative elements

  60. [68]

    The row sums of(I − Q)−1 are at most 1/(1 − α), where α = maxi P j Qij is the maximum row sum of Q

  61. [69]

    if-then" rules specified in natural language, e.g., “if age >= 65 then 0.8

    Each element of (I − Q)−1 is in the interval [0, 1/(1 − α)]. Proof. The row sum of Q is strictly less than 1, so, by a well-known result in linear algebra, the spectral radius of Q is strictly less than 1. It follows that I − Q is a (non-singular) M-matrix by the definition of...

  62. [70]

    State Space: Vary n ∈ {5, 10, 20, 50, 100, 200} using three models: a linear regression for r and two logistic regressions for π and the first row of P (the remaining rows are uniform)

  63. [71]

    Models for r and π are always used, while the number of modeled rows in P varies from 1 to 19, so that the total number of models runs from 3 to 21

    Model Count: Fix n = 20 with linear regression for r and logistic regression for all probability models. Models for r and π are always used, while the number of modeled rows in P varies from 1 to 19, so that the total number of models runs from 3 to 21

  64. [72]

    Remaining rows of P are uniform

    Decision Tree Depth: Fix n = 20using three decision tree models (for r, π, and the first row of P) with depths in {2, 3, 4, 6, 8}. Remaining rows of P are uniform

  65. [73]

    We vary hidden layers in {1, 2} and neurons per layer in {5, 10, 15, 20}, with remaining rows of P set uniformly

    Neural Network Architecture: Fix n = 20using three ReLU multilayer perceptrons, for r, π, and the first row of P. We vary hidden layers in {1, 2} and neurons per layer in {5, 10, 15, 20}, with remaining rows of P set uniformly. We record runtime, objective value, and optimizer...

  66. [74]

    [Yes] " is generally preferable to

    (1200 second limit per problem, and presolve disabled throughout). All code and instructions on how to reproduce our experiments is included along with this paper. We computed the geometric mean and geometric standard deviations of runtimes, and proportions of optimizer status...

  67. [75]

    Guidelines: • The answer NA means that the abstract and introduction do not include the claims made in the paper

    Claims Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope? Answer: [Yes] Justification: We state the key motivation (Markov models with embedded ML models), the key idea (bilinear programming) and the key r...

  68. [76]

    Limitations

    Limitations Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [TODO] 22 Justification: [TODO] Guidelines: • The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are...

  69. [77]

    For proofs using more novel techniques (e.g

    Theory assumptions and proofs Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: [Yes] Justification: All theorems and lemmas are clearly stated, with all proofs given in the Appendix. For proof...

  70. [78]

    As well, we release all code for the numerical experiments (with instructions on how to run each of the experiments with a simple command-line command)

    Experimental result reproducibility Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and da...

  71. [79]

    We also release all the code for the numerical experiments, as simple scripts to run them, and for the case study

    Open access to data and code Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material? Answer: [Yes] Justification: We release markovml in the ...

  72. [80]

    Guidelines: • The answer NA means that the paper does not include experiments

    Experimental setting/details Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results? Answer: [Yes] Justification: Described roughly in the main...

  73. [81]

    Guidelines: • The answer NA means that the paper does not include experiments

    Experiment statistical significance Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments? Answer: [Yes] Justification: Plots show statistical significance, using either ...

  74. [82]

    Experiments compute resources 25 Question: For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments? Answer: [Yes] Justification: Described in appendi...

  75. [83]

    Guidelines: • The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics

    Code of ethics Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines? Answer: [Yes] Justification: We conform in every respect with the NeurIPS Code of Ethics. Guidelines: • The ...

  76. [84]

    Guidelines: • The answer NA means that there is no societal impact of the work performed

    Broader impacts Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed? Answer: [Yes] Justification: In the Discussion we discuss its role in safety-critical domains. Guidelines: • The answer NA means that ...

  77. [85]

    Guidelines: • The answer NA means that the paper poses no such risks

    Safeguards Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)? Answer: [NA] Justification: None needed. Gu...

  78. [86]

    Guidelines: • The answer NA means that the paper does not use existing assets

    Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected? Answer: [NA] Justification: No existing asset...

  79. [87]

    Guidelines: • The answer NA means that the paper does not release new assets

    New assets Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets? Answer: [Yes] Justification: Our software, markovml, is fully documented with extensive examples. Guidelines: • The answer NA means that the pape...

  80. [88]

    Guidelines: • The answer NA means that the paper does not involve crowdsourcing nor research with human subjects

    Crowdsourcing and research with human subjects Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)? A...

  81. [89]

    Guidelines: • The answer NA means that the paper does not involve crowdsourcing nor research with human subjects

    Institutional review board (IRB) approvals or equivalent for research with human subjects Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals...

  82. [90]

    Answer: [No] Justification: Does not use LLMs

    Declaration of LLM usage Question: Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the ...

    2025

Pith tools

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