The Computational Complexity of Formal Reasoning for Encoder-Only Transformers
- URL: http://arxiv.org/abs/2405.18548v1
- Date: Tue, 28 May 2024 19:30:43 GMT
- Title: The Computational Complexity of Formal Reasoning for Encoder-Only Transformers
- Authors: Marco Sälzer, Eric Alsmann, Martin Lange,
- Abstract summary: We investigate challenges and possibilities of formal reasoning for encoder-only transformers (EOT)
We find that SAT is undecidable if we consider EOT, commonly considered in the expressiveness community.
Besides trivial cases, we find that quantized EOT, namely those restricted by some fixed-width arithmetic, lead to the decidability of SAT due to their limited attention capabilities.
- Score: 4.096453902709292
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We investigate challenges and possibilities of formal reasoning for encoder-only transformers (EOT), meaning sound and complete methods for verifying or interpreting behaviour. In detail, we condense related formal reasoning tasks in the form of a naturally occurring satisfiability problem (SAT). We find that SAT is undecidable if we consider EOT, commonly considered in the expressiveness community. Furthermore, we identify practical scenarios where SAT is decidable and establish corresponding complexity bounds. Besides trivial cases, we find that quantized EOT, namely those restricted by some fixed-width arithmetic, lead to the decidability of SAT due to their limited attention capabilities. However, the problem remains difficult, as we establish those scenarios where SAT is NEXPTIME-hard and those where we can show that it is solvable in NEXPTIME for quantized EOT. To complement our theoretical results, we put our findings and their implications in the overall perspective of formal reasoning.
Related papers
- QSETH strikes again: finer quantum lower bounds for lattice problem,
strong simulation, hitting set problem, and more [5.69353915790503]
There are problems for which there is no trivial' computational advantage possible with the current quantum hardware.
We would like to have evidence that it is difficult to solve those problems on quantum computers; but what is their exact complexity?
By the use of the QSETH framework [Buhrman-Patro-Speelman 2021], we are able to understand the quantum complexity of a few natural variants of CNFSAT.
arXiv Detail & Related papers (2023-09-28T13:30:20Z) - Learnability with PAC Semantics for Multi-agent Beliefs [38.88111785113001]
The tension between deduction and induction is perhaps the most fundamental issue in areas such as philosophy, cognition and artificial intelligence.
Valiant recognised that the challenge of learning should be integrated with deduction.
Although weaker than classical entailment, it allows for a powerful model-theoretic framework for answering queries.
arXiv Detail & Related papers (2023-06-08T18:22:46Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning.
The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
arXiv Detail & Related papers (2022-10-04T09:19:13Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques.
We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
arXiv Detail & Related papers (2022-03-02T05:14:12Z) - Pushing the Limits of Rule Reasoning in Transformers through Natural
Language Satisfiability [30.01308882849197]
We propose a new methodology for creating challenging algorithmic reasoning datasets.
Key idea is to draw insights from empirical sampling of hard propositional SAT problems and from complexity-theoretic studies of language.
We find that current transformers, given sufficient training data, are surprisingly robust at solving the resulting NLSat problems.
arXiv Detail & Related papers (2021-12-16T17:47:20Z) - Generalization of Neural Combinatorial Solvers Through the Lens of
Adversarial Robustness [68.97830259849086]
Most datasets only capture a simpler subproblem and likely suffer from spurious features.
We study adversarial robustness - a local generalization property - to reveal hard, model-specific instances and spurious features.
Unlike in other applications, where perturbation models are designed around subjective notions of imperceptibility, our perturbation models are efficient and sound.
Surprisingly, with such perturbations, a sufficiently expressive neural solver does not suffer from the limitations of the accuracy-robustness trade-off common in supervised learning.
arXiv Detail & Related papers (2021-10-21T07:28:11Z) - Design of quantum optical experiments with logic artificial intelligence [1.6114012813668934]
We propose the use of logic AI for the design of optical quantum experiments.
We show how to map into a SAT problem the experimental preparation of an arbitrary quantum state.
We find that the use of logic AI improves significantly the resolution of this problem.
arXiv Detail & Related papers (2021-09-27T18:01:08Z) - From LSAT: The Progress and Challenges of Complex Reasoning [56.07448735248901]
We study the three challenging and domain-general tasks of the Law School Admission Test (LSAT), including analytical reasoning, logical reasoning and reading comprehension.
We propose a hybrid reasoning system to integrate these three tasks and achieve impressive overall performance on the LSAT tests.
arXiv Detail & Related papers (2021-08-02T05:43:03Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems.
In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
arXiv Detail & Related papers (2021-07-15T04:47:35Z) - Comprehensible Counterfactual Explanation on Kolmogorov-Smirnov Test [56.5373227424117]
We tackle the problem of producing counterfactual explanations for test data failing the Kolmogorov-Smirnov (KS) test.
We develop an efficient algorithm MOCHE that avoids enumerating and checking an exponential number of subsets of the test set failing the KS test.
arXiv Detail & Related papers (2020-11-01T06:46:01Z)
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.