Towards Practical First-Order Model Counting

• URL: http://arxiv.org/abs/2502.12278v1
• Date: Mon, 17 Feb 2025 19:28:06 GMT
• Title: Towards Practical First-Order Model Counting
• Authors: Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, Kuldeep S. Meel,
• Abstract summary: First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic.<n>New approach based on first-order knowledge compilation was proposed.<n>The primary contribution of this work is a fully automated compilation algorithm, called Gantry, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic.
• Score: 25.295313268611217
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to variants of FOMC, the design of scalable methods for FOMC has attracted attention from both theoreticians and practitioners over the past decade. Recently, a new approach based on first-order knowledge compilation was proposed. This approach, called Crane, instead of simply providing the final count, generates definitions of (possibly recursive) functions that can be evaluated with different arguments to compute the model count for any domain size. However, this approach is not fully automated, as it requires manual evaluation of the constructed functions. The primary contribution of this work is a fully automated compilation algorithm, called Gantry, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic. These additions allow the new FOMC algorithm to scale to domain sizes over 500,000 times larger than the current state of the art, as demonstrated through experimental results.

Related papers

• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  evaluating constraint on every token can be prohibitively expensive. LCD can distort the global distribution over strings, sampling tokens based only on local information. We show that our approach is superior to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-04-07T18:30:18Z)
• Inference-Time Alignment in Diffusion Models with Reward-Guided Generation: Tutorial and Review [59.856222854472605]
  This tutorial provides an in-depth guide on inference-time guidance and alignment methods for optimizing downstream reward functions in diffusion models. practical applications in fields such as biology often require sample generation that maximizes specific metrics. We discuss (1) fine-tuning methods combined with inference-time techniques, (2) inference-time algorithms based on search algorithms such as Monte Carlo tree search, and (3) connections between inference-time algorithms in language models and diffusion models.
  arXiv  Detail & Related papers  (2025-01-16T17:37:35Z)
• Scalable Inference for Bayesian Multinomial Logistic-Normal Dynamic Linear Models [0.5735035463793009]
  This article develops an efficient and accurate approach to posterior state estimation, called $textitFenrir$. Our experiments suggest that Fenrir can be three orders of magnitude more efficient than Stan. Our methods are made available to the community as a user-friendly software library written in C++ with an R interface.
  arXiv  Detail & Related papers  (2024-10-07T23:20:14Z)
• How to Leverage Digit Embeddings to Represent Numbers? [13.880400817682059]
  In numerical reasoning, understanding numbers themselves is still a challenge for existing language models.<n>Character-level embeddings of numbers have emerged as a promising approach to improve number representation.<n>We use mathematical priors to compute aggregated digit embeddings and explicitly incorporate these aggregates into transformer models.
  arXiv  Detail & Related papers  (2024-07-01T01:31:41Z)
• MAP: Low-compute Model Merging with Amortized Pareto Fronts via Quadratic Approximation [80.47072100963017]
  We introduce a novel and low-compute algorithm, Model Merging with Amortized Pareto Front (MAP) MAP efficiently identifies a set of scaling coefficients for merging multiple models, reflecting the trade-offs involved. We also introduce Bayesian MAP for scenarios with a relatively low number of tasks and Nested MAP for situations with a high number of tasks, further reducing the computational cost of evaluation.
  arXiv  Detail & Related papers  (2024-06-11T17:55:25Z)
• Efficient Model-Free Exploration in Low-Rank MDPs [76.87340323826945]
  Low-Rank Markov Decision Processes offer a simple, yet expressive framework for RL with function approximation. Existing algorithms are either (1) computationally intractable, or (2) reliant upon restrictive statistical assumptions. We propose the first provably sample-efficient algorithm for exploration in Low-Rank MDPs.
  arXiv  Detail & Related papers  (2023-07-08T15:41:48Z)
• Provably Efficient Representation Learning with Tractable Planning in Low-Rank POMDP [81.00800920928621]
  We study representation learning in partially observable Markov Decision Processes (POMDPs) We first present an algorithm for decodable POMDPs that combines maximum likelihood estimation (MLE) and optimism in the face of uncertainty (OFU) We then show how to adapt this algorithm to also work in the broader class of $gamma$-observable POMDPs.
  arXiv  Detail & Related papers  (2023-06-21T16:04:03Z)
• Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures [12.47276164048813]
  First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. We relax the restrictions that typically accompany domain recursion to work with directed graphs that may contain cycles. These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach.
  arXiv  Detail & Related papers  (2023-06-07T06:49:01Z)
• Solving Projected Model Counting by Utilizing Treewidth and its Limits [23.81311815698799]
  We introduce a novel algorithm to solve projected model counting (PMC) Inspired by the observation that the so-called "treewidth" is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance.
  arXiv  Detail & Related papers  (2023-05-30T17:02:07Z)
• Model Predictive Control with Self-supervised Representation Learning [13.225264876433528]
  We propose the use of a reconstruction function within the TD-MPC framework, so that the agent can reconstruct the original observation. Our proposed addition of another loss term leads to improved performance on both state- and image-based tasks.
  arXiv  Detail & Related papers  (2023-04-14T16:02:04Z)
• Formalization of a Stochastic Approximation Theorem [0.22940141855172028]
  approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown. Originally introduced in a 1951 paper by Robbins and Monro, the field of approximation has grown enormously and has come to influence application domains.
  arXiv  Detail & Related papers  (2022-02-12T02:31:14Z)
• Causality-based Counterfactual Explanation for Classification Models [11.108866104714627]
  We propose a prototype-based counterfactual explanation framework (ProCE) ProCE is capable of preserving the causal relationship underlying the features of the counterfactual data. In addition, we design a novel gradient-free optimization based on the multi-objective genetic algorithm that generates the counterfactual explanations.
  arXiv  Detail & Related papers  (2021-05-03T09:25:59Z)
• Slice Sampling for General Completely Random Measures [74.24975039689893]
  We present a novel Markov chain Monte Carlo algorithm for posterior inference that adaptively sets the truncation level using auxiliary slice variables. The efficacy of the proposed algorithm is evaluated on several popular nonparametric models.
  arXiv  Detail & Related papers  (2020-06-24T17:53:53Z)
• Approximate Weighted First-Order Model Counting: Exploiting Fast Approximate Model Counters and Symmetry [16.574508244279098]
  We present ApproxWFOMC, a novel anytime method for efficiently bounding the weighted first-order model count. The algorithm has applications to inference in a variety of first-order probabilistic representations. We show how our algorithm outperforms existing approximate and exact techniques for inference in first-order probabilistic models.
  arXiv  Detail & Related papers  (2020-01-15T12:21:06Z)
• Polynomial-Time Exact MAP Inference on Discrete Models with Global Dependencies [83.05591911173332]
  junction tree algorithm is the most general solution for exact MAP inference with run-time guarantees. We propose a new graph transformation technique via node cloning which ensures a run-time for solving our target problem independently of the form of a corresponding clique tree.
  arXiv  Detail & Related papers  (2019-12-27T13:30:29Z)

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.