# Formal Verification of Markov Processes with Learned Parameters

arXiv: https://arxiv.org/abs/2501.15767 · HTML: https://mlsanity.com/paper/2501.15767/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 62 references that are in the map.
- First posted on arXiv 27 Jan 2025.

## Builds on (most cited first, 16 of 16)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification](https://mlsanity.com/paper/2006.14076/) (2020)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Parameter Synthesis for Markov Models: Covering the Parameter Space](https://mlsanity.com/paper/1903.07993/) (2019)
- [Between steps: Intermediate relaxations between big-M and convex hull formulations](https://mlsanity.com/paper/2101.12708/) (2021)
- [On the convex formulations of robust Markov decision processes](https://mlsanity.com/paper/2209.10187/) (2022)
- [Sensitivity analysis for finite Markov chains in discrete time](https://mlsanity.com/paper/1408.2029/) (2014)
- [Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions](https://mlsanity.com/paper/2211.14706/) (2022)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [New SOCP relaxation and branching rule for bipartite bilinear programs](https://mlsanity.com/paper/1803.09266/) (2018)
- [Exact sensitivity analysis of Markov reward processes via algebraic geometry](https://mlsanity.com/paper/2410.05471/) (2024)

## Built on by (most cited first, 1 of 1)

- [Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI](https://mlsanity.com/paper/2604.19431/) (2026)

## Abstract (arXiv)

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.