Learning Symbolic Rules for Reasoning in Quasi-Natural Language
Authors: Kaiyu Yang
Jia Deng
Venue: Accepted by TMLR ()

Abstract: Symbolic reasoning, rule-based symbol manipulation, is a hallmark of human intelligence. However, rule-based systems have had limited success competing with learning-based systems outside formalized domains such as automated theorem proving. We hypothesize that this is due to the manual construction of rules in past attempts. In this work, we take initial steps towards rule-based systems that can reason with natural language but without manually constructing rules. We propose MetaQNL, a "Quasi-Natural Language" that can express both formal logic and natural language sentences, and MetaInduce, a learning algorithm that induces MetaQNL rules from training data consisting of questions and answers, with or without intermediate reasoning steps. In addition, we introduce soft matching—a flexible mechanism for applying rules without rigid matching, overcoming a typical source of brittleness in symbolic reasoning. Our approach achieves state-of-the-art accuracies on multiple reasoning benchmarks; it learns compact models with much less data and produces not only answers but also checkable proofs. Further, experiments on two simple real-world datasets demonstrate the possibility for our method to handle noise and ambiguity.

Published in Transactions on Machine Learning Research (05/2023)
Learning Symbolic Rules for Reasoning in Quasi-Natural Language
Kaiyu Yang"
haiynyy@ca.piinnttnn.cm
Deportment of Computer Science Princeton University
Jia Dong
Shadeng@@cs.prinneetrr edu
Department Computer Science
Princeton University
Reviewed on OpenReview: openreveee... net/ fortm id= guRuuHUZUgz
Abstract
Symbolic reasoning, rule-based symbol manipulation, hallmark of human intelligence. However, rule-based systems have had limited success competing with learning-based sys- tems outside formalized domains such as automated theorem proving. We hypothosize that this is due to the manual construction of rules in past altempts. In this work, take initial steps towards rule-based systems that can reason with natural language but without manually constructing rules. We propose MetaQNL, "Quasi-Natural Language" that can express both formal logic and natural language sentences, and Metalnduce, learning algo- rithm that induces MetaQNT. rules from training data consisting of questions and answers, with or without intermediate reasoning steps. In addition, we introduce soft matching a flexible mechanism for applying rules without rigid matching, overcoming a typical source of brittleness in symbolic reasoning. Our approach achieves seate-of-the-ane accuracies on multiple reasoning benchmarks; it learns compact models with much less data and produces not only answers but also checkable proofs. Further, experiments two simple real-world datasets demonstrate the possibility for our method to handle noise and ambiguity
1 Introduction
Symbolic reasoning-rulce rrru-uuluaass based symbol manipulation- is core component of human intelligence (Mercier & Sperber 2017). It has also been a core part of computer science research, and has achieved significant suc- cess in domains such as software verification (Darvas et al. 2005) and theorem proving (Kovács & Voronkov 2013). However, such success has been restricted to domains amenable to rigid, precise formalization. It remains challenge how translate such success into "informal" domains such as reasoning with common- sense knowledge and natural language input. Prior attempts to build rule-based systems, which rely on manually constructed rules, have achieved limited success and tended to produce brittle systems.
Deep learning provides an attractive alternative that can casily sidestep the question of representation. Deep networks can be trained to perform a reasoning task by directly predicting the answer without explicit symbol manipulation (Clark et al., 2020). However, they can require a large amount of training data and can suffer from poor genoralization. More importantly, unlike symbolic systems, deep network is a black box that is hard to interpret and verify. Such lack of interpretability is undesirable in certain applications, especially those critical to safety and security.
In this work, we ask how to build a rule-based system that reasons symbolically but can work with natural language and handle domains difficult to formalize. Such system would perform reasoning by explicit
* Research conducted while Kaiyu Yang was Princeton University. TTe code available bttps://githhb www/prriaceonn-ll/teeeeee vi/etatt...

---

Published in Transactions on Machine Learning Research (05/2023)
symbol manipulation based on rules, therefore is more interpretable and verifiable, but at the same time flexible enough for natural language.
At a glance, this may appear a large departure from the conventional wisdom that learning systems, particu- larly deep networks, are far superior to based systems, as history has demonstrated repeatedly. However, we hypothesize that this conventional wisdom is incorrect because it assumes false dichotomy between using learning and using rules; it is difficult to construct rules mamually. Further, we hypothesize learning rules from data is key to building effective sale-based systems, but it may require different kind of learning than gradient descent.
systems underperformed not because they were rule-based, but because
something strong, then it likes cats
If something is [X], then it [V] [A] [X]
The elephant is
The elephant likes cats
[A] is
[A] is [Y]
[A] [
The elephant is tall
XX, [V] things are [2]
The elephant is strong
[A] is [Z]
Big, tall things are strong
Figure 1: Example proof in MetaQNL with 4 assumptions, 1 goal, and 2 rule applications. Each rule has multiple premiscs and one conclusion. They can have variables ([A], [X], [Y], etc.) that bind to concrete sentences during reasoning. The resulting proof is interpretable to humans and checkable by machines. When applying MetaQNL to a specific task, assumptions and the goal are usually given, and the system has to (1) learn a set of rules from data, and (2) apply the rules to find proofs. The name "MetaQNI." " is inspired by Metamath (Megill & Wheeler 2019) a formal language for expressing mathematical theorems/proot in which substitution is the only rule of inference.
Our goal is thus to develop a method that automatically learns symbolic rules from data to enable ruses-based reasoning with natural language. This poses two main questions. First, what is the system of rules the basic structures defining what symbols and manipulations are allowed such that it is compatible with not only logic but also natural language? Second, what is the learning algorithm that induces rules from data?
In this work, we take initial steps towards answering both questions. We propose MetaQNL, symbolic system we call "Quasi-Natural Language", which is compatible with not only rigorous logical inference but also natural language (Fig. D. We prove theoretical results showing that MetaQNT. is Turing complete. In addition, we propose Metalnduce, a learning algorithm that induces MetaQNL rules from training data consisting of questions and answers, with or without intermediate reasoning steps. It encodes the rule learning problem as a maximum satisfiability (MAX-SAT) problem, which can be solved efficiently by existing solvers.
Reasoning in natural language can be fuzzy and ambiguous. We extend MetaQNL to support such reasoning through soft matching Berchinn-relaxiing the rigid matching conditions when applying rules. Soft matching is a potential avenue for applying MetaQNT, to real-world, free-form natural language. And it enables integration with stato-of-the-ar large pretrained language models (Raffel et al. 2020
Overview of Results. We benchmark our method on 3 tasks: learning compositional instructions, logical reasoning, and morphological analysis. For compositional instructions, our method not only achieves 100% accuracy on MiniSCAN (Lake et al.] 2019) and SCAN (Lake & Baroni 2018), but also recovers the ground truth rules. For logical reasoning, it achieves state-of-the-art performance on RuleTaker (Clark et al., 2020). including the noisy data paraphrased by crowd workers. For morphological analysis, it learns morphologccal rules from real-world linguistic data and is competitive with neural seq2seq models in some languages. Compared to existing methods, our approach Iearns compact models with much less data, and produces not only answers but also checkable proofs. On RuleTaker we learn a model that has only 2869 symbols but is competitive with a prior approach that uses a neural network with 11 billion paraneters (Tafjord et al,, 2021). These results demonstrate the promise of MetaQNT./MctaInnde approach. Finally, we discuss the limitations of our current method, as well as potential improvements in the future to make it general and scalable enough for more realistic, free-form natural language.
as a radically different lcarning
2

---

Published in Transactions on Machine Learning Research (05/2023)
2
Related Work
Symbolic Reasoning. Symbolic reasoning has been studied extensively in classical Al (Robinson & Voronkov 2001 Yang & Deng 2019) and cognitive science (Goodman et al., 2008 Piantadosi al. 2016).
An open problem is to handle domains without natural formalization, e.g., images texts. One common approach is to manually construct a formal system (e.g., first-order logic with manually defined functions and predicates) and then perform semantic parsing to convert images/Lexts into formalized statements (Mao et al. 2018 Dai et al.; 2019 Saparov & Mitchell 2022]. In contrast, our approach does not require a se- mantic parser, because MetaQNL rules consist of premises/conee cconclusioss that can take the form of natural language sentences.
is another class of symbolic systems defined using the syntax of natural language, bypassing semantic parsing. It is highly specialized, committing to predefined rules for monotonicity reasoning (Icard III & Moss 2014). In contrast, MetaQNL has no such restrictions because it is not a specific logic but a meta-language with minimal structures such that it can instantiate various types of reasoning.
Natural Logic (McAllester & Givan 1993
MacCartney & Manning, 2007]
None of prior works discussed so far learn rules from data; instead, they use predefined formal systems that are already specialized and already encode substantial amount of prior knowledge. In contrast, MetaQNL is almost "knowledge-free free" in the sense that it imposes the weakest possible structure the permitted rules and lets the specific rules emerge from data (hrough learning.
Reasoning with Neural Networks. Neural networks can perform "soft" reasoning in the space of con- tinuous vectors without manipulating discrete symbols explicitly (Sanyal et al.) 2022 Dalvi et al.] 2022: Sprague et al.
2022 Creswell et al. 2023). Clark et al. (2020) finetune Transformer (Vaswani et al.
2017 to classify whether the goal is provable from the assumptions (both are sentences in natural language)
Tafjord et al.
22021] and Yang el al. (2022) go one step further to generate proofs. And Bostrom et al.
2021h generate conclusions from premises.
Boyond Transformers, rescarchers have tried to incorporate inductive biases inspired by symbolic reason- ing into neural networks, leading to newro-symbolic architeclures. One line of work is Neural Theorem Provers (Rocktäschel & Riedel 2017 Weber et al., 2019), which uses backward chaining, a classical symbolic reasoning algorithm, to construct the network architecture dynamically. Another line of work embeds sym- bolic structures into continuous vectors while preserving logical operations as continuous operations between vectors /Grefenstette] 2013 Cohen et al. 2018 Lee et al. 2016 Schlag et al. 2019).
Unlike these works, we learn symbolic rules instead of neural network weights. Further, during inference, we generate symbolic proofs whose correctness is guaranteed and can be mechanically checked (with respect the rules). Tafjord et al. (2021) and Yang et al. (0022) also generate proofs, but their proofs are natural lan- guage texts whose correctness is neither guaranteed nor mechanically checkable they train neural networks to generate proofs directly but do not expose formal system of rules against which a proof can be checked.
Learning Rules from Data. Inductive logic programming (ILP) learns rules in logic programs such Datalog (Muggleton| 1991). Extending ILP to natural language is non-trivial-dur to the infeasible need as well as perfect semantic parser. Unlike ILP, rules in
for a predefined ontology of bojjects/predicatte MetaQNL can express not only logic programs but also natural language sentences. And our experiments show that MetaQNL can solve tasks where ILP is not casily applicable.
That said, our method for learning rules draws inspiration from IIP approaches that encode proofs as SAT problems (Raghothaman al. 2019). However, we deal with a richer and more complex space of rules. Our rules consist of sentences with variables, and they form rich hierarchy from abstract rules to concrete ones, making the search space for rule learning much larger. In contrast, rules in ILP are more constrained. They are typically Horn clauses in first-order logic. And they impose strong syntactic constraints, c.g. using templates (Raghothanan et al.) (2019), or by restricting to binary predicales (Evans & Grefenstelle 2018). These constraints are critical to good performance but are domain-dependern and difficult to get right (Cropper & Dumančid 2022). Over-constraining the rule space makes the system less expressive, less generally applicable, and more brittle in the presence of noise. Another difference that we minimize the number of rules in order to generalize, which is unnecessary for IIP due to stronger syntactic constraints.
3

---

