Formal Verification of Markov Processes with Learned Parameters

• URL: http://arxiv.org/abs/2501.15767v1
• Date: Mon, 27 Jan 2025 04:34:22 GMT
• Title: Formal Verification of Markov Processes with Learned Parameters
• Authors: Muhammad Maaz, Timothy C. Y. Chan,
• Abstract summary: We show that for a broad class of machine learning models, verifying properties of Markov chains can be formulated as a bilinear program. We show through computational experiments that our method solves the problem to global optimality up to 100x faster than state-of-the-art solvers.
• Score: 2.5694725194040804
• License:
• Abstract: 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.

Related papers

• Learning to sample fibers for goodness-of-fit testing [0.0]
  We consider the problem of constructing exact goodness-of-fit tests for discrete exponential family models. We translate the problem into a Markov decision process and demonstrate a reinforcement learning approach for learning good moves' for sampling. Our algorithm is based on an actor-critic sampling scheme, with provable convergence.
  arXiv  Detail & Related papers  (2024-05-22T19:33:58Z)
• CogCoM: Train Large Vision-Language Models Diving into Details through Chain of Manipulations [61.21923643289266]
  Chain of Manipulations is a mechanism that enables Vision-Language Models to solve problems step-by-step with evidence. After training, models can solve various visual problems by eliciting intrinsic manipulations (e.g., grounding, zoom in) actively without involving external tools. Our trained model, textbfCogCoM, achieves state-of-the-art performance across 9 benchmarks from 4 categories.
  arXiv  Detail & Related papers  (2024-02-06T18:43:48Z)
• Machine Learning Insides OptVerse AI Solver: Design Principles and Applications [74.67495900436728]
  We present a comprehensive study on the integration of machine learning (ML) techniques into Huawei Cloud's OptVerse AI solver. We showcase our methods for generating complex SAT and MILP instances utilizing generative models that mirror multifaceted structures of real-world problem. We detail the incorporation of state-of-the-art parameter tuning algorithms which markedly elevate solver performance.
  arXiv  Detail & Related papers  (2024-01-11T15:02:15Z)
• Generative Learning of Continuous Data by Tensor Networks [45.49160369119449]
  We introduce a new family of tensor network generative models for continuous data. We benchmark the performance of this model on several synthetic and real-world datasets. Our methods give important theoretical and empirical evidence of the efficacy of quantum-inspired methods for the rapidly growing field of generative learning.
  arXiv  Detail & Related papers  (2023-10-31T14:37:37Z)
• Blending gradient boosted trees and neural networks for point and probabilistic forecasting of hierarchical time series [0.0]
  We describe a blending methodology of machine learning models that belong to gradient boosted trees and neural networks families. These principles were successfully applied in the recent M5 Competition on both Accuracy and Uncertainty tracks.
  arXiv  Detail & Related papers  (2023-10-19T09:42:02Z)
• Advancing Reacting Flow Simulations with Data-Driven Models [50.9598607067535]
  Key to effective use of machine learning tools in multi-physics problems is to couple them to physical and computer models. The present chapter reviews some of the open opportunities for the application of data-driven reduced-order modeling of combustion systems.
  arXiv  Detail & Related papers  (2022-09-05T16:48:34Z)
• Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended) [0.0]
  This paper revisits and adapts the classic Baum-Welch algorithm for learning Markov decision processes and Markov chains. We empirically compare our approach with state-of-the-art tools and demonstrate that the proposed active learning procedure can significantly reduce the number of observations required to obtain accurate models.
  arXiv  Detail & Related papers  (2021-10-06T18:54:19Z)
• A Framework for Machine Learning of Model Error in Dynamical Systems [7.384376731453594]
  We present a unifying framework for blending mechanistic and machine-learning approaches to identify dynamical systems from data. We cast the problem in both continuous- and discrete-time, for problems in which the model error is memoryless and in which it has significant memory. We find that hybrid methods substantially outperform solely data-driven approaches in terms of data hunger, demands for model complexity, and overall predictive performance.
  arXiv  Detail & Related papers  (2021-07-14T12:47:48Z)
• Model-agnostic multi-objective approach for the evolutionary discovery of mathematical models [55.41644538483948]
  In modern data science, it is more interesting to understand the properties of the model, which parts could be replaced to obtain better results. We use multi-objective evolutionary optimization for composite data-driven model learning to obtain the algorithm's desired properties.
  arXiv  Detail & Related papers  (2021-07-07T11:17:09Z)
• Outlier-Robust Learning of Ising Models Under Dobrushin's Condition [57.89518300699042]
  We study the problem of learning Ising models satisfying Dobrushin's condition in the outlier-robust setting where a constant fraction of the samples are adversarially corrupted. Our main result is to provide the first computationally efficient robust learning algorithm for this problem with near-optimal error guarantees.
  arXiv  Detail & Related papers  (2021-02-03T18:00:57Z)
• Learning Gaussian Graphical Models via Multiplicative Weights [54.252053139374205]
  We adapt an algorithm of Klivans and Meka based on the method of multiplicative weight updates. The algorithm enjoys a sample complexity bound that is qualitatively similar to others in the literature. It has a low runtime $O(mp2)$ in the case of $m$ samples and $p$ nodes, and can trivially be implemented in an online manner.
  arXiv  Detail & Related papers  (2020-02-20T10:50:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.