Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Verification of Markov Processes with Learned Parameters

Muhammad Maaz, Timothy C. Y. Chan

TL;DR

Formally verify Markov processes whose transition and reward parameters derive from ML outputs by casting verification problems as bilinear programs. The authors develop a decomposition and bound-propagation scheme that delivers global optima far faster than generic solvers, enabling exact analysis in settings with ML-predicted parameters and large state spaces. They validate the approach on synthetic experiments and a healthcare case study, and release markovml to embed pretrained ML models, construct Markov processes, and verify reachability, hitting time, and total reward. The work advances safe and transparent deployment of ML in high-stakes domains by providing rigorous guarantees and a practical, extensible toolchain.

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.

Formal Verification of Markov Processes with Learned Parameters

TL;DR

Formally verify Markov processes whose transition and reward parameters derive from ML outputs by casting verification problems as bilinear programs. The authors develop a decomposition and bound-propagation scheme that delivers global optima far faster than generic solvers, enabling exact analysis in settings with ML-predicted parameters and large state spaces. They validate the approach on synthetic experiments and a healthcare case study, and release markovml to embed pretrained ML models, construct Markov processes, and verify reachability, hitting time, and total reward. The work advances safe and transparent deployment of ML in high-stakes domains by providing rigorous guarantees and a practical, extensible toolchain.

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.
Paper Structure (42 sections, 8 theorems, 14 equations, 3 figures, 2 tables, 1 algorithm)

This paper contains 42 sections, 8 theorems, 14 equations, 3 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Formal Verification of Markov Processes
  4. Markov Processes with Uncertain Parameters
  5. Formal Verification of ML Models
  6. Subgroup Analysis in Healthcare
  7. Bilinear Programming
  8. Problem Formulation
  9. Notation
  10. Preliminaries
  11. Embedding ML Models
  12. Solving the Optimization Problem
  13. Bounds on $\boldsymbol{\mathbf{\theta}}$
  14. Bounds on $\boldsymbol{\mathbf{\pi}}, \boldsymbol{\mathbf{P}}, \boldsymbol{\mathbf{r}}$
  15. Bounds on $\boldsymbol{\mathbf{v}}$
  16. ...and 27 more sections

Key Result

Lemma 4.1

Let $\boldsymbol{\mathbf{\theta}} \in \mathbb{R}^\ell$ be a vector where each component satisfies the bounds $\theta_i^{\min} \leq \theta_i \leq \theta_i^{\max}$ for all $i = 1, 2, \ldots, \ell$. Consider an affine transformation defined by $\boldsymbol{\mathbf{y}} = \boldsymbol{\mathbf{A}} \boldsym

Figures (3)

  • Figure 1: Example of our pipeline. A feature vector $\boldsymbol{\mathbf{x}}$ is passed through different functions, here a linear regression and a neural network, to obtain the output vector $\boldsymbol{\mathbf{\theta}}$, which then determines the parameters of the Markov process through affine equalities.
  • Figure 2: Runtimes of our method versus direct solving. Each panel shows results from experiments 1-4 (left to right). Points represent geometric means with error bars indicating standard deviation. Statistical significance from paired t-tests shown above: * ($p < 0.05$), † ($p < 0.01$), and § ($p < 0.001$).
  • Figure 3: Proportion (%) of instances categorized as optimal, suboptimal, timed out, or other. Each panel shows experiments 1-4 (left to right). Our method is the left bar and direct method is the right bar. Statistical significance from $\chi^2$ shown above: * ($p < 0.05$), † ($p < 0.01$), and § ($p < 0.001$).

Theorems & Definitions (20)

  • Definition 3.1: Reachability
  • Definition 3.2: Expected hitting time
  • Definition 3.3: Total infinite-horizon discounted reward
  • Lemma 4.1
  • Lemma 4.2
  • Lemma 4.3
  • Theorem 4.4
  • Example 4.5
  • proof : Proof of Lemma \ref{['lem:affine_bounds']}
  • proof : Proof of Lemma \ref{['lem:inverse_bounds']}
  • ...and 10 more