用机器学习模型参数构建马尔可夫过程，并验证其性质
Formal Verification of Markov Processes with Learned Parameters
- 将机器学习输出作为马尔可夫过程参数，建模为双线性规划问题
- 在真实医疗案例中实现全局最优解，速度比现有工具快100倍
- 开源工具markovml支持端到端建模与验证，适合医疗决策研究者
我们提出形式化验证由机器学习模型输出参数的马尔可夫过程属性的问题。对于线性模型、树模型和神经网络等广泛类型的机器学习模型，可达性、击中时间与总奖励等马尔可夫链性质的验证可转化为双线性规划问题。我们设计了分解与边界传播求解算法，计算实验表明该方法在求解全局最优解方面比当前最先进的求解器快达100倍。为展示方法的实际价值，我们在一个真实医疗案例中进行了应用。本文附带发布开源工具markovml，用于构建集成预训练机器学习模型的马尔可夫过程并验证其性质，项目地址：https://github.com/mmaaz-git/markovml。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。