One-sentence Summary

University of Manchester and Uniwersytet Opolski investigate how satisfiability problem instances spanning different computational complexity classes and grammatical constructs impact transformer-based language models' ability to learn inference rules, and conduct an empirical study on the distribution of natural language satisfiability problems to support faithful model evaluation.

Key Contributions

• The paper identifies English satisfiability fragments covering determiners, the copula, transitive verbs, relative clauses, and bound-variable anaphora, then constructs datasets sampled from empirically determined phase-change regions.
• The paper evaluates transformer-based language models on natural language satisfiability across fragments with different computational complexity and finds that model performance is noticeably affected by the underlying complexity of the satisfiability problem.
• The paper studies zero-shot performance on these satisfiability tasks and shows that models can fail to adjust to distribution shift and generalize beyond their training distribution, indicating that they may not disentangle dataset patterns from inferential rules.

Introduction

Transformer-based language models are often evaluated on natural language inference by testing whether they can recognize strictly logical entailments that do not rely on commonsense background knowledge. This matters because such tasks probe whether models can learn rules of inference, understand logical meaning, and emulate algorithmic reasoning.

Earlier neural studies of satisfiability and entailment mostly focused on propositional logic or narrowly defined artificial language fragments. This limits expressive power, keeps the underlying complexity mostly fixed at NP-complete problems, and often creates datasets that do not sample the hardest instances. The authors address this by defining English fragments linked to different first-order logic fragments, identifying phase-change regions to build challenging satisfiability datasets, and analyzing how computational complexity affects model performance, including in zero-shot settings.

Dataset

• The authors construct synthetic natural language satisfiability datasets for several language fragments. Each data point contains a set of sentences Φ from a fragment and a binary label, Y or N, indicating whether Φ is satisfiable.

• Data sources are not external corpora. The authors generate examples from language templates. Each sentence is created by choosing a fragment template and uniformly sampling common nouns and, where needed, transitive verbs.

• Each example set Φ has cardinality m. Sampling uses n1 common nouns and, for relational fragments, n2 transitive verbs. The generation process is repeated m times to form one input instance.

• Labels are generated automatically. The sentences are mapped to first-order logic formula templates, and the theorem prover Z3 determines satisfiability.

• The authors sample m, n1, and n2 only within an empirically determined critical region λ_L. This ensures the density ratios α = m / n1 and β = m / n2 fall within the critical region.

• For fragments S and W, training examples sample n1 from 6 to 16. For fragments ν, z, and A, training examples sample n1 from 3 to 8 and n2 from 3 to 8.

• For each language fragment, the authors build a balanced training set with 120K examples, an evaluation set with 10K examples, and a test set with 10K examples.

• The per-fragment datasets are used to fine-tune and evaluate transformer language models on natural language satisfiability.

• The datasets are balanced with equal numbers of satisfiable and unsatisfiable instances, and accuracy is used as the evaluation metric.

• To test whether simpler fragments help models generalize to complex ones, the authors also create joint datasets mixing examples from all fragments. These include 600K total examples with 120K per fragment and 120K total examples with 24K per fragment.

• To test scale-invariance and generalization, the authors evaluate models on datasets containing more predicates or variables than were present in the training data.

• For zero-shot evaluation, the authors generate smaller benchmark datasets. For S and W, they use n1 from 5 to 10. For ν, z, and A, they use n1 from 3 to 5 and n2 from 2 to 5.

• For zero-shot evaluation, they create 1200 problem instances per fragment and place them into prompts using a template-based prompting procedure.

Method

The authors formulate the task as a controlled evaluation of transformer-based language models on natural language inference over formalized fragments of English. The central methodological idea is to define several semantically closed language fragments, translate their sentences into first-order logic, generate challenging satisfiability instances near a phase-change boundary, and label each instance automatically using an external theorem prover. The resulting data are then used to fine-tune and evaluate TLMs on a binary logical decision problem.

The first component of the pipeline is the definition of language fragments. Each fragment is specified by a finite set of natural-language sentence templates, such as “Every p is a q,” “Some p is a q,” “No p is a q,” and “Some p is not a q,” where the schematic variables range over common nouns or, in stronger fragments, over transitive verbs and relative-clause structures. Each sentence template is paired with a first-order formula template that provides its truth-conditional semantics. For example, the basic quantified noun-phrase patterns can be translated as:

Universal sentences are interpreted without existential import. This semantic setup yields well-defined model-theoretic notions of validity and satisfiability. The studied fragments range from a controlled version of the classical syllogistic to richer languages involving relative clauses, transitive verbs, quantified object positions, and bound-variable anaphora. For a given fragment $\mathcal{L}$L, the authors study the decision problem $\operatorname{Sat}(\mathcal{L})$Sat(L), whose input is a finite set of sentences $\Phi$Φ, and whose output is whether $\Phi$Φ is satisfiable.

The second component addresses the need to present TLMs with instances that are genuinely difficult rather than trivially predictable. The authors observe that, analogously to propositional $k$k-SAT, many randomly generated logical instances are either almost certainly satisfiable or almost certainly unsatisfiable. In the noun-phrase fragments, the key parameter is the ratio

where $m$m is the number of sentences in the set $\Phi$Φ and $n_1$n1​ is the number of distinct common nouns used. When $\alpha$α is small, there are many degrees of freedom and satisfiability is likely; when $\alpha$α is large, constraints accumulate and satisfiability becomes unlikely. The challenging region occurs near the point where the probability of satisfiability is around $0.5$0.5. For fragments containing transitive verbs, the authors additionally introduce

