Formal Verification of Markov Processes with Learned Parameters

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.