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. This paper seeks to answer two questions: "Can neural networks understand logical formulae well enough to detect entailment?", and, more generally, "Which architectures are best at inferring, encoding, and relating features in a purely structural sequence-based problem?". In answering these questions, we aim to better understand the inductive biases of popular architectures with regard to structure and abstraction in sequence data. Such understanding would help pave the road to agents and classifiers that reason structurally, in addition to reasoning on the basis of essentially semantic representations. In this paper, we provide a testbed for evaluating some aspects of neural networks' ability to reason structurally and abstractly. We use it to compare a variety of popular network architectures and a new model we introduce, called PossibleWorldNet.Neural network architectures lie at the heart of a variety of applications. They are practically ubiquitous across vision tasks BID19 BID17 BID29 and natural language understanding, from machine translation BID13 BID33 BID2 to textual entailment BID3 BID27 via sentiment analysis BID31 BID14 and reading comprehension BID9 BID25 . They have been used to synthesise programs BID20 BID23 BID5 or internalise algorithms BID6 BID11 BID12 BID26 . They form the basis of reinforcement learning agents capable of playing video games BID22 , difficult perfect information games BID28 BID35 , and navigating complex environments from raw pixels BID21 ). An important question in this context is to find the inductive and generalisation properties of different neural architectures, particularly towards the ability to capture structure present in the input, an ability that might be important for many language and reasoning tasks. However, there is little work on studying these inductive biases in isolation by running these models on tasks that are primarily or purely about sequence structure, which we intend to address. The paper's contribution is three-fold. First, we introduce a new dataset for training and evaluating models. Second, we provide a thorough evaluation of the existing neural models on this dataset. Third, inspired by the semantic (model-theoretic) definition of entailment, we propose a variant of the TreeNet that evaluates the formulas in multiple different "possible worlds", and which significantly outperforms the benchmarks. The structure of this paper is as follows. In Section 2, we introduce the new dataset and describe a generic data generation process for entailment datasets, which offers certain guarantees against the presence of superficial exploitable biases. In Section 3, we describe a series of baseline models used to validate the dataset, benchmarks from which we will derive our analyses of popular model architectures, and also introduce our new neural model, the PossibleWorldNet. In Section 4, we describe the structure of experiments, from which we obtained the results presented and discussed in Section 5. We offer a brief survey of related work in Section 6, before making concluding remarks in Section 7. Experimental results are shown in TAB1 . The test scores of the best performing overall model are indicated in bold. The test scores of the best performing model which does not have privileged access to the syntax or semantics of the logic (i.e. excluding TreeRNN-based models) are italicised. The best benchmark test results are underlined.We observe that the baselines are doing better than random (8.2 points above for the easy test set, for the MLP BoW, and 2.6 above random for the hard test set). This indicates that there are some small number of exploitable regularities at the symbolic level in this dataset, but that they do not provide significant information.The baseline results show that convolution networks and BiDirLSTMs encoders obtain relatively mediocre results compared to other models, as do LSTM and BiDirLSTM Traversal models. LSTM encoders is the best performing model which does not have privileged access to the syntax trees. Their success relative to BiDirLSTMs Encoders could be due to their reduced number of parameters guarding against overfitting, and rendering them easier to optimise, but it is plausible BiDirLSTMs Encoders would perform similarly with a more fine-grained grid search. Both tree-based models take the lead amongst the benchmarks, with the TreeLSTM being the best performing benchmark overall on both test sets. For most models except baselines, the symbol permutation data augmentation yielded 2-3 point increase in accuracy on weaker models (BiDirLSTM encoders and traversals, an convolutional networks) and between 7-15 point increases for the Tree-based models. This indicates that this data augmentation strategy is particularly well fitted for letting structure-aware models capture, at the representational level, the arbitrariness of symbols indicating unbound variables.Overall, these results show clearly that models that exploit structure in problems where it is provided, unambiguous, and a central feature of the task, outperform models which must implicitly model the structure of sequences. LSTM-based encoders provide robust and competitive results, although bidirectionality is not necessarily always the obvious choice due to optimisation and overfitting problems. Perhaps counter-intuitively, given the results of BID27 , traversal models do not outperform encoding models in this pair-of-sequences traversal problem, indicating that they may be better at capturing the sort of long-range dependencies need to recognise textual entailment better than they are at capturing structure in general.We conclude, from these benchmark results, that tree structured networks may be a better choice for domains with unambiguous syntax, such as analysing formal languages or programs. For domains such as natural language understanding, both convolutional and recurrent network architectures have had some success, but our experiments indicate that this may be due to the fact that existing tasks favour models which capture representational or semantic regularities, and do not adequately test for structural or syntactic reasoning. In particular, the poor performance of convolutional nets on this task serves as a useful indicator that while they present the right inductive bias for capturing structure in images, where topological proximity usually indicates a joint semantic contribution (pixels close by are likely to contribute to the same "part" of an image, such as an edge or pattern), this inductive bias does not carry over to sequences particularly well (where dependencies may be significantly more sparse, structured, and distant) § . The results for the transformer benchmark indicate that while this architecture can capture sufficient structure for machine translation, allowing for the appropriate word order in the output, and accounting for disambiguation or relational information where it exists within sentences, it does not capture with sufficient precision the more hierarchical structure which exists in logical expressions.The best performing model overall is the PossibleWorldNet, which achieves significantly higher results than the other models, with 99.3% accuracy on test (easy), and 97.3% accuracy on test (hard). This is as to be expected, as it has the strongest inductive bias. This inductive bias has two components. First, the model has knowledge of the syntactic structure of the expression, since it is a variant of a TreeNet. Second, inspired by the definition of semantic (model-theoretic) entailment in § Related to this point, BID15 show that convolutional networks make for good character-level encoders, to produce word representations, which are in turn better exploited by RNNs. This is consistent with our interpretation of our results, since at the character level, topological distance is-like for images-a good indicator of semantic grouping (characters that are close are usually part of the same word or n-gram). general, the model evaluates the pair of formulas in lots of different situations ("possible worlds") and combines the various results together in a product ¶ .The quality of the PossibleWorldNet depends directly on the number of "possible worlds" it considers (see FIG1 . As we increase the number of possible worlds, the validation error rate goes down steadily. Note that the data-efficiency also increases as we increase the number of worlds. This is because adding worlds to the model does not increase the number of model parameters-it just increases the number of different "possibilities" that are considered. In propositional logic, of course, if we are allowed to generate every single truth-value assignment, then it is trivial to detect entailment by checking each one. In our big test set, there are on average more than 3,000 possible truth-value assignments. In our massive test set, there are on average over 800,000 possible assignments. (See TAB0 ). The PossibleWorldNet considers at most 256 different worlds, which is only 7% of the expected total number of rows needed in the big test set, and only 0.03% of the expected number of rows needed for the massive test set.To understand this result, we sample 32, 64, 128 and 256 truth table rows (variable truth-value assignments) for each pair of formulas in Test (hard), and reject entailment if a single evaluation for the formulas amongst these finds the left hand side to be true while the right hand side is false. This gives us an estimate of the accuracy of sampling a number of truth table rows equal to the number of possible worlds in our model. We estimate that these statistical methods have 75.9%, 86.5%, 93.4% and 97.2% chance of finding a countermodel, respectively. This seems to indicate that PossibleWorldNet is capable of exploiting repeated computation across projections of random noise in order to learn, solely based on the label likelihood objective, something akin to a modelbased solution to entailment by treating the random-noise as variable valuations.6 RELATED WORK BID39 show how a neural architecture can be used to optimise matrix expressions. They generate all expressions up to a certain depth , group them into equivalence classes, and train a recursive neural network classifier to detect whether two expressions are in the same equivalence class. They use a recursive neural network BID30 to guide the search for an optimised equivalent expression. There are two major differences between this work and ours. First, the classifier is predicting whether two matrix expressions (e.g. A and (A T ) T ) compute the same values; this is an equivalence relation, while entailment is a partial order. Second, their dataset consists of matrix expressions containing at most one variable, while our formulas contain many variables. BID1 use a recursive neural network to learn whether two expressions are equivalent. They tested on two datasets: propositional logic and polynomials. There are two main differences between their approach and ours. First, we consider entailment while they consider equivalence; equivalence is a symmetric relation, while entailment is not symmetric. Second, we consider entailment as a relational classification problem: given a pair of expressions A and B, predict whether A entails B. In their paper, by contrast, they generate a set of k equivalence-classes of ¶ See Formula 2 above. This general notion of entailment as truth-in-all-worlds is not dependent on any particular formal logic, and applies to entailment in both formal logics and natural languages.formulas with the same truth-conditions, and ask the network to predict which of these k classes a single formula falls into. Their task is more specific: their network is only able to classify a formula from a new equivalence class that has not been seen during training if it has additional auxiliary information about that class (e.g. exemplar members of the class).Recognizing textual entailment (RTE) between natural language sentences is a central task in natural language processing. (See Dagan et al. (2006) ; for a recent dataset, see BID3 ). Some approaches (e.g., BID37 and BID27 ) use LSTMs with attention, while others (e.g. , BID38 ) use a convolutional neural network with attention. Of course, recognizing entailment between natural language sentences is a very different task from recognizing entailment between logical formulas. Evaluating an entailment between natural language sentences requires understanding the meaning of the non-logical terms in the sentence. For example, the inference from "An ice skating rink placed outdoors is full of people" to "A lot of people are in an ice skating park" requires knowing the non-logical semantic information that an outdoors ice skating rink is also an ice skating park.Current neural models do not always understand the structure of the sentences they are evaluating. In BID3 , all the neural models they considered wrongly claimed that "A man wearing padded arm protection is being bitten by a German shepherd dog" entails "A man bit a dog". We believe that isolating the purely structural sub-problem will be useful because only networks that can reliably predict entailment in a purely formal setting, such as propositional (or first-order) logic, will be capable of getting these sorts of examples consistently correct. In this paper, we have introduced a new process for generating datasets for the purpose of recognising logical entailment. This was used to compare benchmarks and a new model on a task which is primarily about understanding and exploiting structure. We have established two clear results on the basis of this task. First, and perhaps most intuitively, architectures which make explicit use of structure will perform significantly better than those which must implicitly capture it. Second, the best model is the one that has a strong architectural bias towards capturing the possible world semantics of entailment. In addition to these two points, experimental results also shed some light on the relative abilities of implicit structure models-namely LSTM and Convolution networkbased architectures-to capture structure, showing that convolutional networks may not present the right inductive bias to capture and exploit the heterogeneous and deeply structured syntax in certain sequence-based problems, both for formal and natural languages.This conclusion is to be expected: the most successful models are those with the most prior knowledge about the generic structure of the task at hand. But our dataset throws new light on this unsurprising thought, by providing a new data-point on which to evaluate neural models' ability to understand structural sequence problems. Logical entailment, unlike textual entailment, depends only on the meaning of the logical operators, and of the place particular arbitrarily-named variables hold within a structure. Here, we have a task in which a network's understanding of structure can be disentangled from its understanding of the meaning of words.Xiang Zhang, Junbo Zhao, and Yann LeCun. Character-level convolutional networks for text classification. In Advances in neural information processing systems, pp. 649-657, 2015.Xiaodan Zhu, Parinaz Sobihani, and Hongyu Guo. Long short-term memory over recursive structures. In International Conference on Machine Learning, pp. 1604 Learning, pp. -1612 Learning, pp. , 2015 A THE DATASET A.1 DATASET REQUIREMENTS Our dataset D is composed of triples of the form (A, B, A B) , where A B is 1 if A entails B, and 0 otherwise. For example: (p ∧ q, q, 1) (q ∨ r, r, 0)We wanted to ensure that simple baseline models are unable to exploit simple statistical regularities to perform well in this task. We define a series of baseline models which, due to their structure or the information they have access to, should not be able to solve the entailment recognition problem described in this paper. We distinguish baselines for which we believe there is little chance of them detecting entailment, from those for which there categorically cannot be true modelling of entailment. The baselines which categorically cannot detect entailment are encoding models which only observe one side of the sequent: DISPLAYFORM0 where f is a linear bag of words encoder, an MLP bag of words encoder, or a TreeNet.Because the dataset contains a roughly balanced number of positive and negative examples, it follows that we should expect any model which only sees part of the sequent to perform in line with a random classifier. If they outperform a random baseline on test, there is a structural or symbolic regularity on one side (or both) which is sufficient to identify some subset of positive or negative examples. We use these baselines to verify the soundness of the generation process.Let D + and D − be the positive and negative entailments: DISPLAYFORM1 We impose various requirements on the dataset, to rule out superficial syntactic differences between D + and D − that can be easily exploited by the simple baselines described above. We require that our classes are balanced: and , we are guaranteed to produce balanced classes. Unfortunately, this straightforward approach generates datasets that violate most of our requirements above. See TAB3 for the details. DISPLAYFORM2 In particular, the mean number of negations, conjunctions, and disjunctions at the top of the syntax tree (num at(·, 0, op)) is markedly different. A + has significantly more conjunctions at the top of the syntax tree than A − , while B + has significantly fewer than B − . Conversely, A + has significantly fewer disjunctions at the top of the syntax tree than A − , while B + has significantly more than DISPLAYFORM3 The mean number of satisfying truth-value assignments (sat(·)) is also markedly different: A + is true in on average 3.7 truth-value assignments (i.e. it is a very specific formula which is only true under very particular circumstances), while A − is true in 10.3 truth-value assignments (i.e. it is true in a wider range of circumstances). We can use these statistics to develop simple heuristic baselines that will be unreasonably effective on the dataset described above: we can estimate whether A B by comparing the lengths of A and B, or by looking at the number of variables in B that do not appear in A, or by looking at the topmost connective in A and B. In order to satisfy our requirements above, we took a different approach to dataset generation. In order to ensure that there are no crude statistical measurements that can detect differences between D + and D − , we change the generation procedure so that every formula appears in both D + and D − . We sample 4-tuples of formulas FIG1 , B 2 ) such that: DISPLAYFORM4 Here, each of the four formulas appears in one positive entailment and one negative entailment * * .Using this alternative approach, we are able to satisfy the requirements above. By construction , the mean length, number of operators at a certain level in the syntax tree, and the number of satisfying truth-value assignments is exactly the same for D + and D − . See Table 4 . DISPLAYFORM5 (r → c) → ((r → v) ∨ p) * * One consequence of this method is that it rules out A1 from being impossible (if it was impossible, we would not have A1 B2) and B1 from being a tautology (if it was a tautology, we would not have A2 B1).
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. The paper proposes a new model to use deep models for detecting logical entailment as a product of continuous functions over possible worlds. Proposes a new model designed for machine learning with predicting logical entailment.