Formal Verification of Markov Processes with Learned Parameters
This addresses the need for reliable verification in safety-critical applications like healthcare, though it is incremental as it builds on existing verification frameworks.
The paper tackles the problem of formally verifying properties of Markov processes with parameters learned from machine learning models, developing a method that solves verification tasks up to 100x faster than state-of-the-art solvers.
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.