Report
Formal Verification of Markov Processes with Learned Parameters
| العنوان: | Formal Verification of Markov Processes with Learned Parameters |
|---|---|
| المؤلفون: | Maaz, Muhammad, Chan, Timothy C. Y. |
| سنة النشر: | 2025 |
| المجموعة: | Computer Science Mathematics |
| مصطلحات موضوعية: | Computer Science - Machine Learning, Computer Science - Artificial Intelligence, Mathematics - Optimization and Control, 68Q60 (primary) 90C30, 60J20, 60J22 (secondary), F.4.1, G.1.6, I.2.3 |
| الوصف: | We introduce the problem of formally verifying properties of Markov processes where the parameters are the output of machine learning models. Our formulation is general and solves a wide range of problems, including verifying properties of probabilistic programs that use machine learning, and subgroup analysis in healthcare modeling. We show that 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. We also release $\texttt{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. Comment: 8 pages (main manuscript), 3 figures, 1 table |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2501.15767 |
| رقم الانضمام: | edsarx.2501.15767 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |