TOP-DOWN NEURAL MODEL FOR FORMULAE
We present a simple neural model that given a formula and a property tries to answer the question whether the formula has the given property, for example whether a propositional formula is always true. The structure of the formula is captured by a feedforward neural network recursively built for the given formula in a topdown manner. The results of this network are then processed by two recurrent neural networks. One of the interesting aspects of our model is how propositional atoms are treated. For example, the model is insensitive to their names, it only matters whether they are the same or distinct.
Cons
1.	There is no study of the representations developed by the model, which is unfortunate because this is a conference on learning representations and because there is little light shed on how the network achieves its rather high level of performance.
2.	It seems less generally useful to have such a special-purpose network for computing global properties like tautologicality than to have a network that produces actual vector encodings of propositions, as typical of the bottom-up tree-structured models.
Pros
3.	The paper is quite clear.
4.	The problem is important.
5.	The paper pursues the familiar path of a tree-structured network isomorphic to the parse tree of a propositional-calculus formula, but with the original twist of passing information top-down rather than bottom-up.
6.	The results are impressively strong. In particular, it improves by 10% absolute over the special-purpose and highly performant PossibleWorldNet on the most difficult category of problems, the ‘massive’ category, achieving 83.6% accuracy.
Pro/Con mix
7.	Although the paper did not provide much insight into what was going on in the network to allow it to perform well (point 1 in ‘Cons’), I was able to convince myself I could understand a way the architecture *could* succeed (whether this possible approach matches the actual processing in the model I have no way of assessing). In brief, the vector that is passed down the network can be thought of as a list of truth values across multiple possible worlds of the tree node at which the vector resides. To search for a counterexample to tautologicalhood, the original input vector to the root node could be the zero (false) vector. If the kth value in the vector at a parent node labeled ‘or’ is 0 (the disjunction is false in world k) then in the two children the kth value must also be 0. If the kth value of the vector at an XOR node is 0, the kth value of the two children must both be 0 or both be 1; actually these values need not reside in position k so the children could both have value 0 at some position i and both have value 1 at another position j. Then in the RNN-Var component of the network, which checks for consistency across multiple tokens of the same proposition variable, each position k in all vectors for the same variable can be checked for equality, producing a value 1 in the output vector if all have value 1, producing 0 if all have value 0, and producing value -1 if the values do not all agree. Then RNN-All checks across all vectors for proposition variable types to see if there’s a position k in which no value -1 occurs; if so, the values of the variable vectors at position k give the truth values for all variables such that the overall proposition has the desired value 0: a counterexample exists. If no such position k exists, the proposition is a tautology. This seems roughly right, at least.