arXiv:2501.15767v2 宣告类型: replace-cross 摘要: 我们介绍了正式验证具有机器学习模型输出参数的马尔可夫过程性质的问题。对于包括线性模型、树基模型和神经网络在内的广泛类别的机器学习模型，验证马尔可夫链的性质，如可达性、击中时间和总奖励，可以被表述为双线性规划问题。我们开发了一种分解和界传播方案来求解双线性规划问题，并通过计算实验表明，我们的方法在求解问题到全局最优解方面比最先进的求解器快100倍以上。为了展示我们方法的实际用途，我们将其应用于一个实际的医疗健康案例研究。除了论文，我们还发布了 markovml，这是一个开源工具，用于构建马尔可夫过程、集成预训练的机器学习模型以及验证其性质，可在 https://github.com/mmaaz-git/markovml 获取。