Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees

• URL: http://arxiv.org/abs/2309.08883v2
• Date: Sat, 30 Dec 2023 21:05:41 GMT
• Title: Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
• Authors: Jinzhao Li, Nan Jiang, Yexiang Xue
• Abstract summary: Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. XOR-SMC transforms the highly intractable SMC into satisfiability problems, by replacing the model counting in SMC with SAT formulae. XOR-SMC finds solutions close to the true optimum, outperforming several baselines which struggle to find good approximations for the intractable model counting in SMC.
• Score: 18.7083987727973
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. Its general formulation captures many real-world problems at the intersection of symbolic and statistical Artificial Intelligence. SMC searches for policy interventions to control probabilistic outcomes. Solving SMC is challenging because of its highly intractable nature($\text{NP}^{\text{PP}}$-complete), incorporating statistical inference and symbolic reasoning. Previous research on SMC solving lacks provable guarantees and/or suffers from sub-optimal empirical performance, especially when combinatorial constraints are present. We propose XOR-SMC, a polynomial algorithm with access to NP-oracles, to solve highly intractable SMC problems with constant approximation guarantees. XOR-SMC transforms the highly intractable SMC into satisfiability problems, by replacing the model counting in SMC with SAT formulae subject to randomized XOR constraints. Experiments on solving important SMC problems in AI for social good demonstrate that XOR-SMC finds solutions close to the true optimum, outperforming several baselines which struggle to find good approximations for the intractable model counting in SMC.

Related papers

• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• Best Arm Identification with Fixed Budget: A Large Deviation Perspective [54.305323903582845]
  We present sred, a truly adaptive algorithm that can reject arms in it any round based on the observed empirical gaps between the rewards of various arms. In particular, we present sred, a truly adaptive algorithm that can reject arms in it any round based on the observed empirical gaps between the rewards of various arms.
  arXiv  Detail & Related papers  (2023-12-19T13:17:43Z)
• Worst-Case Analysis is Maximum-A-Posteriori Estimation [9.61085323616992]
  Worst-case resource usage of a program can provide useful information for many software-engineering tasks. This paper presents a generic, adaptive, and sound fuzzing framework, called DSE-SMC, for estimating worst-case resource usage.
  arXiv  Detail & Related papers  (2023-10-15T08:24:02Z)
• On the Global Solution of Soft k-Means [159.23423824953412]
  This paper presents an algorithm to solve the Soft k-Means problem globally. A new model, named Minimal Volume Soft kMeans (MVSkM), is proposed to address solutions non-uniqueness issue.
  arXiv  Detail & Related papers  (2022-12-07T12:06:55Z)
• Stability and Generalization for Markov Chain Stochastic Gradient Methods [49.981789906200035]
  We provide a comprehensive generalization analysis of MC-SGMs for both minimization and minimax problems. We establish the optimal excess population risk bounds for both smooth and non-smooth cases. We develop the first nearly optimal convergence rates for convex-concave problems both in expectation and with high probability.
  arXiv  Detail & Related papers  (2022-09-16T15:42:51Z)
• Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL* [6.574517227976925]
  We present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs) Our algorithm performs better both in terms of the verification time and the number of samples required to deduce satisfiability of a given HyperPCTL* formula.
  arXiv  Detail & Related papers  (2022-09-06T17:36:28Z)
• 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)
• Variational Combinatorial Sequential Monte Carlo Methods for Bayesian Phylogenetic Inference [4.339931151475307]
  We introduce Vari Combinatorial Monte Carlo (VCSMC), a powerful framework that establishes variational search to learn over intricate structures. We show that VCSMC and CSMC are efficient and explore higher probability spaces than existing methods on a range of tasks.
  arXiv  Detail & Related papers  (2021-05-31T19:44:24Z)
• 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)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

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.