PaperlayerView exact revision on arXiv

Source-linked AI summary

Can Neural Networks Understand Logical Entailment?

Richard Evans, David Saxton, David Amos, Pushmeet Kohli, Edward Grefenstette

arXiv:1802.08535v1cs.NEcs.AI

TL;DR

The paper investigates whether neural networks can understand logical formulae well enough to detect entailment and which architectures best handle purely structural sequence problems. The authors create a controlled logical-entailment dataset, compare popular neural architectures, and introduce PossibleWorldNet, which evaluates formulas across imagined possible worlds. PossibleWorldNet achieves 99.3% accuracy on test (easy) and 97.3% on test (hard), significantly outperforming the other models.

  • Problem

    The paper investigates whether neural networks can understand logical formulae well enough to detect entailment and which architectures best handle purely structural sequence problems.

  • Method

    The authors create a controlled logical-entailment dataset, compare popular neural architectures, and introduce PossibleWorldNet, which evaluates formulas across imagined possible worlds.

  • Results

    PossibleWorldNet achieves 99.3% accuracy on test (easy) and 97.3% on test (hard), significantly outperforming the other models.

  • Takeaways & Limitations

    Architectures with explicit structural bias perform better on this task, and the strongest results come from biasing the model toward possible-world semantics.

  • Takeaways & Limitations

    PossibleWorldNet considers at most 256 worlds, versus averages exceeding 3,000 assignments in the big set and 800,000 in the massive set.

Abstract

from arXiv · show

We introduce a new dataset of logical entailments for the purpose of measuring models' ability to capture and exploit the structure of logical expressions against an entailment prediction task. We use this task to compare a series of architectures which are ubiquitous in the sequence-processing literature, in addition to a new model class---PossibleWorldNets---which computes entailment as a "convolution over possible worlds". Results show that convolutional networks present the wrong inductive bias for this class of problems relative to LSTM RNNs, tree-structured neural networks outperform LSTM RNNs due to their enhanced ability to exploit the syntax of logic, and PossibleWorldNets outperform all benchmarks.

1 INTRODUCTION

The paper introduces logical entailment as a testbed for whether neural networks capture and exploit structural information, comparing popular architectures with a new PossibleWorldNet model.

  • Motivation: The paper asks whether neural networks can detect logical entailment and which architectures best infer, encode, and relate features in structural sequence problems.It uses these questions to study architectural inductive biases concerning structure and abstraction.
  • Motivation: The testbed is intended to assess structural and abstract reasoning beyond reasoning based primarily on semantic representations.The broader goal is to support agents and classifiers that reason structurally.
  • Contributions: The authors introduce a dataset for training and evaluation, thoroughly evaluate existing neural models, and propose a PossibleWorldNet inspired by model-theoretic entailment.The new model evaluates formulas across multiple possible worlds and significantly outperforms the benchmarks.
  • Contributions: The dataset-generation process is designed to reduce superficial exploitable biases, while the experiments compare baseline architectures and the new model.The paper presents dataset construction, benchmark models, experiments, results, related work, and conclusions in sequence.

2 DATASET CREATION

The dataset encodes propositional entailment examples while controlling superficial differences between positive and negative cases, then creates increasingly difficult and varied evaluation splits.

  • Dataset definition: Logical entailment is represented as triples (A, B, A ⊨ B), labeled 1 when every model satisfying A also satisfies B and 0 otherwise.Examples include (p ∧ q, q, 1) and (q ∨ r, r, 0).
  • Dataset construction: The generation process balances classes and formula lengths while minimizing lexical and syntactic distributional differences between positive and negative examples.These constraints target superficial cues that trivial baselines could exploit.
  • Dataset construction: Four-tuples pair two positive entailments with cross-paired negative entailments so each formula appears once in each class.This arrangement minimizes crude structural differences between positive and negative examples.
  • Evaluation splits: The dataset includes easy, hard, big, massive, and exam splits that vary in formula complexity, variable count, operators, or textbook provenance.The massive split uses formulas with 20–26 variables and 20–30 operators, while the exam split contains 100 textbook-derived examples with mutated negatives.
  • Generalisation: Validation and test formulas are filtered to exclude α-equivalent training formulas, supporting evaluation on unseen structures rather than renamed duplicates.Formulas are converted to de-Bruijn form before filtering.
  • Generalisation: Training-time symbol permutation augmentation encourages models to treat entailments with renamed propositional variables as structurally equivalent.The same permutation is applied consistently to both sequents in each training example.

