Formal Verification of Markov Processes with Learned Parameters

TL;DR

This paper presents a novel method for the formal verification of Markov processes with parameters learned from machine learning models, enabling efficient analysis of properties like reachability and reward.

Contribution

It introduces a bilinear programming approach for verifying properties of Markov processes with ML-derived parameters, and provides an open-source tool for practical application.

Findings

Method solves bilinear programs up to 100x faster than existing solvers.

Applicable to various ML models including neural networks and trees.

Demonstrated on a real-world healthcare case study.

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.