Learning Better Representations From Less Data For Propositional Satisfiability

• URL: http://arxiv.org/abs/2402.08365v2
• Date: Wed, 29 May 2024 13:47:14 GMT
• Title: Learning Better Representations From Less Data For Propositional Satisfiability
• Authors: Mohamed Ghanem, Frederik Schmitt, Julian Siber, Bernd Finkbeiner,
• Abstract summary: We present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability. Our model learns better representations than models trained for classification only, with a much higher data efficiency. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.
• Score: 7.449724123186386
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by ~32% after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

Related papers

• Rethinking Classifier Re-Training in Long-Tailed Recognition: A Simple Logits Retargeting Approach [102.0769560460338]
  We develop a simple logits approach (LORT) without the requirement of prior knowledge of the number of samples per class. Our method achieves state-of-the-art performance on various imbalanced datasets, including CIFAR100-LT, ImageNet-LT, and iNaturalist 2018.
  arXiv  Detail & Related papers  (2024-03-01T03:27:08Z)
• Boosting Low-Data Instance Segmentation by Unsupervised Pre-training with Saliency Prompt [103.58323875748427]
  This work offers a novel unsupervised pre-training solution for low-data regimes. Inspired by the recent success of the Prompting technique, we introduce a new pre-training method that boosts QEIS models. Experimental results show that our method significantly boosts several QEIS models on three datasets.
  arXiv  Detail & Related papers  (2023-02-02T15:49:03Z)
• HyperImpute: Generalized Iterative Imputation with Automatic Model Selection [77.86861638371926]
  We propose a generalized iterative imputation framework for adaptively and automatically configuring column-wise models. We provide a concrete implementation with out-of-the-box learners, simulators, and interfaces.
  arXiv  Detail & Related papers  (2022-06-15T19:10:35Z)
• CAFA: Class-Aware Feature Alignment for Test-Time Adaptation [50.26963784271912]
  Test-time adaptation (TTA) aims to address this challenge by adapting a model to unlabeled data at test time. We propose a simple yet effective feature alignment loss, termed as Class-Aware Feature Alignment (CAFA), which simultaneously encourages a model to learn target representations in a class-discriminative manner.
  arXiv  Detail & Related papers  (2022-06-01T03:02:07Z)
• Training Data Subset Selection for Regression with Controlled Generalization Error [19.21682938684508]
  We develop an efficient majorization-minimization algorithm for data subset selection. SELCON trades off accuracy and efficiency more effectively than the current state-of-the-art.
  arXiv  Detail & Related papers  (2021-06-23T16:03:55Z)
• BiFair: Training Fair Models with Bilevel Optimization [8.2509884277533]
  We develop a new training algorithm, named BiFair, which jointly minimizes for a utility, and a fairness loss of interest. Our algorithm consistently performs better, i.e., we reach to better values of a given fairness metric under same, or higher accuracy.
  arXiv  Detail & Related papers  (2021-06-03T22:36:17Z)
• Less is More: Data-Efficient Complex Question Answering over Knowledge Bases [26.026065844896465]
  We propose the Neural-Symbolic Complex Question Answering (NS-CQA) model, a data-efficient reinforcement learning framework for complex question answering. Our framework consists of a neural generator and a symbolic executor that transforms a natural-language question into a sequence of primitive actions. Our model is evaluated on two datasets: CQA, a recent large-scale complex question answering dataset, and WebQuestionsSP, a multi-hop question answering dataset.
  arXiv  Detail & Related papers  (2020-10-29T18:42:44Z)
• Modeling Token-level Uncertainty to Learn Unknown Concepts in SLU via Calibrated Dirichlet Prior RNN [98.4713940310056]
  One major task of spoken language understanding (SLU) in modern personal assistants is to extract semantic concepts from an utterance. Recent research collected question and answer annotated data to learn what is unknown and should be asked. We incorporate softmax-based slot filling neural architectures to model the sequence uncertainty without question supervision.
  arXiv  Detail & Related papers  (2020-10-16T02:12:30Z)
• A Neural Network Approach for Online Nonlinear Neyman-Pearson Classification [3.6144103736375857]
  We propose a novel Neyman-Pearson (NP) classifier that is both online and nonlinear as the first time in the literature. The proposed classifier operates on a binary labeled data stream in an online manner, and maximizes the detection power about a user-specified and controllable false positive rate. Our algorithm is appropriate for large scale data applications and provides a decent false positive rate controllability with real time processing.
  arXiv  Detail & Related papers  (2020-06-14T20:00:25Z)
• The Right Tool for the Job: Matching Model and Instance Complexities [62.95183777679024]
  As NLP models become larger, executing a trained model requires significant computational resources incurring monetary and environmental costs. We propose a modification to contextual representation fine-tuning which, during inference, allows for an early (and fast) "exit" We test our proposed modification on five different datasets in two tasks: three text classification datasets and two natural language inference benchmarks.
  arXiv  Detail & Related papers  (2020-04-16T04:28:08Z)
• PrIU: A Provenance-Based Approach for Incrementally Updating Regression Models [9.496524884855559]
  This paper presents an efficient provenance-based approach, PrIU, for incrementally updating model parameters without sacrificing prediction accuracy. We prove the correctness and convergence of the incrementally updated model parameters, and validate it experimentally. Experimental results show that up to two orders of magnitude speed-ups can be achieved by PrIU-opt compared to simply retraining the model from scratch, yet obtaining highly similar models.
  arXiv  Detail & Related papers  (2020-02-26T21:04:06Z)

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.