Skip to yearly menu bar Skip to main content


Poster
in
Workshop: CODEML: Championing Open-source DEvelopment in Machine Learning

$\texttt{markovml}$: A Python Package for Verifying Markov Processes with Embedded Machine Learning Models

Muhammad Maaz · Timothy Chan

[ ] [ Project Page ]
Fri 18 Jul 2:15 p.m. PDT — 3 p.m. PDT

Abstract: We present $\texttt{markovml}$, a Python package for verifying properties of Markov processes whose parameters are defined by machine learning (ML) models. While existing tools support formal verification of either Markov processes or ML models individually, none support reasoning about systems that integrate both. $\texttt{markovml}$ fills this gap by allowing users to construct Markov processes and embed pretrained models from standard ML libraries, including linear models, decision trees, and neural networks. The package provides an expressive domain-specific language to specify constraints and verify common properties such as reachability, expected hitting time, and total reward. We illustrate usage through several examples and release the package with full documentation and tutorials.

Chat is not available.