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

• Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints [0.0]
  We introduce and benchmark a local search for the NP-complete satisfiability problem 3-SAT.<n>Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima.<n>We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N=15000.
  arXiv  Detail & Related papers  (2025-06-18T18:00:01Z)
• Critical Thinking: Which Kinds of Complexity Govern Optimal Reasoning Length? [72.70486097967124]
  We formalize a framework using deterministic finite automata (DFAs) We show that there exists an optimal amount of reasoning tokens such that the probability of producing a correct solution is maximized. We then demonstrate an implication of these findings: being able to predict the optimal number of reasoning tokens for new problems and filtering out non-optimal length answers results in consistent accuracy improvements.
  arXiv  Detail & Related papers  (2025-04-02T17:45:58Z)
• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• Solving the Challenge Set without Solving the Task: On Winograd Schemas as a Test of Pronominal Coreference Resolution [21.19369044026899]
  We show that despite the strong performance of prompted language models (LMs) on the Winograd Challenge set, these same modeling techniques perform relatively poorly at resolving certain pronominal ambiguities attested in OntoNotes. We propose a method for ensembling a prompted LM with a supervised, task-specific system that is overall more accurate at resolving pronominal coreference across datasets.
  arXiv  Detail & Related papers  (2024-10-12T09:04:53Z)
• 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)
• A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation [1.5201992393140886]
  We develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. We have proved the correctness of our approaches and demonstrated them in simulations.
  arXiv  Detail & Related papers  (2023-08-07T06:52:06Z)
• Evolutionary Diversity Optimisation in Constructing Satisfying Assignments [20.386139395296215]
  This paper studies the Boolean satisfiability problem (SAT) in the context of EDO. SAT is of great importance in computer science and differs from the other problems studied in EDO literature, such as KP and TSP. We introduce evolutionary algorithms employing a well-known SAT solver to maximise diversity among a set of SAT solutions explicitly.
  arXiv  Detail & Related papers  (2023-05-19T06:26:10Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  The amplitude amplification algorithm can be applied to unstructured search for satisfying variable assignments. The Quantum Approximate Optimization Algorithm (QAOA) is a promising candidate for solving 3SAT for Noisy Intermediate-Scale Quantum devices. We introduce amplitude amplification-inspired variants of QAOA to improve the success probability for 3SAT.
  arXiv  Detail & Related papers  (2023-03-02T11:52:39Z)
• Circuit Complexity through phase transitions: consequences in quantum state preparation [0.0]
  We analyze the circuit complexity for preparing ground states of quantum many-body systems. In particular, how this complexity grows as the ground state approaches a quantum phase transition.
  arXiv  Detail & Related papers  (2023-01-11T19:00:10Z)
• 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)
• 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)
• Pareto Probing: Trading Off Accuracy for Complexity [87.09294772742737]
  We argue for a probe metric that reflects the fundamental trade-off between probe complexity and performance. Our experiments with dependency parsing reveal a wide gap in syntactic knowledge between contextual and non-contextual representations.
  arXiv  Detail & Related papers  (2020-10-05T17:27:31Z)

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.