Published in Transactions on Machine Learning Research (05/2023)
Beyond ILP, rule learning has also been explored in other contexts. RNNLogic (Qu et al. 2021 uses RNNs to generate rules for knowledge base completion. They impose strong syntactic constraints that rules must be expressed as sequence of predicates, making them less suitable for more general reasoning. Nye et al. (2020) learn rules for a string rewriting system. MotaQNL is more general because it can be applied to not only string rewriting but also other forms of reasoning (Sec. Gh. Similar to us, Unification Networks (Cingillioglu & Russo, 2020) use concrete examples to learn abstract rules with variables. However, their system of rules is significantly less general than ours: their variables can only bind to a single word, whereas our variables bind to arbitrary sentence fragments. In addition, their system does not support multi-step reasoning. All reasoning is done in single step: producing a conclusion in the form of an answer ("yes/no", number, etc.) given premises consisting of a question and a set of supporting facts.
3 MetaQNL: A Symbolic System in Quasi-Naturas Language
In this section, we formally define MetaQNL and present theoretical results showing that MetaQNL is Turing complete. We call MetaQNL a quasi-natural language because it has a formal syntax but is compatible with natural language. Like natural language, a senlence in MetaQNL is simply a sequence of tokens. There are 3 different types of tokens wwrds, variables, and special symbols. Taking the sentence "SFALSE$ The elephant likes [X]" " as example, "The", "elephant" and "likes" are words. They are treated as pure symbols without any semantic meanings. " *[x] "K]"i is variable-a a placeholder that binds to concrete sentences in reasoning. "$FALSE$" is a special symbol. They are useful for encoding the structures of specific tasks, which will become more clear in Sec. G In this paper, we delimit special symbols with S. Sentences without variable are called concrete sentences, c.g., "SFALSE$ The elephant likes cats".
Definition 3.1 (Sentence). Let Ew, Ep, Eg be vocabularies of words, variables, and special symbols; they are disjoint and countable. Let Σ = Ew UE, UE,; then any t E Σ is a token. A sentence (41, 12,,.., ) E Σ+ is a non-emply sequence of tokens. A concrete sentence is a sentence without any variable, i.e., Vi, 4 & Ep.
MetaQNL expresses permitted reasoning steps through rules. A rule has multiple sentences as its premises ("The elephant [X]", "If something [x] then it [Y]") and one sentence as the conclusion ("The elephant [Y]"). Intuitively, the conclusion should follow from the premises regardless of what values the variables take. Concrele rules are rules without variables.
Definition 3.2 (Rule). A rule takes the form of P2i ..:i...PPp :n + c, with n premises P1, ......, Pr E Σt and conclusion c E Σ+. It is a concrete rule if all premisos and the conclusion are concrete sentences.
In reasoning, rules are made concrete by substituting variables with concrete sentences. Given the rule ri- "The elephant [X] If something [x] then it [Y] + The elephant [Y]", we can instantiate it with the substitution { [x] + is strong, [Y] + likes cats), deriving the concrete rule r2 = "The elephant is strong; If something is strong then it likes cats + The elephant likes cats". Here we say is more general than r2, or equivalently, 22 is an instance of r1- Applying substitutions makes a sentence/rule more specific, introducing a partial order among sentences //ules (proofs in Appendix
Definition 3.3 (Substitution). Let Σt, (E.. UΣ,)+ be the set of sentences with only words and variables (without special symbols). A substitution o is a function from E, to Σt_ 2 Substitutions can be extended to be functions on tokens, sentences, and rules. Given a token i E Σ, applying the substitution a produces a sentence ot, which equals to (t) is a variable. Otherwise, at is just & itself. Given a sentence (t.,tt....,tt)) tt)) applying the substitution produces as = (at,, ot,...,.,... + c, applying a produces another rule or opi: op:: ..: opn + ac.
Given a rule r
Definition 3.4 (Partial order among sentences and rules). Let 81 and 82 be two sentences, 82 is an instance of 81 (denoted by 82 S 81) if and only if there exists a substitution a such that 82 = σ81. In this case, we also say 81 is more general than 82. Similarly, let rı and T2 be two rules, r2 is an instance of ri (denoted by r2 S r1) if and only if 3a, r2 = oTi.
2A substitution is defined the of all variables, but practice it only involves few. We can think of being the Identity function for other variables. This convention makes easier to composite substitutions as function composition. We are abusing notations treat a token and a single-token sentence interchangeably.
4

---

Published in Transactions on Machine Learning Research (05/2023)
In reasoning (Fig. 1 the prover is given set of rules M, multiple concrete sentences A assumptions, and one sentence as the goal. It. iteratively instantiates concrete rules from M and applies them to generate a proof of g. Similar to Prolog, I may have variables ("The elephant [X]",, and the prover succeeds if it proves any instance of g (c.g., "The elephant sleeps").
Definition 3.5 (Proof), A proof P = E) is a directed acyclic graph whose vertices V are concrete sentences or concrete rules. For each concrete rule r = P2i Pn I cEV, it must satisfy two conditions: (1) r connects to its conclusion c E V via an edge (r.c) E E; (2) For each premise ps, we have pt E V and (por) E. Besides these edges, there is other edge in E. In addition, the proof P can have multiple sentences without inbound edges (assumptions) but only one sentence without outbound edges (goal).
Definition 3.6 (Theorem proving). Given set of rules M (r., concrete sentences A {a,, .2...... an3 J as assumptions, and a sentence g as the goal, the theorem prover trics to find proof P such that: (1) P's assumptions are A. (2) P's goal is an instance of g. (3) Rules in P are instances of rules in M.
Now we have defined MctaQNI. as a symbolic system. To characterize its theoretical expressiveness, we note that MetaQNL is Turing complete (Theorem 3.7 is proved in Appendiix B). The implication is encouraging In principle, MetaQNT. can solve any task to the extent that the task is solvable by computer programs. Though in practice challenges may arise from how to express the task in an appropriate form and how to learn suitable set of rules.
Theorem 3.7 (Turing completeness of MetaQNL.). For any recursively enumerable language L,, it is possible to construct set of MetaQNL rules for recognizing L.
4 Metalnduce: Learning Rules from Data
4.1 Problem Setup and Loss Function
Learning rules is a machine learning problem where the model consists of not contimuous weights but symbolic rules. The problem sctup is familiar: We want to use the training set Dirain to find a model that performs well not only on Derain itself but also on the test set Drest- For MetaQNL specifically, the training set Dirain = (Ditain: Presin) consists of a set of provable examples Dit and set of unprovable examples D Duriin They both contain training examples in the form of (Ar, 9:), where A, is a set of assumptions and gi is the goal. Intuitively, provable examples are positive examples demonstrating sound logical inference, whereas unprovable examples are negative examples demonstrating unsound inference. More formally, a model M is consistent with a provable example (Ar, 9:) E Dit if g, is provable from A; using rules in M. Similarly, M is consistent with an unprovable example (Ai,g:) E Durai if gi cannot be proved from A..
Given only Dersin we need to find a model that is consistent with as many examples in Dreat as possible, However, it is not sufficient to optimize the consistency with training data, because there is a trivial model that performs perfectly in training but fails in testing one rule per example. That is, any example (Ai gi) E Dit with A, = ...,,,......0 . } is provable using the rule 01; ; a J g. To prevent trivial solutions, we need to penalize the model complexity. Here we measure it as the number of rules and minimize a loss function that ovaluates both model complexity and consistency with training data:
((M) |M|- - X+ AMM D attm X N D Derai)).
(1)
[M] is the number of rules; W(M,Dtt and ((M, Drmin)) are the number of provable/ provable/umprovable examples consistent with M. A+ and X= are hyperparameters controlling the trade-off between the three terms.
The optimization is challenging. Even a single evaluation of L(M) is expensive: (M,, Dita and ((M, D,,in) require running the prover on all training examples. Further, it is much harder to find the op- timal M due the combinatorial and non-differentiable scarch space. We introduce MctaInduce, a general method for learning rules by encoding Eqn. as a maximum satisfiability (MAX-SAT) problem, which can be solved efficiently by existing solvers.
5

---

Published in Transactions on Machine Learning Research (05/2023)
Algorithm 1: MetaInduce
Input : Training data Durin = ((A4)))) A, the assumptions; 9i is the goal.
Output: Model M consisting of a set of rules
M M+Ø
for j 1 to nwm_epochs do
for to do candidates +- propose__peeeeee proposerrules
4
5
prove(A; Ii, condidales U M)
rules f centrrcc_ruless
M + prune_ aorumerrulesti rules (rules)
rrule(
4.2 Metalnduce Algorithm
Overview. MetaInduce is outlined in Algorithm Similar to SGD for training neural networks, MetaIn- duce goes through the training data for several epochs; during an epoch, it processes example per iteration. Given an example (Ai.9:) (either provable or unprovable), it first relies on rule proposer for generating candidate rules that are concrete and potentially useful for proving from A,, Then it runs an existing prover to search for proofs, using both the candidate rules and existing rules in the model. At the end of each epoch, Metalnduce abstracts all concrete rules used in the proofs into rules with variables. Then it performs rule pruning pruning-sclecting M as a subset of the rules minimizing the loss (Eqn. 1 Next, we explain each step in more detail.
Rule Proposal. It is desirable to have a learning system that can learn with minimal domain knowledge but learn more efficiently when more knowledge is available. Therefore, we design the rule proposers to domuin-dependenll, which enables incorporating domain knowledge into the system for more elficient, learning. Specific designs of rule proposers used in this paper can be found in Sec. G and Appendix [ E However, domain-dopendent rule proposers do not significantly compromisc different tasks. As argued in Sec. G rule proposers used in this paper only make modest task-specific assumptions not more than the assumptions made by prior works. Also, the rule proposer has substantial room for future research (Sec. 7 One particularly exciting direction is to train deep neural networks for proposing rules, which can reduce the need for manually crafted hcuristics.
method's general applicability to
Furthermore, a good rule proposer alone-if not used as part MetaInduce-is not sufficient for learning rules. First, the rule proposer only generates concrete rules. It is up to Metalnduce to abstract them into rules with variables. Second, the rule proposer only generates rules useful for single training example, whereas MetaInduce learns rules useful for the entire dataset. Third, the rule proposer does not have to be accurate, Metalnduce can reliably learn correct rules even if most candidate rules are wrong (see Sec. 6.1
Theorem Proving. Theorem proving in MetaQNL is straightforward, thanks existing algorithms such forward/bacde barkwrddb chaining (Russell & Norvig 2002). Forward chaining starts with the assumptions and applies rules to derive new sentences until the goal is reached. Conversely, backward chaining starts with the goal and applies rules in the reverse direction until all assumptions are satisfied. There may be multiple proof paths, and our inplementation finds all of them up to a predefined depth limit.
Rule Abstraction. The proofs contain only concrete rules, and we have to generalize them into rules with variables. We use symbolic procedure called anti unificaiiion (Plotkin 1970.. Given two rules rı and r2, it attempts to find the most specific rule r such that S r and r2 S (analogous to the lowest common ancestor of two nodes in a tree; see Fig, (Left) for examples and Appendix C for more details). Our algorithm performs anti-unification by recursively matching the beginning of two sentences.
Let I be the set of all concrete rules the proofs. We itcratively anti-unify rules in and add the result back, until no new rule can be generated. The result is denoted by I', which contains not only concrete rules but also their generalizations.

---

Published in Transactions on Machine Learning Research (05/2023)
[X] and round and [Y]
[X] and [Y] and [2] and [W]
round
round
104
65
green and round and big and heavy
red and light and round and small
round
round
(cr, Aorg) V cr (er, A
Figure 2: Left: Examples of anti-unifying two concrete rules into more abstract rules. Anti-unification may have multiple solutions that are not comparable with each other. Right: Encoding boolean constraint proof with 3 paths from assumptions to the conclusion. Each concrete rule cr; corresponds to a boolcan variable. The proof is a disjunction of all paths; each path is a conjunction of concrete rules.
Rule Pruning. Rule pruming selects M as a subset of I" by encoding all proofs as a MAX-SAT problem, whose solution corresponds to a set of rules that approximately minimizes the loss function Equ. [ We encode each rule r E I' using a boolean variable (also denoted r). r r= 1 means the rule should be included in M. For any concrete rule E I", we have an additional boolcan variable cr. cr means er is necessary for proving the training examples. We impose different lypes of constraints on these boolean variables:
Data consistency: As shown in Fig. 2 (Right), for the ith training example, its proof P. may have many paths from the assumptions to the goal, but the example is provable as long one of them is valid. For provable examples, we encode P; as disjunction of proof paths. Each path is valid if and only if all concrete rules along the path are valid. So we encode a proof path as a conjunction of all er boolean variables it contains. Analogously, for unprovable examples, we simply take the negation the previous boolean formula to encourage the absence of valid proof. Finally, a good model is not necessarily consistent with every training example. So P. encoded a soft constraint with weight A or A=
Model complezity: To minimize the number of rules, we add soft constraint or of weight 1 for each r boolean variable. It encourages r 0.
Rules instantiation: Each concrete rule must be instance of rule r. Let 71, r2...... Pk E L' be the set of all rules in I" such that cr 5 can be instantiated only if at least one of them is in the model .M. Therefore, we add hard constraint er + ri VV2V.... rk.
Given the boolean constraints above, MAX-SAT solver finds an assignment of boolean variables to minimize the combined weights of violated constraints, which equals to Eqn. 1 Therefore, it learns a set of rules minimizing our loss function.
4.3 Computational Complexity and Scalability
Let be the number of training examples, the complexities of rule proposal and theorem proving are ((n) since they are performed independently for each example. Rule abstraction is Q(n²) since we anti-unify all pairs of rules. However, rule pruning is NP-hard in the worst case due to the use of MAX-SAT (Krentel, 1986). Therefore, our system, its current form, would struggle with very large n. In order to scale to millions of examples, future work would have to reduce the complexity to O(n).
For rule abstraction, note that our pairwise anti-unification is only design choice at the implementation level, rather than conceptual necessity. In principle, all we need is a procedure for generating abstract rules from concrete ones. It is possible to develop more efficient algorithms for rule abstraction with lincar or even sublinear complexity. They can also be based on machine learning, e.g., Cingillioglu & Russo 2020
For rule pruning, one way to scale it up is through approximate MAX-SAT solvers, which are faster but not guarantcod to find the global optimum. Similar to deep learning, MetaInduce does not require the global optimum to work well in practice. Another direction is learning in mini- hini-batches. It avoids encoding the entire dataset large MAX-SAT problem, and instead solves multiple small MAX-SAT problems.
7

---

Published in Transactions on Machine Learning Research (05/2023)
In addition to theoretical complexity, we also report Metalnduce's experimental run time in Sec. 6 which compares favorably to existing methods based on deep neural networks. Our run time is noteworthy consid- ering that deep neural networks are trained on software/ hardware stacks highly optimized for them (GPUs, cuDNN, PyTorch, etc.), whereas Metalnduce can run even on a laptop without GPUs. Our method is at an early stage without nearly as much engineering effort for improving the run time efficiency. At this stage, it is difficult to perform a fair and comprehensive comparison of the run time (e.g., using the same hardware).
5 Soft Matching
Similar to classical theorem proving, reasoning in MetaQNL relies on precise and rigid matching between rules and assumptions. For example, the rule "The [A] smiles + Someone smiles" is not applicable to "An elephant smiles" due to the lack of "The". Although precise matching guarantoes the rigor of rea- soning, reasoning in natural language is often fuzzy and ambiguous, without the same degree of rigor as a mathematical proof. Supporting fuzzy reasoning necessary for MetaQNL to cover broader spectrum of reasoning in natural language. It requires with scores indicating the degree of rigor. Another benefit of soft matching is that it allows the system to degrade gracefully- it can produce an "educated guess" if existing rules are insufficient for producing a rigorous answer.
to relax the rigorous proofs in Definition 3.6 to fuzzy proofs
We extend MctaQNL with soft matching-relaxingg the rigid matching conditions when applying rules. Think of applying a rule r to a set of assumptions as instantiating concrete rules: with rigid matching, we instantiate concrete rules such that cr's premises are A and er must be an instance of r. In contrast, soft matching produces both concrete rules er and scores. cr's premises are still but er is not required to be an instance of r. Furthe,, the matching scores can be aggregated to calculate proof scores, allowing to produce fuzzy proofs when rigorous proofs are impossible.
Definition 5.1 (Soft matching). Given rule and concrcte sentences A {ai, 02,... a0 assumptions, soft matching outputs concrete rules with scores: (cr1, $1), (cr2, (272,8)).... (Crk: 8k) such that (1) Vi, [0, 1]. (2) Vi, cry's premises are A.
There are many possible ways to realize soft matching, including using neural networks. In this paper, as initial step, perform soft matching only in testing. During training, MetaInduce still uses rigid matching for learning rules. Once the rules have been learned, we use them for making predictions with soft matching. We study two simple mechanisms for soft matching based on:
Neural pretrained language model: Given r and A, we use pretrained language model to output conerete rules. Specifically, we encode soft matching as a seq2seq task and finetune T5 (Ralfel et al., 2020 model. Note that it requires supervision for finetuning.
Symbolic anti-unificatioon Given and A, r is not applicable, but we can find more general applicable rule r' by anti-unifying A with r's premises. For example, anti-unifying "An elephants smiles" with "The [A] smiles" produces [A] smiles". Note that rigid matching is special case when r itself is applicable. For calculating the matching score, we use heuristics based on the number of perfectly matched words between r and A.
6 Experiments
We instantiate MetaQNL MMNLLLMMetanduuee on three tasks: learning compositional instructions on MiniS- CAN Lake et al., 2019 /SCAN Lake & Baroni 2018), logical reasoning on RuleTaker (Clark et al. 2020 and morphological analysis on SIGMORPHON 2018 (Cotterell et al. 2018). We achieve statc-of-the-art
accuracies on the three synthetic datasets (MiniSCAN, SCAN, and Rule Taker) using only a minor fraction of training data. On MiniSCAN and SCAN, Metalnduce recovers the ground truth rules precisely. Fur- ther, we evaluate our method with soft matching on two non-synthetic datascts: SIGMORPHON 2018 and ParaRules. Results show the promise of our method in handling noise and ambiguity that are ubiquitous in real-world data. Note that our experiments do not show MetaQNI./Metalndue readily outperform neural
8

---

Published in Transactions on Machine Learning Research (05/2023)
networks unconstruined, free-form natural language. Nevertheless, they demonstrate the promise of radically different learning approach.
6.1 Learning Compositional Instructions
Task and Datasct. MiniSCAN and SCAN have similar format of translating source sequence to a larget sequence, e.g., "jump + JUMP", "jump twice + JUMP JUMP". MiniSCAN consists of only 14 training ex- amples, whereas SCAN has 17K. State-of-the-arr methods have reached 100% accuracy on both datasets (Lit
ct al. 2020
Nye et al.
2020
Chen et al. 2020).
Experimental Sctup.
In training, each source/target pair - is treated provable example (A, 9:). with emply assumplions A, = Ø and the goal Di "x $MAPS_ TO$ y", for examples:
walk
SMAPS_TO$
WALK
turn right
$MAPS_TOP TO$
RIGHT
jump after turn left
$MAPS_TOS
LEFT JUMP
turn left twice
$MAPS_TOS
LEFT LEFT
turn around right
$MAPS_TO$
RIGHT RIGHT RIGHT RIGHT
In lesting, we use "x SMAPS_TOW [Y]" as the goal, where [Y] is a placeholder to be filled by the prover. The prover succeeds if it proves goal with any [Y]. There is no unprovable example.
We use a rule proposer independent of specific training examples. First, generates all concrete rules with S premises by combining the sentences in the training set all possible ways. Then filters the rules using prior knowledge about compositional generalization: The meaning of a long sequence depends on its subsequences. For example. "jump $MAPS_ JUMP + jump twice $MAPS_TOP TOS JUMP JUMP" is valid rule, since jump is a subsequence of jump twice. But "look $MAPS_TU TO$ LOOK jump twice $MAPS _O$ JUMP JUMP" is not valid rule. Similar assumptions were also made in the "interpretation grammar" in Nye et al. (2020) and the "analytical expressions" in Liu et al. (2020). Below are examples of concrete rules generated. Note that many of them do not make sense. However, we do not require the rule proposer to be accurate.
walk $MAPS_TOP TOS WALK; run $MAPS_TOV TO$ RUN + walk after run $MAPS_ TO$ RUN WALK
$MAPS TO$ RUN
+ walk after $MAPS_TO TO$ RUN WALK
$MAPS_ TO$ RUN
T jump twice after twice $MAPS_TOS
RUN RUN JUMP JUMP
run twice SMAPS_TOS TO$ RUN RUN jump twice after run twice $MAPS_TOS TO$ RUN RUN JUMP JUMP
We use backward chaining as the prover and Z3 De Moura & Bjorner 2008 the MAX-SAT solver. For SCAN, we train only on the 400 shortest examples and test on four different splits: simple, length, addprim_jump, and addprim turn left.

---

Published in Transactions on Machine Learning Research (05/2023)
Results. On both datasets, MetaInduce achieves 100% testing accuracy and successfully recovers the ground truth rules. Below are example rules learned from SCAN (more in Appendix D
walk $MAPS_TOD TO$ WALK
+ turn right $MAPS_TO __o RIGHT
+ turn left SHAPS_TOS LEFT
turn around left $MAPS_ TO$
LEFT LEFT LEFT LEFT turn around right SMAPS_TOS
RIGHT RIGHT RIGHT RIGHT
[A] $MAPS_TOS [B]
F [A] left $MAPS_ TO$ LEFT [B]
[A] SMAPS_TOS [B]
+ [A] right $MAPS_ TOS RIGHT [B]
[A]
SMAPS_TOS [B]
[A] twice $MAPS_TOS [B]
[B]
[A]
$MAPS_TOE TOS [B]
[A] thrice $MAPS_ _O$ [B]
[B]
[B]
[A] $MAPS_TO$ [B]
[C]
SMAPS_TOS [D]
[c] and [A] $MAPS_TO$ [D] [B]
[A] $MAPS_TOS TO$ [B] [C]
SMAPS_TOS
[D] [A] after [c] SMAPS_ TO$ [D] [B]
Our experiments take minutes to run on a laptop, which compares favorably with methods using deep neural networks (e.g., 1 day on GPUs in Liu et al. (2020)).
In Eqn. 1 smaller X encourages the cost of accuracy. We tune X+ on 1000 validation examples. Results in Table 1 show that the accuracy on SCAN is fairly robust w.r.t. x+.
compact models (i.e., small number of learned rules) potentially
Table 1: Validation accuracies SCAN with different X+
+
0.32
0.64
1.28
2.56
5.12
00
# RRules learned Accuracy 85.9
16
17
20
20
20
90.3
100.0
100.0
100.0
100.0
6.2 Logical Reasoning
Task and Experimental Setup. RuleTaker tests logical reasoning using synthetic sentences. It consists of examples similar to Fig. We use the OWA (open-world assumption) version introduced by TTaford et al.) (2021), where sentence can be proved, disproved, or neither. For example, if "The elephant be tall" is true, then "The elephant be not tall" should be false. To handle such cases, prepend sentences with special symbols $TRUE$ $FALSE$, so that the example can be disproved using the rule "$TRUE$ The elephant be tall + $FALSES The elephant be not tall". For each example to be proved, we add it to the set of provable examples ti and its negation to unprovable examples Dirain Conversely, for each example to be disproved, we add it to Drrain and its negation to D Dit For examples that can be neither proved nor disproved, we add both itself and its negation to D
RuleTaker includes ground truth proofs providing concrete rules such "$TRUE$ The elephant be tall H $FALSES The elephant be not tall" but not any abstraction that allows generalizing beyond the specific examples. Our rule proposer simply generates these ground truth concrete rules, whereas MetaInduce tries to learn abstract rules. And we use simple heuristios for filtering invalid rules generated by anti-unification
[Appendix Fb. Note that prior works on Rule also rely on ground truth proofs (Clark et al. 2020 Saha
et al. 2020 Tafjord et al. 2021
On machines with 0 GPUs, 32GB RAM, and CPUs, we run MetaInduce for epochs on 10K training examples, which takes about 20 hours. We use forward chaining the prover and depth limit of 7. The
10

---

Published in Transactions on Machine Learning Research (05/2023)
hyperparameters X and - are tuned on validation data. Examples of learned rules are in Appendix E Our experiments take 2 days. It is impossible to directly compare our run time with Proo/Writer since their code is not publicly available.
Answer predicting accuracies on RuleTaker (OWA). Rows are depths of test proofs. N/A means the test example can be neither proved nor disproved.
Table 2:
D3
D5
ProofWriter
Ours
Proo[Writer
Ours
N/A
99.9
99.4
99.4
99.6
100.0
100.0
100.0
100.0
99.3
100.0
100.0
100.0
99.7
99.7
99.9
100.0
99.2
98.9
100.0
100.0
99.1
98.9
99.9
99.4
98.8
98.6
100.0
99.1
All
99.6
99.4
99.7
99.7
Table 3: Answer predicting accuracies the OWA version of ParaRules. Rules and lested on ParaRules.
The model is trained on D3
PRover
ProofWriter
Ours
99.7
99.9
100.0
98.6
99.3
99.7
98.2
98.3
99.4
3
96.5
98.2
98.8
88.0
100.0
98.4
99.1
99.7
Results Synthetic Data. The RuleTaker dataset consists of simple synthetic sentences generated by templates. We compare our method with ProofWriter (Tafford et al. 2021 state-of-the-ar method that also uses ground truth proofs. Following their setup, we test on D5 (a subset RuleTaker with proof depths & 5) and train separate models on D5 and D3 (proof depths < 3). Results are in Table 2 MetaInduce achieves stale-of-the-art accuracies and competitive with Proo/Writer. Further, it learns significantly more compact models with much less training data. For example, the model trained on D3 with A = 1.28 using only 14% of the training data has only 79 rules and total of 2869 symbols, but achieves overall test accuracy of 99.4%. In comparison, Proo/Writer has accuracy of 99.6% and is based on T5-11B (Ralee et al. 2020 which has 11 billion parameters.
Note that we only compare with noural approaches, as many cxisting neurosymbolic approaches are not readily applicable to our task setting without significant mamual design. For example, [Rockääschel & Riedel (2017): Evans & Grefenstette (2018); Cohen Cohen et al. (2018); Saparov & Mitchell (2022) require human-defined
predicates. Lee al. (2016); Weber et al. (2019) require semantic parsing.
Handling Noisy Data with Soft Matching. To test our our system using data closer to natural language, we evaluate on ParaRules- part of RuleTaker consisting of 40K examples paraphrased into natural language by crowd workers. We apply the language model-based soft matching mechanism described in Sec. Following ProofWriter, we train on D3 + ParaRtues and test on ParaRules.
First, we run Metalnduce on (synthetic) D3 to learn a set rules just like before. Let T be the set of sentences the learned rules. Then we extract a dataset from ParaRules for training the soft matching network. ParaRules contains pairs of (s,p), where is synthetic sentence ("The elephant like cats") and p is its paraphrased version (e.g., "The elephant is fond of felines"). For each (s, p) and
11

---

Published in Transactions on Machine Learning Research (05/2023)
Table Fl scores of morphological analysis. FP is the average of FUT and PST. represents OTHER.
Model
Spanish
Swahili
Turkish
FP
O
FP
0
FP
0
LSTMs
Atlention
66
88
75
90
69
85
Ours
55
82
81
86
53
71
Ours + Soft matching
66
84
80
85
53
70
(e.g. "[A] [B]"), we check whether 8 can match with t symbolically (yes in this case). If so, we know applying soft matching to p and should produce 8. And the training data consists of all triples of (s,p,
The soft matching network is implemented by finetuning T5 model (Raffel et al. 2020 The input sequence concatenates p and ("the elephant is fond of felines <SEP> [A] [B] "). And the output is ("the elephant like cats"). We finetune the model with learning rate of 10-1 and a batch size of 32 using the
AdamW optimizer (Loshchilov & Hutter 2019). Once trained, we use the soft matching network to perform matching when ovaluating the learned rules on ParaRules. Results in Table show an overall accuracy of 99.7%, outperforming PRover (Saha et al. 2020 and ProofWriter.
6.3 Morphological Analysis
Finally, we evaluate on the morphological analysis task in Akyürck et al. (2021 Morphological analysis is not a reasoning lask. But is frequently used by prior work as a lestbed of com- positional generalization and learning symbolic rules/programs from data, which are two important aspects of our method. Given the surface form of word (c.g., studied), the model predicts its lemma (study) and an unknown number of tags, such as SG (singular) and PST (past tense). The data is constructed from the SIGMORPHON 2018 dataset. It consists of 3 languages with varying morphological complexity-Spanne Spanish, Swahili, and Turkish. For each language, they sample training set of 1K examples and three test sets of 100 examples each (FUT, PST, and OTHER). FUT consists exclusively of words in the future tense; PST consists of words in the past. lense. The training set has only past-tense words and 8 future-tense words. Therefore, FUT and PST test models' few-shot learning capabilities.
Task and Datasct.
Experimental Setup. To apply MetaQNL, we represent both the surface form and the lemma as charac- ters. The surface form serves as the assumption, whereas the lemma and the tags serve as conclusions. For example, for the Spanish surface form zarandeamos with lemma zarandear and tags V;IND;PRS 11;L, we treat r a r d a $TAG$ V, ..., $TAG$ PL. Any other goals are treated as unprovable. The rule proposer simply generates rules that can prove the conclusion in a single step. For this example, it generates the 6 candidate rules below:
the assumptions and construct provable examples with goals $LEMMAS z
d
$LEMMAS zarandear
2 r
d
a
m
0
T $TAG$ V
2 a r a n
d
a 0
T $TAG$ IND
2 a r a
n
d
8
+ STAG$ PRS
2 r
m
+ $TAG$
d
T $TAG$ PL
Following Akyürek et al. (2021). we evaluate the predictions using F1 score and compare with a standard seq2seq neural network: LSTMs (Hochreiter Schmidhuber, 1997) with attention. Note that we're com- paring with the baseline in Akyürek et al. (2021), not their proposed method. Their method is orthogonal to us since it focuses augmenting the training data.
12

---

Published in Transactions on Machine Learning Research (05/2023)
Results w/o Soft Matching. Results are shown in Table 4 Note that the task is not trivial: the neural baseline performs far from perfect, especially on FUT and PST (an F1 score of 66% on Spanish). Our met hod (without soft matching) is competitive with the baseline on Swahili, but there are still gaps on Spanish and Turkish. Further analysis reveals different reasons behind the gaps: Turkish morphology is very complex. But our current way of instantiating MetaQNI. only considers proofs of depth 1, which could be a restriction for learning more expressive rules. Spanish morphology is relatively simple. Our F1 score still has a large room for improvement, because it learns over-specific rules that achieve high precision but low recall.
Below are example rules learned from the Spanish part of the dataset. Unlike the baseline, method learns interpretable morphological rules; e.g., the suffix áramos indicates the past tense
[A] e a m a
$LEMMAS [A] eer
[A] á r a m 0
STAGS PST
n O S [A] m 0
$TAGS SBJV
n [A]
$LEMMAS [A]
[A]
$LEMMAS [A]
Results w/ Soft Matching. To explore soft matching, we keep training the same and apply soft matching only in testing. Given a testing example such as "z a n e o s", we consider not only applicable rules learned by Metalnduce but also additional rules generated through our simple soft matching mechanism based anti-unification (Sec. 5). All rules ranked based on their matching scores, which are calculated using heuristics. Rigid matching always has the highest score, and more perfectly matched characters lead to higher scores. After ranking the rules, we apply them one by one until we gel a predicted lemma.
The bottom row in Table 4 shows the result of soft matching. Even this simple form soft matching can close the gap on Spanish. However, leads to no improvements on Swahili and Turkish. We found that the individual rules learned on Swahili and Turkish are more approximate, ie. more like "rules of thumb" they capture the general pattern but have many exceptions. This is due to the increased morphological complexity. In these two languages, there are fewer simple rules such as "This suffix always indicates the past tense." As a result, relaxing the matching conditions naively would lead to too many spurious rules.
7 Limitations and Open Questions
First, our approach is far from mature. Substantial further development is needed for handling free-form natural language, e.g., in benchmarks of arithmetic or commonsense reasoning (Cobbe et al. 2021 Talmor et al. 2019). Soft matching one possible way to address linguistic variations, c.g., by using pretrained language model to output matching scores between rules and assumptions.
Our experiments are not large-scale but serve as proof of concept for novel approach at an early stage, Metalnduce does not yet scale to millions of training examples (Sec. 1.3), which may be necessary learn enough rules to handle the complexity of natural language. The current bottleneck is rule abstraction, which can be possibly addressed through better methods than anti-unification.
MetaInduce is meta algorithm that permits many variations of its components. This provides many open questions and opportunities for integration with deep learning. For example, the rule proposer or theorem prover can be a deep network instead of a manually crafted heuristic.
Acknowledgments
This work partially supported by the Office of Naval Rescarch under Grant N00014-20-1-2644 The authors also gratefully acknowledge financial support from the Schmidt DataX Fund at Princeton University, made possible through major gift from the Schmidt Futures Foundation.
13

---

Published in Transactions on Machine Learning Research (05/2023)
References
Ekin Akyürek, Afra Feyza Akyürek, and Jacob Andreas. Learning to recombine and resample data for compositional generalization. In International Conference on Learning Representations (ICLR), 2021.
Kaj Bostrom, Xinyu Zhao, Swarat Chaudhuri, and Greg Durrett. Flexible generation of natural language deductions. In Conference on Empirical Methods in Natural Longuage Processing (EMNLP). 2021.
Xinyun Chen, Chen Liang, Adams Wei Yu, Dawn Song, and Denny Zhou. Compositional generalization via neural-symbolic stack machines. In Advances in Neural Information Processing Systems (NeurPPS), 2020.
Nuri Cingillioglu and Alessandra Russo. Learning invariants through soft. unification. In Advances in Newral Information Processing Systems (NeurIPS), 2020.
Peter Clark, Oyvind Tafjord, and Kyle Richardson. Transformers as soft reasoners over language. Tn International Joint Conference on Artificial Intelligence (IJCAI), 2020.
Karl Cobbe, Vincet Kosaraju, Mohammad Bavarian, Jacob Hilton, Reiichio Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprinl or wrXie:2110.41166 2021.
William W Cohen, Fan Yang, and Kathryn Rivard Mazaitis. Tensorlog: Deep learning meets probabilistic databases. Journal of Artificial Intelligence Research, 1:1-15, 2018.
Ryan Cotterell, Christo Kirov, John Sylak-Glassmin Géraldine Walther, Ekaterina Vylomova, Arya D McCarthy, Katharina Kann, Sabrina Mielke, Garrett Nicolai, Miikka Silfverberg, et al. The conll- sigmorphon 2018 shared lask: Universal morphological reinflection. Proceedings of the CoNLL- SIGMORPHON 2018 Shared Task: Universal Morphological Reinfiection, pp. 1 1-27, 2018.
Antonia Creswell, Murray Shanahan, and Trina Higgins. Selection-infernnce: Exploiting large language mod- els for interpretable logical reasoning. In International Conference on Learning Representations (ICLR), 2023.
A Cropper and S Dumančíć. Inductive logic programming: new introduction. Journal of Artificial Intel- ligence Research, 2022.
Wang-Zhor Dai, Qiuling Xu, Yang Yu, and Zhi-Hua Zhou. Bridging machine learning and logical reasoning by abductive learning. Tn Advances Neural Information Processing Systems (NeurIPS), 2019.
Bhavana. Dalvi, Oyvind Tafjord, and Peter Clark. Towards teachable reasoning systems: Using a dynamic memory of user feedback for continual system improvement. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
Ádám Darvas, Reiner Hähnle, and David Sands. A theorem proving approach analysis of secure informa- tion flow. In International Conference Security in Pervasive Computing (SPC), 2005.
Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008
Richard Evans and Edward Grefenstette. Learning explanatory rules from noisy data. Journal of Artificial Intelligence Research, 61:1-64, 2018.
Noah D Goodman, Joshua B Tenenbaum, Jacob Feldman, and Thomas L Griffiths. rational analysis of rule-based concept lcarning. Cognitive Science, 32(1):108-154; 2008.
Edward Grefenstette. Towards formal distributional semanties: Simulating logical calculi with tensors. arXiv preprinl ar Xro:::1004.558 2013.
Sepp Hochreiter and Jürgen Schmidluber. Long short-term memory. Neural computation, 98))17335-178) 1997.
14

---

Published in Transactions on Machine Learning Research (05/2023)
John E Hopcroft, Rajeev Motwani, and Jeffrey D Ullman. Introduction automata theory, languages, and computation. Acm Sigact News, 32(1):60 15,60065---0 2001.
Thomas F Teard III and Lawrence Moss. Recent progress on monotonicity. In Linguistic Issues Language
Technology (LLLT), 2014.
Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In International Conference on Computer Aided Verification (CAV), 2013.
Mark W Krentel. The complexity of optimization problems. In Symposium on Theory of Computing (STOC), 1986.
Temur Kutsia. Unification with sequence variables and flexible arity symbols and its extension with pattern- terms. pp. 190-304, 2002.
Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-unification for unranked terms and hedges. Journal of Automated Reasoning, 52:155-190, 2014.
Brenden Lake and Marco Baroni. Generalization without systematicity: On the compositional skills of sequence-to-seqqeeee recurrent networks. In International Conference on Machine Learning (ICML), 2018.
Brenden M Lake, Tal Linzen, and Marco Baroni. Human few-shot learning of compositional instructions. In Annual Meeting of the Cognitive Science Society (CogSci), 2019.
Moontae Lee, Xiaodong He, Wen-tau Yih, Jianfeng Gao, Li Deng, and Paul Smolensky. Reasoning vector space: An exploratory study of question answering. In International Conference on Learning Representations (ICLR), 2016.
Qian Liu, Shengnan An, Tlan-Guang Lou, Bei Chen, Zeqi Lin, Yan Gao, Bin Zhou, Nanning Zheng, and Dongmei Zhang. Compositional generalization by learning analytical expressions. In Advonces in Neural Information Processing Systems (NeurIPS), 2020.
Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In International Conference Learning Representations (ICLR), 2019.
Bill MacCartney and Christopher D Manning. Natural logic for textual inference. In ACL-PASCAL Workshop on Textual Entailment and Paraphrasing. 2007.
Jiayuan Mao, Chuang Gan, Pushmeet Kohli, Joshua B Tenenbaum, and Jiajun Wu. The neuro-symbolic concept learner: Interpreting scenes, words, and sentences from natural supervision. In International Conference on Learning Representations (ICLR), 2018.
David McAllester and Robert Givan. Taxonomic syntax for first order inference. Journal of the ACM (JACM), 40:246-283, 1993.
Norman D. Megill and David A. Wheeler. Metamath: A computer language for mathematical proofs. 2019.
Hugo Mercier and Dan Sperber. The enigma of reason. Harvard University Press, 2017.
Stephen Muggleton. Inductive logic programming. New Generation Computing, 8:295-318, 1991.
Maxwell I Nye, Armando Solar-Lezama, Joshua B Tenenbaum, and Brenden M Lake. Learning compositional rules via neural program synthesis. In Advances in Neural Information Processing Systems (NeurIPS), 2020.
Steven T. Piantadosi, Joshua B Tenenbaum, and Noah D Goodman. The logical primitives of thought: Empirical foundations for compositional cognitive models. Psychological Review, 123(4):392, 2016.
Gordon Plotkin. A note inductive generalization. Machine Intelligence, 5:153 163, 1970.
15

---

Published in Transactions on Machine Learning Research (05/2023)
Meng Qu, Junkun Chen, Louis-Pascal Xhonneux, Yoshua Bengio, and Jian Tang. Rnnlogic: Learning logic rules for reasoning on knowledge graphs. In International Conference on Learning Representalions (TCI.R) 2021.
Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J Liu. Exploring the limits of transfer learning with a unified text-to-text transformer. Journal of Machine Learning Research (JMLR), 21:1 67, 2020.
Mukund Raghothaman, Jonathan Mendelson, David Zhao, Mayur Naik, and Bernhard Scholz. Provenance- guided synthesis of datalog programs. In Symposium on Principles of Programming Languages (POPL), 2019.
Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. 2001.
Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. Tn Advances in Neural Information Processing Systems (NeurIPS), 2017.
Stuart Russell and Peter Norvig. Artificial intelligence: modern approach. 2002.
Swarnadeep Saha, Sayan Ghosh, Shashank Srivastava, and Mohit Bansal. Prover: Proof generation for interpretable reasoning over rules. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2020.
Soumya Sanyal, Harman Singh, and Xiang Ren. FaiRR: Faithful and robust deductive reasoning over natural language. In Annual Meeting of the Association for Computational Lènguistics (ACL), 2022.
Abulhair Saparov and Tom M Mitchell. A generative symbolic model for more general natural language understanding and reasoning. Trunsaclions of the Associalion for Compulational Linguisties (TACL), 10: 325 342, 2022.
Imanol Schlag, Paul Smolensky, Roland Fernandez, Nebojsa Jojic, Jürgen Schmidhuber, and Jianfeng Gao. Enhancing the transformer with explicit. relational encoding for math problem solving. arXiv preprinl wwXiv:1910.06611 2019.
Zayne Sprague, Kaj Bostrom, Swarat Chaudhuri, and Greg Durrett. Natural language deduction with incomplete information. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. Proofwriter: Generating implications, proofs, and ab- ductive statements over natural language. In Findings of the Association for Computational Linguistios: ACL, 2021.
Alon Talmor, Jonathan Herzig, Nicholas Lourie, and Jonathan Berant. CommonsenseCA:: A question answer- ing challenge targeting commonsense knowledge. In Annual Conference of the North American Chapter of the Association for Compulational Linguisties (NAACL), 2019.
Ashish Vaswani, Noam Shazoer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in Neurol Information Processing Systems (NeurIPS). 2017.
Leon Weber, Pasquale Minervini, Jannes Münchheyer, Ulf Leser, and Tim Rocktäschel. Niprolog: Reasoning with weak unification for question answering in natural language. In Annual Meeting of the Association for Computational Linguistics (ACL), 2019.
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019.
Kaiyu Yang, Jia Deng, and Danqi Chen. Generating natural language proofs with veriffer-guided search. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
Gonzague Yernaux and Wim Vanhoof. Anti-umifiation in constraint logic programming. Theory and Practice of Logic Programming, 19:773 789, 2019.
16

---

Published in Transactions on Machine Learning Research (05/2023)
A Partial Order Among Sentences and Rules
Here prove that the < in Definition 3.4 is indeed a partial order relation. First note that the equality between rules is defined modulo premise reordering and a-conversion. In other words, premises are unordered, and variable renaming does not change a rule.
Definition A.1 (Sentence length). The length of (f2, Et, denoted by length(s), is n.
Lemma A.2 (Substitutions noncontractive). Applying substitutions does not make sentence shorter. More formally, for any sentence s (f1, ,,,...,ta fa) E E+ and substitution a E. + I we have length(as) 2 n. Further, lenglh(as) = n if and only if a maps all lokens in to sentences of length 1, i.e., Vi, length(t:))
Proof. For any substitution o En + Σt and variable u E Ee, a(v) E Σt is a sentence. Therefore, for any token t E Σ, length(ot) 2 (Definition 3.3 For any sentence $ = (4,, f2.12....... tn), length(as) En length(ol,) 2 n.. And the equality holds and only if liggehgth(rt,) =.
Theorem A.3 (Partial order among sentences). If sentence equality is defined modulo a-conversion, then the < in Desenition 3.4 is a partial order among sentences. In other words,
1. V Σ s....
Vs1. E of S 82 and 82 I $1, then 81 = 82 modulo a-conversion.
3. 82 83 if $2 and sa, then $1 S 83.
Proof. We prove the statements separately.
1. Let be the identity substitution mapping any variable to itself, i.c., Ve Ev, From Definition 3.3 also maps any token to itself (Vi E E, = L), and therefore any sentence to itself (Vs E Et ES s). Applying Definition 3.4 we have Vs E 5t,s5
2. Given sentences $1 (t,, .....,.,,.... 52 (ti, ,,, ( such that S1 S 82 and $2 S S1, there exist substitutions a, y such that 81 082 and 82 48i (Definition 3.4h. Applying Lemma A.2 to them separately leads to n and Vi, lengh((pptt) we derive Vi, = of; and t. st,, If & is not a variable, 1 = pt; = 4, i.e., all non-variabie tokens in 81 and 82 are identical. If 4; is a variable, & must also be a variable because otherwise t; = ot, would not be a variable. Therefore, both a and are just renaming variables. And is straightforward to verify that they cannot map different variables to the same. other words, o and ip are a conversion;; 81 = 82 modulo a-conversion.
length(ot)) 1. According to Definition 3.3
3. Given three sentences 81, 82, and 83 such that 81 I and 82 S there cxist substitutions and such that 81 = 082 and 82 = 488. Let a be the function composite of a and yp. P is also a substitution and 81 = μs3z. Therefore, $1 $ 83.
Theorem A.4 (Partial order among rules). The S in Definilion 3.4 is a partial order among rules. In other words,
1. For any rule S.
For any two rules in and r2, if Fı S r2 and r2 S rı, then rı = 12 modulo a a-conversion.
3. For any three rules T1, T2 and r3, ri I 12 and S ra, then T1 T-
Proof. Similar the proof of Theorem
A.3
17

---

Published in Transactions on Machine Learning Research (05/2023)
Definition A.5 (Strictly partial order among sentences/rules). Let $1 and $2 be two sentences, $1 is strictly more general than 82 (denoted by 82 81) if and only if 82 S and 81 & 82 modulo a-conversion. Similarly, if ri and 72 are rules, r2 < T1 if and only if r2 S 71 and rı # r2 modulo a-conversion.
B Turing Completeness of MetaQNL
We prove the Turing completeness of MetaQNL (Theorem 3.7 grammars, which have been known to be equivalent to Turing machines. First, we repeat a few definitions that can be found in common textbooks on formal languages and automata theory (Hopcroft et al. 2001
through its connection with unrestricted
Definition B.1 (Unrestricted grammar). An unrestricted grammar is formal grammar G G= (N, P.S). where N is a finite set of nonterminal symbols, T is a finite set of terminal symbols, and N N = Ø. P is a finite set of production rules of the form a + 33 where a E (N U)+ is an non-empty string, and B E UT)* is an arbitrary string. S E N is a designated start symbol.
Definition B.2 (Direct derivation). For any strings e E (N we say u directly derives to v (denoted as u + v) if and only if there exists a production rule a - B such that u = lar and v = 13r, where L UT) are arbitrary strings.
Definition B.3 (Derivation). The "derives to" relation (=*) is the reflexive transitive closure of the "direct derives to relation (+).
Definition B.4 (Language of unrestricted grammar). Given an unrestricted grammar G = (N,T, P,S), its language LGG) = {w E T S w] consists of all terminal strings derivable from the start symbol S.
Next, we prove that for any unrestricted grammar G, there exists a set of MetaQNT. rules that can recognize its language LGG).
Theorem B.5 (MetaQNL can express unrestricted grammar). For any unrestricted grammar G (N,T,P. P,S), there exists a set of MetaQNL rules that can recognize L(G), i.e., for any w E TT" w E L(G) if and only if S > w is provable in MetaQNT.
Proof. Let G = (,S),P.S) be an arbitrary unrestricted grammar. We construct a system of MetaQNL rules with the word vocabulary En- = NU,, the variable vocabulary Σ, = R). and the special symbol vocabulary Σg = { We can assume they are disjoint without loss of generality. Then for each production rule a + E P, we construct four MetaQNT. rules:
S [L] a [R]
S [
(2)
S a [R]
} S - [RR]
(3)
S = [L]
T S 3 [L]
S a
T S 3.
(5)
And we have a special rule without any assumption:
ト S
(6)
We want to prove that these rules can be used to recognize L(G).
Let w E L(G), i.c., = w. From Definition B.3 we have S > in = U2 = ... 4 = w, where un E (NUT) UT) are intermediate strings for deriving w. We prove that S = w is provable in MetaQNL by induction on k. When k = 1, have S > According to Definition B.2 there must be production rule
S + w E P. It corresponds to a MetaQNI. rule S + S h S = w (Eqn. Together with the special rule | S - S (Eqn. 6), we can prove S > w in MetaQNL.
When k > 1, since uk-1 + w, there must be a production rule a + 3 e P such that ux-1 = lar and w = 13r, where 1,r E UT). Regardless of whether I and are empty. One of the four corresponding MctaQNI. rules can be instantiated be S 3" lar + 3 lßr, which equivalent S x* uk-1 H S = w. Also, the inductive hypothesis tells S = u is provable in MetaQNL. Therefore, S 3 w is also provable.
18

---

Published in Transactions on Machine Learning Research (05/2023)
Conversely, given any (NUT) such that S =" is provable in MetaQNL, we want to prove S = We perform induction on the number of steps k it takes to prove S = in MetaQNI. When k = 1, it must be proved by a single application of the special rule + S *' S (Eqn. 6 Therefore w = S. According to Definition B.3 = w holds.
When > 1, our proof depends on which one of the four types of MetaQNT, rules (Fqn. to Equ. 5 is applied in the last step when proving S +* w. Here we only consider Equ. siice it is the most sophisticated case; other cases are similar. So S = [L]a [R] S = [L] 3 [R] is the last MetaQNL rule applied, and Lr E (NU UT+ are the strings used to instantiate the variables [L] and [R] (w (ßr). By that time, we must have alrcady proved the assumption S +" lar within k - 1 steps. So the inductive hypothosis tells us S =* lor. The last MetaQNL rule corresponds to a production rule a + B. Definition B.2 tells us lar + 1ßr. Therefore, we have S + 10r, and S w.
Theorem 3.7 is a direct corollary of Theorem B.5 since unrestricted grammars can express any recursively enumerable language.
C Unification and Anti-unification of Sentences and Rules
Robinson & Voronkov 2001 are basic symbolic procedures in formal logic that are useful for theorem proving and logic programming (Russell & Norvig 2002; Yernaux & Vanhoof 2019). In MetaQNL, unification is used in backward chaining, and anti-unification is used to abstract concrete rules into rules with variables. We adapt existing problem setups and algorithms from formal logic to Met The algorithms we use for MetaQNL do not have theoretical guarantees as in formal logic, but they work well in practice. The anti-unifiers they compute may not satisfy the conditions of most specific anti- unifiers (Definition C.7). But strict anti-unification is not necessary for rule abstraction to work. In principle, all we need is a procodure for generating abstract rules from concrete ones.
Unification and anti-unification (Plotkin 1970
Unification. Given two sentences (or two rules), unification aims to find substitutions mapping them to the same sentence (or rulc). Such substitutions are called unificrs. We extend unification to MctaQNL by adapting prior work, especially the unification algorithm developed by Kutsia (2002) for a variant of first-order logic with sequence variables and flexible arity symbols.
Definition C.1 (Unifier). A substitution a: : Σ, + Σt, is a unifier of two sentences $1,82 E if and only if ass = 032. Similarly, is a unifier of two rules rı and r2 if and only if Øri = =rr2.
Two sentences may have multiple unifiers. Taking $1 [X] is [Y], 82 The e elphant [2] as an example, their unifiers include a = {[x] + The elephant, [2] - is [Y]] 9 = [[x] + The elephant, [Y] tall, [Z] + is tall}. etc. Both a and & are valid unifiers, but they lead to different sentences when applicd: as = The elephant is [Y], (os = The elephant is tall. We profer a to i because it is more general; it does not introduce any new information not in $1 and $2. In contrast, we cannot infer the "tall" in yp. This the intuition behind the concept of "most general unifiers".
Definition C.2 (Most general unifier). Let the substitution a be a unifier of sentencens $1 and $2, it is a most general unifier if and only if there is no unifier yp of $ and $2 such that σs1 < (p31.
In unification, we want to compute a set of most general unifiers, and we want the set to be minimal and complete. Below we define these concepts for sentences.
Definition C.3 (Complete set of unifiers). Let U be a set of unifiers of sentences 81 and 82, U is complete if and only if for any unifier yp of s1 and $2, there exists a unifier a E U4 such that 60s S GS1.
Definition C.4 (Minimal set of unifiers). Tet 24 be a set of unifiers of sentences 81 and 82, U is minimal if and only if for any a, & E U, (08 I as implics o = 4 (modulo a-conversion).
Definition C.5 (Minimal complete set of unifiers). Let U be a set of unifiers of sentences s and 32, U is a minimal complete set of unificrs if and only if it both minimal and complete.
The definitions for rules are parallel. Given two sentences (or two rules), the unification problem is compute a minimal complete set of unifiers. The result can be empty (e-g. unifying "hello world" and
19

---

Published in Transactions on Machine Learning Research (05/2023)
hello [X]
[X] hello
[X] you [
[X] are [Y]
hello hello
hello hello
hello hello hello hello
How are you ?
? you are how
Figure 3: The minimal complete set unifiers of two sentences can empty, finite, or infinite (e.g., "hello [X] and " "[X] hello"). The minimal complete set of anti-unifiers is non-empty and finite.
"how are you"); finite ("hello [x] and [YY] world"), infinite ("hello [x] th and [X] hello", Fig. Left).
Anti-unification. Given two sentences (or two rules), anti-unification aims to generalize them into a single sentence (or rule). Anti-unificaion has also been studied in formal logic (Plotkin 1970 Kutsia et al, 2014). We extend it MetaQNT. by adapting prior work. For simplicity, we define anti-unification only for sentences, but it applies to rules as well.
Definition C.6 (Anti-unifier). Given two sentences $1 and 82, their anti-unifier is a triple (s,0), 02) of a sentence and two subsitutions Ø1, 02, such that 01s $1 and 022 $2.
Definition C.7 (Most specific anti-uniferr. Let (s, 01, 02) be an anti-unifier of sentencens 81 and 82, is a most specific anti-unifier if and only there no substitution is, of and og such that
1. σ = o 02 = =020
sos <8
3. ( o22) is also an anti-unifier of and 82
Definition C.8 (Complete set of anti-unifiers). Let. be a set of anti-unifiers of sentences 81 and 82, is complete if and only if for any anti-unifier (2)0)) of 81 and $2, there exists substitution yp and an anti-unificr (4s,,0), of o3) such that 0, 0' p, d2 02 p.
Definition C.9 (Minimal set of anti-unifiers). Let A be set of anti-unifiers of sentences 81 and 82, is minimal if and only if for any (2, (8', d(,')),)))
A, if there exists substitution &p such that
= 408
2. 01 oi o s, 02 0200 o
then o must be an a-conversion, i.e. fos= = s (modulo a-conversion).
Definition C.10 (Minimal complete set of unti-uiiferr). Let A be set of anti-unifiers of sentences and $2, A a minimal complete set of anti-unifiers if and only if it both minimal and complete.
Given two sentences (or two rules), the anti-unification problem is to compute minimal complete set of anti-unifiers. Unlike unification, the result of anti-unification must be non-empty and finite (Fig. 3
Theorem C.11 81 and 82, then A non-empty and finite.
is finitary). Let A be minimal complete set of anti- anfi-unifiers of sentences
Proof. For any sentences and we have trivial anti-unifier (DX), 01, .2) where 01 = (IX - s1} and = [[x] + sz). Since A is complete, apply Definition C.8 and we will know A must be non-empty.
For any anti-unifier (s. p1, (2) E A, we have 6is = $1 (Definition C.6 Apply Lemma A.2 to derive length(s) < length((pss) = ls)) Therefore, the length of is bounded. Also, s cannot have non- variable tokens besides those $1. so its vocabulary also bounded. There are a finite number of different sentences that can take. Therefore, A must also be finite.
20

---

Published in Transactions on Machine Learning Research (05/2023)
Our current anti-unifccation algorithm is adapted from Kutsia et al. (2014) It recursively matches the beginning of two sentences. Let 81 and be sentences, and is more general sentence in their anti-unifier. If 81 and 92 start with the same word w, should also start with w. Otherwise, should start with a variable corresponding to some prefixes of 81 and 82. The algorithm searches for such prefixes and anti-unifics the remaining parts the sentences recursively.
D Details of MiniSCAN/SCAN Experiments
MiniSCAN. The 14 MiniSCAN (Lake al. 2019) training examples represented sentences in MctaQNI.
($MAPS_TOR _OS is special symbol):
dax
$MAPS_TOS
RED
lug
$MAPS_ __0
BLUE
wif $MAPS_ $O$
GREEN
zup
$MAPS_TO$
YELLOW
dax fep
$MAPS_TO ___
RED RED
lug fep
$MAPS_TO$
BLUE BLUE BLUE
wif blicket dax
$MAPS_TH _
GREEN RED GREEN
lug blicket wif
$MAPS_TOS
BLUE GREEN BLUE
dax kiki lug
$MAPS_TOP
BLUE RED
lug kiki wif
$MAPS_ TO8
GREEN BLUE
lug fep kiki wif lug kiki wif fep $MAPS_TON
$MAPS_TOR
GREEN BLUE BLUE BLUE
GREEN GREEN GREEN BLUE
wif kiki dax blicket lug wif blicket dax kiki lug "MAPS_TOS
$MAPS_TOS
RED BLUE RED GREEN
BLUE GREEN RED GREEN
The 10 testing examples:
zup fep
$MAPS_ TO$
YELLOW YELLOW YELLOW
zup blicket lug
$MAPS TO$
YELLOW BLUE YELLOW
zup kiki dax
$MAPS_TON
RED YELLOW
zup fep kiki lug
$MAPS_TON
BLUE YELLOW YELLOW YELLOW
wif kiki zup fep
$MAPS_TON TOS
YELLOW YELLOW YELLOW GREEN
lug kiki wif blicket zup zup blicket wif kiki dax fep zup blicket zup kiki zup fep $MAPS_TOS
$MAPS_ TO$
GREEN YELLOW GREEN BLUE
$MAPS_TON
RED RED RED YELLOW GREEN YELLOW
YELLOW YELLOW YELLOW YELLOW YELLOW YELLOW
dax blicket zup wif kiki zup $MAPS_TO$
$MAPS_TON _
RED YELLOW RED
YELLOW GREEN
Below are some examples of candidate rules generated by the rule proposer. Note that many of them are wrong because the premises not sufficient to deduce the conclusion.
21

---

Published in Transactions on Machine Learning Research (05/2023)
T lug fep kiki wif $MAPS_ SOAPS_TO$
GREEN BLUE BLUE BLUE
dax $MAPS_TO TO$ RED
T wif blicket dax $MAPS_ TAPS_TO$ GREEN RED GREEN
lug SMAPS_TO BLUE + lug kiki wif $MAPS_TOU GREEN BLUE
lug SMAPS_TON BLUE lug fep $MAPS_ TO$ BLUE BLUE BLUE
dax $MAPS_TOS RED; lug $MAPS_TOW _0s BLUE wif blicket dax kiki lug $MAPS_ TO$
BLUE GREEN RED GREEN
MetaInduce learns 7 rules corresponding to the ground truth rules of MiniSCAN:
dax
$MAPS_ __0$ RED
lug
$MAPS_ TO$ BLUE
wif
$MAPS_TOS GREEN
zup $MAPS_TOE YELLOW
[A] $MAPS_TOS [B]
[A] fep $MAPS_TOR TO$ [B]
[B]
[B]
[A] SMAPS_TOP [B] [C] $MAPS_TOS [D]
[A] kiki [C] $MAPS_ TO$
[D]
[B]
[A] $MAPS_TON TO$ [B]; ; [C] SKAPS_TOS _O$$ [D] [A] blicket [C] $MAPS_ TO$
[B]
[D]
[B]
SCAN.
Some examples in SCAN Lake & Baroni 2018
walk
$MAPS_TO TOS
WALK
jump
$MAPS_TON TO$
JUMP
turn right
$MAPS_ TO$
RIGHT
jump after turn left
$MAPS_ _
LEFT JUMP
walk right
$MAPS_TOS
RIGHT WALK
walk after run
$MAPS_ TOS
RUN WALK
turn left twice
$MAPS_TOR
LEFT LEFT
turn opposite left
$MAPS_TOS TOS
LEFT LEFT
turn around right
$MAPS_TON
RIGHT RIGHT RIGHT RIGHT
walk around left
$MAPS_TOR TO$
LEFT WALK LEFT WALK LEFT WALK LEFT WALK
Below some examples of the candidate rules generated by the rule proposer.
run $MAPS_ TO$ RUN } walk after run SMAPS_TO TOS RUN WALK
walk $MAPS_TOP TOS WALK; $MAPS_TON TO$ RUN
} walk after SMAPS_TO TO$ RUN WALK
run $MAPS_ TO$ RUN
T jump twice after run twice $MAPS_TOD TO$ RUN RUN JUMP JUMP
run twice SMAPS_TOS RUN RUN
H jump twice after run twice $MAPS_TO, RUN RUN JUMP JUMP
22

---

Published in Transactions on Machine Learning Research (05/2023)
Metalnduce learns 20 rules corresponding to the ground truth rules of SCAN:
walk $MAPS_TOS WALK
look $MAPS __o LOOK
$MAPS_TOS RUN
jump $MAPS_TO __o JUMP
turn right $MAPS TRAPSTTO$>TT RIGHT
turn left $MAPS_ TO$ LEFT
turn opposite left $MAPS_TOS
LEFT LEFT
turn opposite right SMAPS_TOS
RIGHT RIGHT
turn around left SMAPS_TOS
LEFT LEFT LEFT LEFT
turn around right $MAPS_TO$
RIGHT RIGHT RIGHT RIGHT
[A] SMAPS_TOS [B]
[A] left $MAPS_ LEFT [B]
[A] $MAPS_TO$ [B]
[A] right $MAPS_ RIGHT [B]
[A] $MAPS_ TOS [B]
[A] opposite left $MAPS_TO9
LEFT LEFT [B]
[A] $MAPS_TOD [B]
[A] opposite right SMAPS_TOS
RIGHT RIGHT [B]
[A] 1MAPS_TON [B]
[A] around left $MAPS_TOD TOS
LEFT [B] LEFT [B] LEFT [B] LEFT [B]
[A] $MAPS_TOS TOS [B]
[A] around right $MAPS_TOR
RIGHT [B] RIGHT [B] RIGHT [B] RIGHT [B]
[A] $MAPS_TOP [B]
[A] twice $MAPS_TOS [B] [B]
[A] @MAPS_TOS [B] [A] thrice SMAPS_TON [B] [B] [B]
[A] SMAPS_TOD TO$ [B] [C]
$MAPS_TO$ [D] [C] and [A] $MAPS_ [D] [B]
[A] $MAPS_TOS TO$ [B] [C]
$MAPS_TO$ [D] [A] after [C] SMAPS_TO$ [D] [B]
E Details of Taker Experiments
Examples in RuleTaker are lemmatized and converted to lowercase. We also remove periods and insert a space before each comma. Fig. 4 shows the form of ground truth proofs in RuleTaker. For this specific example, our rule proposer would generate 2 candidate rules below:
STRUES the elephant be big; STRUE$ the elephant be tall;
STRUE$ big tall things be strong:
STRUE$ the elephant be strong
23

---

STRUES [A] [B]; Published in Transactions on Machine Learning Research (05/2023)
if something be strong, then it like cats
the elephant be big
the elephant like cats
the elephant is tall
the elephant be strong
big tall things be strong
Figure 4: RuleTTaker contains ground truth proofs in the form of directed acyclic graphs from the assumptions to the conclusion. The nodes in the graph are concrete sentences without variables.
$TRUES the elephant be strong: $TRUES if something be strong then it like cats; $TRUES the elephant like cats
Below are some example rules learned from RuleTaker
$TRUE$ [A] [B]
$TRUE$ [A]
[C];
$TRUE$ if someone [C] and they [B] then [D];
$TRUE$ [D]
$TRUES [A] does not [B];
$FALSES [A] [B]
STRUES [C] [D];
STRUES someone [B] and [C] [D] then they [E]:
$TRUES [A] [E]
STRUE$ [A] be [B]
$TRUE$ [A] be [C];
$TRUE$ [B] [C] things be [E];
STRUE$ [A] be [E]
STRUES [A] be [B];
STRUE$ [A] be [C];
$TRUES someone be [C] and [B] then they [D];
$TRUES [A] [D]
24

---

Published in Transactions on Machine Learning Research (05/2023)
STRUE$ [A] be [B] + $FALSE$ [A] be not [B]
STRUES [A] [B];
STRUE$ if something [B] then it [C]
STRUE$ [A] [C]
F Heuristics for constraining the space of rules
We use few simple and general heuristics for constraining the space of rules and pruning invalid rules generated by anti-unification First, we merge multiple variables that always appear together. For example, the [A] [B] [c] and [D] [E] in the rule below can be merged.
STRUES if [A] [B]
[C]
then [D]
[E]
STRUES [A] [B]
[C]
STRUES [D] [E]
So the rule becomes:
$TRUES if [A] then [B];
$TRUE$ [A]
$TRUE$ [B]
A variable in a rule is called free variable, if it appears only once. For example, the rule
if something is red, then tomorrow will be sunny;
[X] is red
T tomorrow will sunny
contains a free variable [x]. We only consider rules with no more than 1 free variable and require that they cannot appear in the conclusion. Because they would allow arbitrary conclusions formed by substituting them with other sentences. For example, the rule below is not allowed because of the free variable [x] in the conclusion:
$TRUES today sunny | $TRUES Tommorow is [X]
In addition, rule cannot contain a premise made of one single free variable. Bocause this premise can be satisfied by any sentence, and there point including it in the rule. For example, the rule below is not allowed because of the free variable [x]:
$TRUE$ [X];
$TRUE$ if [A] then [B];
STRUE$ [A]
$TRUE$ [B]
25


Reviews:
[{"review_id": "dVI3tdHQna", "reviewer": "Reviewer_HDXx", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "# Strengths\n- Interesting and important avenue to apply ILP-style systems to fuzzier/more ambiguous datasets.\n- Good variety of both synthetic and less synthetic datasets observed. I personally don't take much stake in the synthetic reuslts, as it's somewhat unsurprising that MetaInduce (and indeed any ILP system) can 100% such tasks with rigid logical grammars. But the more naturalistic datasets are a good attempt.\n- Interesting proposal to blend pretrained LMs with rule based systems, with some promising results here.\n\n# Weaknesses\nMy biggest concerns with the paper have to do with clarity and relation to existing work. Unfortunately I am not super familiar with the literature on ILP and continuous approximations thereof, so I am not in a super strong position to judge the novelty or relation to other work. \n- However, from my cursory knoweldge of ILP, my main concern with the paper is that either empirical comparisons to related attempts at making \"soft\" versions of ILP is missing from this paper. Either that, or greater discussion about the differences between this work and existing work. For example, I am familiar with $\\partial \\text{ILP}$, by Evans and Grefenstette, one of the early attempts at learning softer ILP systems via gradient descent. But such approaches are not examined in this paper—they are dismissed as learning rules restricted to \"binary predicates\". As Evans and Grefenstette note, however, restricting to binary predicates does not result in a loss of generality, since any logical system can be decomposed into more but simpler binary rules. I don't beliee this is a constraint that is \"domain-dependent and difficult to get right\". Moreover, it's ideal if authors explain how the tasks they explore indeed leverage n > 2-ary predicates to a greater degree than that handleable by $\\partial \\text{ILP}$. Could authors respond to these points?\n- Moreover, going off of the author's related work section, I think a bit more context is need. Authors mention several existing weaknesses of the existing work, e.g. Unification Networks, and dismiss them as \"less general\", with the system not supporting multi-step reasoning. These may be true, but one question I have is whether the tasks explored in this paper are indeed unsolable by these existing systems. Specifically, do the tasks in this paper indeed dependent on certain properties (multi-step reasoning, variable binding to sentence fragments) that are only handlable by MetaQNL? Some qualitative evidence that this is the case (e.g. some examples of multi-step proofs or variable bindings) would be nice to have here. For example some tasks still look like one-step reasoning (SCAN/Morphological analysis) if I'm not mistaken, so some clarification would be good here.\n- Soft matching only at test time seems like a good first step, but also a fairy limited attempt. Being able to do soft matching at test time doesn't seem to matter if you need to use soft matching at training time in order to learn the right model in the first place. It seemsl ike the success of using soft matching at test time must be explained by the fact that tasks are easy enough to learn w/o soft matching at training time. Could authors comment on this?\n\n# Conclusion\n\nOverall, it is clear that MetaInduce is in a fairly early stage, with limited (although promising) experiments and a somewhat unclear comparison to the rest of the ILP literature. Overall, it is clear that the paper will be of interest to many in TMLR's audience, and I appreciate the concerted effort towards a paradigm that is *not* deep learning nowadays, so I am leaning positive on the paper as is (though I don't feel strongly). I'd be more strongly in favor of acceptance if authors compared to more existing approaches for neurosymbolic learning, or clarify more why such comparisons are not warranted beyond what is already discussed in the related work.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper proposes a framework and algorithm for learning logical rules from (possibly noisy) sentences in the style of inductive logic programming (ILP). The authors correctly note that existing methods for ILP are brittle and unable to handle domains with softer reasoning and noisier, more ambiguous input, as is commonplace in natural language.\n\nThis work is an attempt to bridge the gap of promises of ILP: a system that can infer rules from possibly noisy data, while gracefully handling natural language. It consists of the following steps:\n\n1. Define the problem: a set of provable and unprovable examples, where each example is a tuple of (A, g), where A is the assumptions and g is the goal. The goal is to learn the simplest possible model M with rules consisting of transformations of the assumptions in A -> g that proves all of the provable examples and cannot prove the unprovable examples.\n2. Rule proving: for each example in the dataset, propose rules consistent with each example (But not necessarily correct)\n3. Use standard forward/backward chaining to construct proofs given the proposed rules.\n4. Generalize instances of concrete rules (e.g. \"if an elephant is big, it is heavy\") to rules with variables (\"in X is big, X is heavy\") via a process called anti-unification\n5. Simplify the model as much as possible, via rule pruning, represented as a MAXSAT problem.\n\nThe key innovation over prior work seems to be the attempt at soft matching: the ability for MetaInduce to handle software natural language statements, rather than rigid logical systems. The apply this system only at test time: given a set of assumptions and a rule that transforemrs assumptions into conclusions, instead of rigidly depending on exact string matching, they can use soft string matching, or train a transformer LM, to propose a list of approximate conclusions with scalar matching scores.\n\nThe authors show that their proposed method solves synthetic logical datasets like SCAN and RuleTaker at 100% accuracy (being more efficient than nerual approaches) and is also able to handle fuzzy ambiguous datasets, as evaluated on a morphological induction dataset and a natural language version of RuleTaker. They show promising results in this domain, again compared to neural network baselines.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "As in the section above, I think this paper is possibly fine as is (borderline) but would be much more solid if some more explanation of differences (and/or empirical comparisons if warranted) to existing fuzzy ILP systems. These are not crucial to securing my recommendation but I believe would make the paper stronger.\n\nMinor typo page 12: paste -> past.", "broader_impact_concerns": "None that I can see.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "BqJA2dftDu", "reviewer": "Reviewer_kVrX", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n\n- S1: The approach is well-motivated through discussion of how rules and learning are not incompatible\n\n- S2: The proposed meta-language and algorithm are both described clearly (with a couple minor exceptions - see below), and the design decisions seem sensible\n\n- S3: The experiments are thorough, covering a range of domains\n\n- S4: The results are impressive. Beyond the numerical results, what I found particularly exciting was some additional strengths of their approach compared to neural networks: First, it learns explicit rules which can be examined for correctness (and in many cases the learned rules match ground-truth ones), and the learning process is efficient in time and parameters (at least for the relatively simple cases considered here - as the authors note, the current implementation would struggle to scale up).\n\n\nWeaknesses:\n\n- W1: There are some minor issues with the framing and explanation, which I have listed below under “Requested changes.” However, I did not find there to be any major weaknesses.\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The authors propose an approach for learning symbolic rules from data. This differs from the most prevalent types of learners in that what is learned is a symbolic rule (rather than weights in a neural network), and it differs from the best-known rule-based systems in that the rules are learned rather than hand-coded. The system includes both an abstract language for expressing rules called MetaQNL and a learning algorithm for learning rules called MetaInduce. The authors also augment these components with a soft matching mechanism that can enable the system to handle messy natural language inputs. These approaches provide very strong results on several synthetic reasoning benchmarks as well as respectable results on some more natural real-world datasets.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Critical to securing my recommendation for acceptance:\n\n- RC1: One branch of literature that is missing from the literature review is work in the tradition of Bayesian methods and probabilistic modeling. There have been prominent works in this tradition about learning symbolic rules from data, so it seems like this area should be discussed at least briefly. Here are some representative publications from this area:\n    - Piantadosi et al: The Logical Primitives of Thought: Empirical Foundations for Compositional Cognitive Models\n    - Goodman et al: A rational analysis of rule-based concept learning\n    - Yang & Piantadosi: One model for the learning of language\n\n- RC2: The figures are missing labels, so you can’t see which figure is “Figure 2”\n\n\n\nNot critical to securing my recommendation:\n- RC3: The first 2 paragraphs include many claims about the current state of machine learning. Many of these claims do not have citations (e.g., rule-based systems being brittle; neural nets requiring large amounts of training data and generalizing poorly). It would be nice to add citations for these points (but I labeled this “not critical” because I think all of these points represent standard views in the field, so probably no one will doubt these claims even without citations. Still, citations could be helpful for someone from a different field approaching this paper).\n- RC4: I found it a little confusing how “r” and “cr” could refer to either a rule or a Boolean variable corresponding to the rule - maybe rename the boolean variable to “b_r” and “b_cr” or something?\n- RC5: A fair number of examples from the datasets are ungrammatical e.g., “An elephants smiles”, “The elephant be not tall”). Is this just how the dataset is formatted? If so, it might be worth adding a footnote at the first instance saying “In this dataset, for simplicity, sentences do not perfectly follow English grammar.”\n- RC6: Use of the term “state-of-the-art”: When it is said that a system achieves state-of-the-art results, I typically take that to mean it outperforms all previous systems. However, if I understand correctly, several of the cases where this paper uses the term “state-of-the-art” (e.g., SCAN) instead mean matching previous work, not exceeding it. So I would prefer it if the wording was clearer, perhaps saying “we match or exceed the previous state-of-the-art” so that it is clear that some of the results are matching rather than exceeding.\n- RC7: “In principle, MetaQNL can solve any task to the extent that the task is solvable by computer programs.” To me, “solve” suggests “find a solution to.” However, MetaQNL doesn’t  find the solution, it just represents it. So it might be more accurate to say “MetaQNL can represent a solution for any task which has a solution that can be represented by a computer program.” (I admit that this sounds clunkier, however!)\n- RC8: “our method learns interpretable morphological rules; e.g., the suffix áramos indicates the paste tense.“ I don’t speak Spanish - is this indeed a past-tense suffix in Spanish? Could be worth mentioning. (Also, note that there is a typo: “paste” instead of “past”).\n", "broader_impact_concerns": "None", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "QykdvJyMvx", "reviewer": "Reviewer_5gc4", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "STRENGTHS\n\nThis paper is covering very exciting territory. The idea of inducing rules to enable logical reasoning in natural language is a very nice one. There is significant research in this space recently and I believe that this entry will be of interest to many researchers working here.\n\nWhile aspects of the approach resemble those from prior work, I believe the rule selection using MAX-SAT is novel, as are the particulars of the rule abstraction piece. While it would've been nice to see some ablations to understand the impact of each of these components, the whole procedure together is novel and seems to work well.\n\nIt is nice to see results across three datasets. The generality of the approach is well-supported and the paper analyzes the results on each of the settings convincingly, with each setting bringing some new and different insight.\n\nBased on the results, the claims this paper makes are well-supported.\n\nWEAKNESSES\n\nI believe the strengths in general outweigh the weaknesses for this paper. However, there are a few weaknesses.\n\nThe biggest weakness of this paper is that the main results are on artificial datasets. A procedure like MetaInduce/MetaQNL is likely to work well compared to neural networks when the underlying data reflects a regular inference process that MetaQNL can represent.  However, as the paper discusses in limitations, many approaches which work for RuleTaker do not generalize to other settings like EntailmentBank or other types of commonsense reasoning.\n\nI do buy the argument that this is a first step and that it will take time to flesh out approaches like these and get them to the same level as more neural-first approaches. However, some of the challenges like scalability mentioned in 4.3 and the need for soft matching in 5 can quickly become unmanageable problems when carried to more realistic settings, and I question how easy it will be to address those shortcomings.  The neural theorem proving line of work has been around for a while, yet most of the winning neurosymbolic approaches look like slightly structured versions of neural inference (e.g., chain-of-thought) rather than NTPs. I don't see anything in this paper to really convince me that that state of affairs is going to change.\n\nAs a result, I think the low rule counts (a selling point of the results) don't reflect any magic properties of this approach, merely that these datasets can be fit with low description-length models. This is reflected by the fact that the model seems to struggle on Swahili and Turkish morphology and the soft matching doesn't alleviate this.\n\nThe related work section is generally quite complete. There are, however, a few recent papers particularly relevant to the idea of rule learning in natural language:\n\n* Weir and van Durme Dynamic Generation of Interpretable Inference Rules https://arxiv.org/pdf/2209.07662.pdf\n* Dalvi et al. Towards Teachable Reasoning Systems EMNLP 2022 https://arxiv.org/pdf/2204.13074.pdf\n* Bostrom et al. Natural Language Deduction with Incomplete Information EMNLP 2022 https://arxiv.org/pdf/2211.00614.pdf\n* Sanyal et al. Faithful and Robust Deductive Reasoning over Natural Language ACL 2022 https://arxiv.org/pdf/2203.10261.pdf\n\nThese are other recent papers in natural language reasoning:\n\n* Creswell et al. Selection-Inference ICLR 2023 https://arxiv.org/abs/2205.09712\n* Creswell and Shanahan Faithful Reasoning https://arxiv.org/abs/2205.09712\n\nI do not think all of these necessarily need to cited, but I wanted to bring them to the authors' attention.\n\nFurthermore, I think that this paper probably could go farther in comparing to other approaches. The systems above present many other ways of doing a similar kind of process, but this paper basically only compares to neural approaches.  When we already have a number of symbolic or neurosymbolic approaches for these tasks, why should a researcher prefer this framework? A better justification here would strengthen the results of the work.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper presents a method for inducing a set of symbolic rules from examples of theorem proving in natural language.  The procedure, called MetaInduce, first involves proposing rules for individual examples, then \"anti-unifying\" those rules to abstract them, then finally pruning them using a MAX-SAT procedure. This procedure enforces that the rules should allow the data to be proven (softly; not every example must be provable) with a parsimonious set of rules.  At test time, a soft matching procedure is employed to be able to handle lexical divergences between assumptions and rules.\n\nResults are given on three datasets: SCAN and MiniSCAN, RuleTaker, and a morphological analysis task from past work.  In the first two settings, the proposed method fits the data nearly perfectly, including on a paraphrased version of RuleTaker, and outperforms PRover and ProofWriter. On the third setting, the method shows mixed performance compared to an LSTM with attention.\n\nAs TMLR is about identifying claims and whether or not they are supported, I will try to identify the paper's claims here.  I believe them to be as follows:\n\nClaim 1: \"We propose MetaQNL, a symbolic system we call a \"Quasi-Natural Language\", which is compatible with not only rigorous logical inference but also natural language (Fig. 1).\"\n\nClaim 2: MetaQNL is Turing-Complete (proven in Appendix B; I won't discuss this claim further)\n\nClaim 3: MetaInduce is a learning algorithm that can be solved efficiently by MAX-SAT solvers\n\nThen various claims about the results, which I believe are all well-calibrated.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Beyond possible modifications to the related work, I do not have any suggested changes for the paper.", "broader_impact_concerns": "None", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper presents MetaQNL, a framework for learning logical rules from natural language data. An important component of the proposed method is the soft matching, removing thus some of the brittleness of previous work. The method is evaluated on 4 datasets reporting positive results wrt to comparisons.

All reviewers agree that this is a very interesting submission and of interest to the TMLR audience. However all reviewers have mentioned a number of discussions currently missing from the paper. Hence, I’m recommending acceptance with minor revisions.

Below are things that would be useful to get into the final manuscript.
* extend the discussion around scalability of method, per Reviewer 5gc4
* add additional literature on reasoning in NL and probabilistic modeling (per Reviewers kVrX and 5gc4)
* include discussion on why some comparisons are not made (per Reviewer HDXx)

Decision: Accept (poster)