Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2501.15767 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866918016693829632 |
|---|---|
| author | Maaz, Muhammad Chan, Timothy C. Y. |
| author_facet | Maaz, Muhammad Chan, Timothy C. Y. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_15767 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Verification of Markov Processes with Learned Parameters Maaz, Muhammad Chan, Timothy C. Y. Machine Learning Artificial Intelligence 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 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. |
| title | Formal Verification of Markov Processes with Learned Parameters |
| topic | Machine Learning Artificial Intelligence Optimization and Control 68Q60 (primary) 90C30, 60J20, 60J22 (secondary) F.4.1; G.1.6; I.2.3 |
| url | https://arxiv.org/abs/2501.15767 |