Identifying the limits of transformers when performing model-checking with natural language (2023)

Abstract: Can transformers learn to comprehend logical semantics in natural language? Although many strands of work on natural language inference have focussed on transformer models’ ability to perform reasoning on text, the above question has not been answered adequately. This is primarily because the logical problems that have been studied in the context of natural language inference have their computational complexity vary with the logical and grammatical constructs within the sentences. As such, it is difficult to access whether the difference in accuracy is due to logical semantics or the difference in computational complexity. A problem that is much suited to address this issue is that of the model-checking problem, whose computational complexity remains constant (for fragments derived from first-order logic). However, the model-checking problem remains untouched in natural language inference research. Thus, we investigated the problem of model-checking with natural language to adequately answer the question of how the logical semantics of natural language affects transformers’ performance. Our results imply that the language fragment has a significant impact on the performance of transformer models. Furthermore, we hypothesise that a transformer model can at least partially understand the logical semantics in natural language but can not completely learn the rules governing the model-checking algorithm.

## introduction recent years have seen a surge of interest in the application of neural networks to the topic of natural language inference @xcite @xcite , the central task of which is to recover information entailed by, but not explicitly stated in natural language texts @xcite @xcite 1 dataset and code available at https://github.com/ itharindu/reasoning-withing-a-structure @xcite . this problem is of theoretical (as well as practical) interest because the ability to understand the logical consequences of natural language sentences is an essential part of what it is to understand the grammatical constructions and closed-class expressions they contain. more specifically, the ability of neural network models to recognize logical entailments is constitutive of their ability to understand the texts they are processing. it is important to distinguish two strands of work in this area. the first focuses on entailment as defined by human-constructed datasets @xcite , where the inferences depend on implicit background knowledge and have a probabilistic character. the second focuses on the recognition of formal logical entailments, for which data sets can be machinegenerated using existing symbolic reasoning techniques @xcite @xcite . this latter strand of work is particularly pertinent to the theoretical problem of whether neural network models can learn the logical semantics of natural language. commonsense knowledge, human judgement and considerations of plausibility are consciously excluded. a logical problem of great theoretical interest that has not been studied in the context of natural language inference is the model-checking problem: given a formula ϕ and a structure a, determine whether ϕ is true in a (a |= ψ). the ability to perform model-checking is indicative of a grasp of the logical semantics of the expressions concerned. in the context of natural language inference, we are particularly interested in a variant of the modelchecking problem where the structure and the formula are interpreted in natural language. it is noteworthy to emphasise how the model-checking problem differs from other inference problems. in other logical reasoning problems such as satisfiability, computational complexity varies among multiple figure 1 : an instance of the model-checking problem, the domain of the structure is represented in d, and predicates are characterised by p. a formula can be valid or not according to the structure (the formula on the left is valid, while the one on the right is invalid). corresponding natural language representations for both the structure and the formula are also presented. figure 1 depicts an instance of the modelchecking problem, where the sentence "some actors love every scholar" is true according to the structure presented, as the assignment of "hailee" to the variable x makes the corresponding formula (∃x(actor(x) ∧ ∀y(scholar(y) ⇒ love(x, y)))) t rue. however, when assessing the sentence "all actors who are happy are scholars", there is no assignment that makes the formula (∀x((actor(x) ∧ happy(x)) ⇒ scholar(x))) t rue according to the structure (the set of actors who are musicians is {hailee}, which is not a subset of scholars', namely {alan, tony}). in our analysis of transformers' capabilities in the model-checking problem, we ask two fundamental questions, (1) can transformers perform model-checking with natural language? (2) if so, can transformers understand the logical seman-tics of natural language: i.e. can transformers comprehend the semantics of distinctively logical words and grammatical concepts such as determiners, relative clauses and anaphora? to answer the above-mentioned questions, we construct a modelchecking dataset (fo 2 -mc dataset) utilising language fragments. unlike the work by @xcite and @xcite , whose work was limited to only one language fragment, we explore a varied set of fragments. the consideration of linguistic complexity of language fragments led us to ask an additional question: how does the linguistic complexity of the fragment affect the performance of the transformer model when performing model-checking with natural language? the contributions of this paper are as follows: (1) to the best of our knowledge, we are the first to broaden natural language reasoning over formal theories to include model-checking with natural language; (2) we develop a novel algorithm for constructing a dataset for model-checking with natural language; (3) we investigate whether transformers can learn to understand the logical semantics of natural language; (4) in a first-of-its-kind study in rule reasoning, we include complex fragments such as anaphora and relative clauses with transitive verbs; and (5) we provide a systematic analysis of how the linguistic complexity of language fragments affects rule reasoning. ## related work our work follows the literature on evaluating neural approaches, especially transformer models on deductive and linguistic reasoning tasks @xcite @xcite @xcite . moreover, it is also related to other research approaches that have been conducted on data synthesis for rule reasoning problems @xcite @xcite . however, our study is distinct from the above-mentioned work in two ways. firstly, we focus on an unexplored problem space, modelchecking with natural language. secondly, unlike the above literature, we explore multiple language fragments and provide a deconstruction of how the linguistic complexity of language fragments affects the performance of transformer models in a rule reasoning task. our work can also be viewed as broadening the research conducted on training neural networks to perform algorithmic tasks, including learning to solve sat problems @xcite , propositional inference @xcite , semantic parsing @xcite , symbolic integration @xcite ) and natural theorem proving @xcite @xcite . in our study, we aim to investigate the transformers' ability to emulate the algorithm governing the modelchecking problem and comprehend the logical semantics of natural language. when defining language fragments, we follow the definition set out by @xcite @xcite , who described it more precisely as a subset of a language equipped with semantics that translates sentences into a formal system such as first-order logic. moreover we employ their work on fragments of firstorder logic as the foundation when constructing the dataset. notably, @xcite has investigated the complexity of fragments' first-order logic, and we limit our analysis in this paper to fragments that have been examined in that study. moreover, we also closely follow the cognitive science literature on model-checking and quantifier verification @xcite @xcite when defining our experimental evaluation. it provides us with a baseline to compare results from transformer models with the empirical studies that have been conducted with humans. ## data construction to decide whether transformer models can learn to understand logical semantics of natural language from formulae (sentences) and structures represented in natural language, we developed an algorithm (shown in algorithm 1) to construct a balanced dataset designed to be free from trivial linguistic patterns that are easily exploitable. this section will outline the data construction methodology in detail. we sample a set of words (proper nouns prn, nouns n, verbs vb, adjectives adj) from a predefined vocabulary (v ′ ) to form a list of words v. the proper nouns in v are used to define the domain d of the structure, while the nouns, verbs and adjectives are used for defining the set of predicates p. when generating sentences, we follow a template-based approach. a language template is a sentence of natural language with open-clause words replaced by schematic variables; for example, some n 1 v is every n 2 . through substitution of vocabulary items of the appropriate category, we can generate natural language sentences, i.e., some artists admire every doctor. a simple way of defining a fragment of natural language (language fragment) is via a finite set of template sentences. for example, the classical syllogistic fragment can be defined as the sentences confirming the sentence schemata, all n 1 are n 2 , some n 1 is n 2 , no n 1 are n 2 and some n 1 are not n 2 . the formula template is a formula of first-order logic with non-logical symbols replaced by schematic variables; for example, ∃x( let φ l denote the set of first-order formula templates that can be translated to natural language templates l. given a language fragment l and a vocabulary v, we can obtain a set of formulae φ l (v), such that φ l (v) is a fragment of first-order logic over the vocabulary v, i.e., φ l (v) only contains the vocabulary v. the first-order formula ϕ is selected from the φ l (v), and then the formula ϕ is translated to a natural language sentence s ϕ using a template l. a summary of the language fragments we used in our evaluation is provided in the next section. ## experimental setup in this section, we describe the experiments we conducted in order to address our research questions. ## conclusion we investigate the limits of transformers in an unexplored problem space of model-checking with natural language employing language fragments. we use five different language fragments and explore how linguistic complexity and other linguistic properties such as boolean coordinators affect rule reasoning in transformer models. in a broader sense, our study is to determine whether transformer models can learn to understand the logical semantics of natural language and emulate the model-checking algorithm. we posit that transformers can learn logically significant words and grammatical constructs but fall short when learning the underlying algorithm. moreover, different linguistic properties such as the language fragment, boolean coordinators and the number of quantifiers have a notable impact on the learning ability of the transformers. thus, an interesting future direction would be to investigate how these linguistic properties affect more complex reasoning tasks like natural language satisfiability.