Natural Language Satisfiability: Exploring the Problem Distribution and Evaluating Transformer-based Language Models (2024)

Abstract: Efforts to apply transformer-based language models (TLMs) to the problem of reasoning in natural language have enjoyed ever-increasing success in recent years. The most fundamental task in this area to which nearly all others can be reduced is that of determining satisfiability. However, from a logical point of view, satisfiability problems vary along various dimensions, which may affect TLMs’ ability to learn how to solve them. The problem instances of satisfiability in natural language can belong to different computational complexity classes depending on the language fragment in which they are expressed. Although prior research has explored the problem of natural language satisfiability, the above-mentioned point has not been discussed adequately. Hence, we investigate how problem instances from varying computational complexity classes and having different grammatical constructs impact TLMs’ ability to learn rules of inference. Furthermore, to faithfully evaluate TLMs, we conduct an empirical study to explore the distribution of satisfiability problems.

## introduction the impressive performance of transformer-based language models (tlms) in natural language inference tasks @xcite @xcite has created a surge of interest in the development of linguistic and deductive reasoning benchmarks to evaluate these models @xcite @xcite . one such area of interest is the ability to recognise valid entailments, understood in a strictly logical sense @xcite , where the inference does not depend on background knowledge and commonsense. the ability of tlms to understand this type of entailment is indicative of their ability to learn rules of inference, understand the logical semantics of natural language and emulate complex algorithms. since the inferences we shall be concerned with do not depend on background knowledge or intuitive plausibility, they can be captured using the apparatus of formal logic. logicians usually find it convenient to reconstruct entailment in terms of satisfiability: a set of formulae φ is satisfiable if there is a structure (in the model-theoretic sense) a such that every formula of φ is true in a. a set of formulae φ entails a formula ψ just in case φ ∪ {¬ψ} is not satisfiable. the same duality holds for natural language (which incorporates a concept of negation) just as it does for formal logic. thus, we consider the following problem: given a collection of sentences expressed in a natural language such as english, determine whether it is-in a strictly logical sense-satisfiable. figure 1 illustrates two instances of the satisfiability problem in english, one positive and one negative. note that any method for determining satisfiability yields a method for recognising entailments and vice versa. we approach this problem in a controlled way. the sentences in figure 1 feature only rudimentary grammatical resources: the determiners some, no and all, transitive verbs with unqualified nounphrases as subjects and objects, and the copula is. it is well-known from formal logic that the computational complexity of the satisfiability problem for a logic depends on its expressive power. for example, the satisfiability problem for propositional logic (known as sat) is nptime-complete, but the corresponding problem for the two-variable fragment of first-order logic is nexptime-complete, while for the whole of first-order logic is r.e.-complete (i.e. undecidable); for a survey, see @xcite . the same is true when it comes to fragments of natural languages @xcite @xcite , as we explain presently. the question therefore arises as to how tlms' ability to learn rules of inference is affected by the fragment of language within which they operate. figure 1 : the table depicts two instances of a satisfiability problem; one is unsatisfiable while the other is satisfiable. in the first example, the first two formulae imply ∀x(scholar(x) → ∃y(musicians(y) ∧ love(x, y))), while the last formula is ∃x(scholar(x) ∧ ∀y(musician(y) → ¬love(x, y)))-a direct contradiction, hence unsatisfiable. in the the second example (satisfiable), a structure a can be easily found that makes all formulae t rue: imagine, for instance, a world where scholars exist, all musicians are artists, and everyone loves everyone. in recent years, researchers have analysed the limitations of various neural approaches when solving satisfiability problems @xcite @xcite , including natural language satisfiability problems @xcite . however, in all cases, the problems are in propositional logic or its close relatives, and as such, the expressive power of the expressions or sentences is limited. moreover, it restricts the problem space to be in a single computational complexity class, np-complete. we overcome these limitations by generating sentences from various fragments of english that are related to more varied fragments of first-order logic. by utilising language fragments of varying expressive power, we also provide an analysis of how computational complexity affects tlms' ability to grasp the rules governing logical entailment. when investigating tlms' ability to solve instances of natural language satisfiability problems, it is important to ensure that the training and test data sets include a sufficient number of challenging problem instances. the difficulty is that randomly constructed sets of formulae (or sentences) are, depending on the sampling parameters, in many cases easily seen either to be satisfiable or to be unsatisfiable, a situation dramatically illustrated in the case of propositional logic satisfiability @xcite @xcite , where challenging problems occur only when the ratio of clauses to propositional variables is close to a critical threshold, i.e., the so-called phase-change region. in this region, where the probability of a randomly generated problem instance is close to 0.5, algorithms for determining satisfiability typically exhibit long running times. therefore, to demonstrate that tlms can learn rules of inference, we must ensure that they work on the hardest region of the target problem space. indeed, recent work has shown some pitfalls associated with synthetic data due to undersampling challenging problems @xcite . consequently, we conduct an empirical study to determine, for each of the language fragments investigated, the relevant "phase-change" region where the challenging problem instances are to be found. the contributions of this paper are as follows. (1) we identify a number of fragments of english featuring a range of logico-syntactic constructions involving determiners, the copula, transitive verbs, relative clauses and bound-variable anaphora. (2) we empirically determine the phase-change region for these fragments and construct data sets containing instances of the satisfiability problems sampled from these regions. (3) we investigate the ability of transformer-based language models to solve the satisfiability problem for the investigated fragments and carry out a systematic analysis of how the underlying computational complexity of the satisfiability problem correlates with tlms' ability to grasp the relevant inferential principles. (4) furthermore, we explore the proficiency of tlms in solving instances of the satisfiability problem within a zero-shot context. to the best of our knowledge, this investigation represents the first attempt to probe the behaviour of tlms in zero-shot scenarios with respect to their efficacy in solving satisfiability problems. ## related work our work closely follows the literature on identifying strengths and weaknesses of neural approaches, including transformer-based language models on deductive reasoning tasks @xcite @xcite . neural networks, particularly graph neural networks (gnn), have been utilised to solve satisfiability problem in-stances @xcite . as mentioned in the introduction, various studies have extended that work to natural language satisfiability, utilizing tlms instead of gnns @xcite . however, the sentences considered fail to exercise the full range of inference patterns licenced by commonly encountered grammatical constructions. moreover, in each case, the underlying satisfiability problems were derived from that for propositional logic (i.e. sat), thus, confining attention to a single problem type. indeed in the case of natural language satisfiability, the sentences are sometimes hardly natural-sounding. for example, the grounded rule language (grl) fragment introduced in @xcite includes sentences such as "if carrot and not steak then apples". our work can also be viewed as an attempt to identify various limitations that affect tlms' ability to emulate algorithms. there have been numerous studies of tlms' ability to solve algorithmic tasks, including sat-solving @xcite , semantic parsing @xcite , modelchecking @xcite , theorem proving @xcite @xcite etc. we extend this work to a family of related problems spanning multiple computational complexity classes, thus, providing a breakdown of the impact of computational complexity on tlms' ability to solve algorithmically challenging problems. ## conclusion we have investigated transformer-based language models' ability to solve instances of natural language problems belonging to different language fragments with varying computational complexity. our investigation demonstrated that the computational complexity of the fragment has a noticeable effect on tlms' ability to perform a logical inferential task. even in a simpler language fragment for which the transformer models achieved a reasonable performance, the model failed to adjust to distribution shift and generalise beyond its training distribution. thus, we posit that tlms do not reliably disentangle the patterns that exist within the dataset and the rules of inference needed when determining satisfiability. therefore, it is imperative to acknowledge that a considerable body of research remains to be conducted in order to enhance the capacity of these models to comprehend rules of inference. we also acknowledge that the generalisation aspect of tlms may need a deeper analysis, which we leave for future work.