where $n_2$n2​ is the number of distinct transitive verbs. In those cases, the phase-change region is a two-dimensional region in the $(\alpha,\beta)$(α,β) plane.

To operationalize this notion, the authors define the phase-change region $\lambda_{\mathcal{L}}$λL​ for each fragment $\mathcal{L}$L as the set of parameter combinations for which the empirical probability of satisfiability lies in the interval $[0.35,0.65]$[0.35,0.65]. This interval is determined empirically by random sampling. Data points are then generated only when their $(\alpha,\beta)$(α,β) coordinates, or in noun-only fragments their $\alpha$α coordinate, fall within $\lambda_{\mathcal{L}}$λL​. This filtering step is crucial because uniform sampling over all parameters would produce many instances whose answers can be guessed from simple statistical regularities rather than from logical structure.

The data-construction module turns filtered parameter combinations into concrete supervised examples. For each example, the system samples $n_1$n1​ common nouns and, for verb-containing fragments, $n_2$n2​ transitive verbs. It then samples sentence templates from the grammar of the target fragment and instantiates their schematic variables using the sampled nouns and verbs. Repeating this process $m$m times produces a set of sentences $\Phi=\{\phi_1,\ldots,\phi_m\}$Φ={ϕ1​,…,ϕm​}. The corresponding first-order formula templates are also generated from the same template list and the same sampled vocabulary.

The label for each sentence set is produced automatically by applying the Z3 theorem prover to the translated first-order representation. If Z3 determines that the formula set is satisfiable, the data point receives the label Y; otherwise it receives the label N. This creates a large-scale dataset of natural-language inference problems with machine-verified logical ground truth. For each fragment, the authors construct a training set of 120K examples, an evaluation set of 10K examples, and a test set of 10K examples. The same protocol is designed to be reusable for any language fragment defined through sentence and formula templates.

The TLM training procedure uses these datasets for supervised fine-tuning. The model is provided with the natural-language sentences of $\Phi$Φ as input and is trained to predict the satisfiability label associated with that set. Because the inputs and labels are generated directly from the formal fragment, the supervision signal reflects logical validity or satisfiability rather than surface stylistic cues. The authors also evaluate zero-shot and prompt-based settings by constructing additional problem instances from the same fragments, selecting noun and verb sets from specified ranges, and embedding the sentences into a template-based prompt. The theorem prover supplies the target label for evaluation. Thus, the overall method combines formal semantic scaffolding, phase-change-aware instance filtering, automated theorem-prover labeling, and controlled fine-tuning or prompting of TLMs on logic-relevant natural language tasks.

Experiment

The study evaluates transformer language models on natural language satisfiability by fine-tuning T5 and DeBERTa on balanced language fragments, jointly mixing fragments, and testing unseen predicate counts, while also probing ChatGPT, GPT-4, and LLaMA-2 in zero-shot settings. Fine-tuned models handle simpler fragments more effectively, but performance declines as logical and linguistic complexity increases, and joint training helps complex fragments only when the data volume is sufficient. The models generally fail to generalize to larger instances, while zero-shot models, especially GPT-4, achieve only modest gains over chance and remain sensitive to prompt format and variable count, suggesting they do not reliably learn the underlying rules of inference.

Two natural-language logic examples show that small changes in quantified statements can turn a contradiction into a consistent scenario. The accompanying experiment reports GPT-4 as the strongest among the evaluated models and the only one clearly above random guessing. Reported accuracy also falls when problems use more variables, suggesting growing difficulty from larger search spaces and longer inputs. One example is unsatisfiable because a scholar must both love a musician and avoid loving every musician. Another example is satisfiable by assuming scholars exist, all artists are musicians, and everyone loves one another. GPT-4 is described as outperforming the other evaluated models and being better at strict output formatting.

Fine-tuned transformer language models solve natural language satisfiability problems more accurately in simpler fragments than in harder fragments. Their accuracy drops most sharply when moving from the simplest fragment to the next fragment and then declines more gradually as complexity increases. The two evaluated models show broadly similar behavior, indicating that computational complexity rather than model choice mainly shapes performance. Accuracy is highest on the simplest fragment and lowest on the most complex fragment. The performance gap is largest between the simplest and next fragments, while later declines are smaller.

A larger mixed training dataset improves test accuracy on every language fragment when T5-large is trained on instances from all fragments. The accuracy gains from using more training data are consistent across fragments, while performance across fragments remains fairly close. The 600K mixed training variant outperforms the 120K variant on all reported fragments. Training on data from all fragments yields comparable accuracy across the different fragments rather than large fragment-specific differences.

When T5-large is trained on smaller problem sizes and evaluated on larger ones, its accuracy does not transfer well. The decline appears across all language fragments, including fragments where the model previously achieved relatively high accuracy, indicating limited systematic generalization. Accuracy drops when evaluated on problems with more predicates and clauses than those seen during training. The failure to generalize is not limited to the most complex fragments. The results suggest that T5-large relies more on training-distribution patterns than on learned inference rules.

The experiments evaluate model performance on natural-language satisfiability tasks, including quantified reasoning examples and increasingly complex language fragments. GPT-4 outperforms the evaluated models and is the only one clearly above random guessing, while accuracy generally declines as problems involve more variables and greater logical complexity. Training on a larger mixed dataset improves performance across fragments and reduces fragment-specific differences, whereas training on smaller problem sizes and evaluating on larger ones leads to substantial drops, indicating limited systematic generalization.