3 MODELS

The paper compares sequence, relational, and syntax-aware neural architectures for logical entailment, then introduces PossibleWorldNet as a model inspired by semantic entailment. Its central design evaluates both formulas across imagined worlds and combines those evaluations into an entailment decision.

  • 3.2 BENCHMARKS: Encoding models produce separate formula representations for an MLP, whereas relational models directly observe the expression pair and relate its substructures.This distinction separates models that compress each side independently from models that make decisions while traversing or comparing both expressions.
  • 3.2.1 ENCODER BENCHMARKS: Convolutional and LSTM encoders traverse formulas as sequences, while relational LSTM models process the concatenated sequent and its entailment separator.The convolutional encoder stacks one-dimensional convolutions, pooling, and fully connected layers; LSTM encoders use final recurrent states.
  • 3.2.1 ENCODER BENCHMARKS: TreeRNN and TreeLSTM encoders compose formula representations according to provided parse trees, allowing logical operators to determine the order of composition.TreeLSTMs adapt LSTM updates to capture long-range dependencies and propagate gradients through the tree.
  • 3.2.3 THE TRANSFORMER BENCHMARK: The Transformer benchmark concatenates the sequents, adds a learnable bias to the right sequent, and decodes one output position for entailment logits.The bias distinguishes the right sequent analogously to positional signals distinguishing sequence positions.
  • 3.3 THE POSSIBLEWORLDNET: PossibleWorldNet evaluates A and B across imagined worlds, combining their satisfaction values as a convolution over possible worlds.The model is inspired by the model-theoretic definition of entailment and improves as the number of imagined worlds increases.
  • 3.3 THE POSSIBLEWORLDNET: PossibleWorldNet does not encode constraints specific to propositional or formal logic, so its world-based procedure is proposed as potentially applicable to other logics and natural-language entailment.The paper frames this broader applicability as a speculation grounded in entailment’s semantic definition.

4 EXPERIMENTAL SETUP

The experiments use shared encoder parameters for both sides of each sequent and jointly train model-specific classifiers and embeddings. Hyperparameters are selected by grid search, repeated across random seeds, and evaluated using the associated training, validation, and test accuracies.

  • 4 EXPERIMENTAL SETUP: Each encoder shares parameters between the left and right sequents, while the binary classifier and symbol embeddings are model-specific and jointly trained.The classifier is re-initialized for each architecture before joint training.
  • 4 EXPERIMENTAL SETUP: Models are optimized with Adam and tested across learning rates, minibatch sizes, MLP depths, and layer sizes, with three random seeds per configuration.The search includes learning rates [1e−5, 1e−4, 1e−3] and minibatch sizes [64, 128].
  • 4 EXPERIMENTAL SETUP: The best model for each architecture is selected using validation results, and its training, validation, and test accuracies are recorded.Reported accuracies correspond to the selected model’s associated time step.

5 RESULTS AND DISCUSSION

PossibleWorldNet achieves the strongest performance by combining syntax-aware tree processing with evaluation across multiple possible worlds. Across benchmarks, structure-aware models outperform models that must infer sequence structure implicitly, while increasing sampled worlds steadily reduces validation error.

  • Benchmark comparisons: Tree-based models lead the benchmarks, with TreeLSTM best overall among benchmark models on both test sets.LSTM encoders are the strongest models without privileged syntax access, while convolutional and bidirectional LSTM encoders perform relatively poorly.
  • Benchmark comparisons: Permutation augmentation improves weaker models by 2–3 points and tree-based models by 7–15 points, indicating a particular fit with structure-aware representations.The authors relate this effect to capturing the arbitrariness of symbols denoting unbound variables.
  • Architectural inductive biases: Structure-aware models outperform models that must implicitly model sequence structure when syntax is explicit, unambiguous, and central to the task.Traversal models do not outperform encoding models here, suggesting their advantage may be more specific to long-range dependencies in textual entailment.
  • Overall results: 99.3% accuracy on test (easy) and 97.3% accuracy on test (hard) make PossibleWorldNet the best overall model.Its inductive bias combines access to syntactic structure with evaluation across many possible worlds.
  • PossibleWorldNet analysis: Validation error decreases steadily as the number of possible worlds increases, without increasing model parameters.The model therefore considers more possibilities while retaining the same parameter count; sampling 256 rows is estimated to find countermodels with 97.2% probability.
  • PossibleWorldNet analysis: PossibleWorldNet considers at most 256 worlds, versus averages exceeding 3,000 assignments in the big test set and 800,000 in the massive test set.Thus, its computation samples only 7% and 0.03% of the expected rows for those sets, respectively.

