Enhancing SMT-based Weighted Model Integration by Structure Awareness

• URL: http://arxiv.org/abs/2302.06188v2
• Date: Tue, 9 Jan 2024 13:47:37 GMT
• Title: Enhancing SMT-based Weighted Model Integration by Structure Awareness
• Authors: Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
• Abstract summary: Weighted Model Integration (WMI) emerged as a unifying formalism for probabilistic inference in hybrid domains. We develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure.
• Score: 10.812681884889697
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress has been made in dealing with purely discrete or purely continuous domains, adapting the developed solutions to tackle hybrid domains, characterised by discrete and continuous variables and their relationships, is highly non-trivial. Weighted Model Integration (WMI) recently emerged as a unifying formalism for probabilistic inference in hybrid domains. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in drastic computational savings. Additionally, we show how SMT-based approaches can seamlessly deal with different integration techniques, both exact and approximate, significantly expanding the set of problems that can be tackled by WMI technology. An extensive experimental evaluation on both synthetic and real-world datasets confirms the substantial advantage of the proposed solution over existing alternatives. The application potential of this technology is further showcased on a prototypical task aimed at verifying the fairness of probabilistic programs.

Related papers

• A unified consensus-based parallel ADMM algorithm for high-dimensional regression with combined regularizations [3.280169909938912]
  parallel alternating multipliers (ADMM) is widely recognized for its effectiveness in handling large-scale distributed datasets. The proposed algorithms serve to demonstrate the reliability, stability, and scalability of a financial example.
  arXiv  Detail & Related papers  (2023-11-21T03:30:38Z)
• SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
  Large Language Models (LLMs) have driven substantial progress in artificial intelligence. We propose a novel framework called textbfSEquential subtextbfGoal textbfOptimization (SEGO) to enhance LLMs' ability to solve mathematical problems.
  arXiv  Detail & Related papers  (2023-10-19T17:56:40Z)
• Solution to Advanced Manufacturing Process Problems using Cohort Intelligence Algorithm with Improved Constraint Handling Approaches [0.07989135005592125]
  Cohort Intelligence (CI) algorithm is a socio inspired optimization technique which is successfully applied for solving several unconstrained & constrained real-world problems from the domains such as design, manufacturing, supply chain, healthcare, etc.
  arXiv  Detail & Related papers  (2023-10-16T05:40:23Z)
• Distributionally Robust Model-based Reinforcement Learning with Large State Spaces [55.14361269378122]
  Three major challenges in reinforcement learning are the complex dynamical systems with large state spaces, the costly data acquisition processes, and the deviation of real-world dynamics from the training environment deployment. We study distributionally robust Markov decision processes with continuous state spaces under the widely used Kullback-Leibler, chi-square, and total variation uncertainty sets. We propose a model-based approach that utilizes Gaussian Processes and the maximum variance reduction algorithm to efficiently learn multi-output nominal transition dynamics.
  arXiv  Detail & Related papers  (2023-09-05T13:42:11Z)
• A Multi-Head Ensemble Multi-Task Learning Approach for Dynamical Computation Offloading [62.34538208323411]
  We propose a multi-head ensemble multi-task learning (MEMTL) approach with a shared backbone and multiple prediction heads (PHs) MEMTL outperforms benchmark methods in both the inference accuracy and mean square error without requiring additional training data.
  arXiv  Detail & Related papers  (2023-09-02T11:01:16Z)
• SMT-based Weighted Model Integration with Structure Awareness [18.615397594541665]
  We develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in substantial computational savings.
  arXiv  Detail & Related papers  (2022-06-28T09:46:17Z)
• Minimum-Delay Adaptation in Non-Stationary Reinforcement Learning via Online High-Confidence Change-Point Detection [7.685002911021767]
  We introduce an algorithm that efficiently learns policies in non-stationary environments. It analyzes a possibly infinite stream of data and computes, in real-time, high-confidence change-point detection statistics. We show that (i) this algorithm minimizes the delay until unforeseen changes to a context are detected, thereby allowing for rapid responses.
  arXiv  Detail & Related papers  (2021-05-20T01:57:52Z)
• Offline Model-Based Optimization via Normalized Maximum Likelihood Estimation [101.22379613810881]
  We consider data-driven optimization problems where one must maximize a function given only queries at a fixed set of points. This problem setting emerges in many domains where function evaluation is a complex and expensive process. We propose a tractable approximation that allows us to scale our method to high-capacity neural network models.
  arXiv  Detail & Related papers  (2021-02-16T06:04:27Z)
• Efficient semidefinite-programming-based inference for binary and multi-class MRFs [83.09715052229782]
  We propose an efficient method for computing the partition function or MAP estimate in a pairwise MRF. We extend semidefinite relaxations from the typical binary MRF to the full multi-class setting, and develop a compact semidefinite relaxation that can again be solved efficiently using the solver.
  arXiv  Detail & Related papers  (2020-12-04T15:36:29Z)
• Iterative Algorithm Induced Deep-Unfolding Neural Networks: Precoding Design for Multiuser MIMO Systems [59.804810122136345]
  We propose a framework for deep-unfolding, where a general form of iterative algorithm induced deep-unfolding neural network (IAIDNN) is developed. An efficient IAIDNN based on the structure of the classic weighted minimum mean-square error (WMMSE) iterative algorithm is developed. We show that the proposed IAIDNN efficiently achieves the performance of the iterative WMMSE algorithm with reduced computational complexity.
  arXiv  Detail & Related papers  (2020-06-15T02:57:57Z)
• Hyperspectral Unmixing Network Inspired by Unfolding an Optimization Problem [2.4016406737205753]
  The hyperspectral image (HSI) unmixing task is essentially an inverse problem, which is commonly solved by optimization algorithms. We propose two novel network architectures, named U-ADMM-AENet and U-ADMM-BUNet, for abundance estimation and blind unmixing. We show that the unfolded structures can find corresponding interpretations in machine learning literature, which further demonstrates the effectiveness of proposed methods.
  arXiv  Detail & Related papers  (2020-05-21T18:49:45Z)

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.