6 RELATED WORK

The paper situates its logical-entailment task among neural approaches to expression equivalence and textual entailment. It emphasizes that formal entailment isolates structural reasoning and differs from both equivalence classification and natural-language entailment.

  • Expression reasoning: Earlier work on matrix expressions and formula equivalence uses recursive networks, but differs in task definition and auxiliary information requirements.Zaremba et al. classify equivalent matrix expressions, while Allamanis et al. classify formula equivalence and may require exemplar members of unseen classes.
  • Expression reasoning: Prior recursive models learn expression equivalence, whereas this paper studies the asymmetric relation of entailment between formula pairs.The distinction matters because equivalence is symmetric while entailment is not.
  • Textual entailment: Natural-language textual entailment uses recurrent or convolutional models, but the paper argues that formal logic isolates the structural subproblem these systems may not reliably solve.The cited example shows neural models incorrectly identifying a sentence entailment, motivating a purely formal setting.

7 CONCLUSION

The paper finds that explicit structural modeling improves logical-entailment performance, while PossibleWorldNets perform best by encoding entailment's possible-world semantics. Convolutional networks appear poorly biased for heterogeneous, deeply structured syntax compared with LSTMs.

  • Explicitly structure-aware architectures significantly outperform models that must capture structure implicitly.
  • PossibleWorldNets are the best-performing models because they encode the possible-world semantics of entailment.
  • Convolutional networks may have the wrong inductive bias for exploiting heterogeneous, deeply structured syntax in formal and natural-language sequence problems.
  • The dataset provides a new evaluation point for neural models' ability to understand structural sequence problems.

A.1 DATASET REQUIREMENTS

The dataset is designed to prevent entailment models from succeeding through superficial statistical regularities. Its requirements balance classes and control lexical, syntactic, operator-level, and variable-related distributions, while excluding intuitionistic entailment.

  • Baseline models are included to verify that the generation process prevents one-sided or simple statistical information from solving entailment recognition.
  • The dataset uses balanced positive and negative classes so models seeing only one side of a sequent should perform near random.
  • Positive and negative examples are constrained to match formula lengths, operator counts, and operator positions across syntax-tree levels.
  • The requirements also match the number of new free variables between classes and exclude intuitionistic entailment by focusing on classical propositional logic.

A.2.1 A NAIVE APPROACH TO DATASET GENERATION

The naive generation strategy alternates positive and negative entailments, but creates exploitable differences in syntax, satisfiability, and new-variable counts. These differences enable simple heuristic baselines to perform well without modeling entailment.

  • The naive approach produces marked top-level differences in negations, conjunctions, and disjunctions between positive and negative examples.
  • Positive A formulas average 3.7 satisfying truth assignments, compared with 10.3 for negative A formulas.
  • The mean number of new variables is 0.80 for positive examples and 1.39 for negative examples, with χ2 = 3308.1 and 8 degrees of freedom.
  • These distributional gaps allow heuristics based on formula length, new variables, or topmost connectives to become unreasonably effective.

A.2.2 OUR PREFERRED APPROACH TO DATASET GENERATION

The preferred generator pairs formulas into 4-tuples so each formula appears in both a positive and a negative entailment. This construction equalizes most structural statistics across classes, while leaving a measurable new-variable difference.

  • The preferred approach uses 4-tuples satisfying A1 ⊨ B1, A2 ⊨ B2, A1 ⊭ B2, and A2 ⊭ B1.
  • Each formula appears once in a positive and once in a negative entailment, minimizing crude structural differences between classes.
  • By construction, positive and negative classes have identical mean lengths, operator counts at each syntax-tree level, and numbers of satisfying truth assignments.
  • The remaining crude difference is new-variable count: 1.25 for positive examples versus 1.60 for negative examples, with χ2 = 922.1 and 8 degrees of freedom.
  • The method rules out impossible A1 formulas and tautological B1 formulas because the cross-pair negative entailments must also exist.
Loading 1802.08535v1…