Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars (2024)

Abstract: Logical reasoning remains a challenge for natural language processing, but it can be improved by training language models to mimic theorem provers on procedurally generated problems. Previous work used domain-specific proof generation algorithms, which biases reasoning toward specific proof traces and limits auditability and extensibility. We present a simpler and more general declarative framework with flexible context-sensitive rules binding multiple languages (specifically, simplified English and the TPTP theorem-proving language). We construct first-order logic problems by selecting up to 32 premises and one hypothesis. We demonstrate that using semantic constraints during generation and careful English verbalization of predicates enhances logical reasoning without hurting natural English tasks. Using relatively small DeBERTa-v3 models, we achieve state-of-the-art accuracy on the FOLIO human-authored logic dataset, surpassing GPT-4 in accuracy with or without an external solver by 12%.

## introduction language models trained only on natural language show lackluster capabilities at logical reasoning @xcite . as a countermeasure, we can train neural models to match the output of symbolic reasoning systems (e.g., logic theorem provers, or other algorithms) on procedurally generated problems, to sharpen their reasoning capabilities. this process improves accuracy on some human-authored problems @xcite @xcite . previous work on synthetic first-order logic (fol) reasoning datasets, ruletaker @xcite , logicnli @xcite and fld @xcite , write dedicated code reimplementing the fol axioms from scratch to generate proofs, and translate the generated problems to natural language. we propose unigram, a framework for synthetic reasoning data generation, specifically designed to generate problems jointly into multiple languages. we represent grammars with concise and expressive rules binding two languages, and constraints to prune unwanted generations. we write the most extensive grammar of fol semantic fragments to our knowledge. we structure the generated expressions into premise, hy-pothesis pairs, and annotate their logical relationship (entailment/contradiction/neutral) with a fol solver, following the natural language inference (nli) framework @xcite . a simplistic fol nli problem is: premise: everyone who is happy is rich. mary is rich. hypothesis: mary is happy label: neutral. we fine-tune deberta nli models @xcite on unigram-fol and compare it with previous similar datasets. the 184m parameters (basesize) beats gpt-4 augmented or not with external theorem provers, on the folio @xcite dataset. our contributions are as follows: (i) a dataset of reasoning problems expressed in english and tptp (a language that can be interfaced with numerous theorem provers) alongside vampire proof annotations, covering fol with equality and both finite and open domains, improved compositionality, and more extensive quantifiers. (ii) ablations measuring the effect of constraining material conditionals usage, of using realistic english predicates, and of reimplementing logicnli with declarative generation instead of proof tree generation, highlighting that declarative can work better but that a richer logical modeling drives most of the improvement. (iii) a general reasoning problem grammar-based generation framework relying on solvers. the generation library, grammars, models, and generated dataset are publicly available foot_0 . ## related work synthetic datasets for reasoning numerous works investigate the logical capabilities of nlp models using textual datasets and symbolic reasoning @xcite . we focus on the grammarderived synthetic datasets. ruletaker @xcite explores this area with a subset of first-order logic. logicnli addresses a broader fol subset @xcite . fld explores full fol @xcite and increased compositionality. @xcite ; @xcite use a solver to study the satisfiability in natural language using the z3 solver and dedicated generation logic on constrained problems. pron-toqa @xcite generates proofs from ontologies and then derives questions from the proofs to analyze chains of thoughts in language models. other work explore non-standard logic with synthetic dataset, notably probabilistic @xcite , paraconsistant @xcite , epistemic @xcite logics. generation frameworks multiple frameworks already implement generation from handwritten grammars. nltk @xcite has a context-free grammar tool, but cannot natively handle multiple languages or large-scale generation. grammatical framework @xcite is the closest tool to ours. it enables generation from abstract grammars and linearization into concrete grammars (e.g. french and english) but it is translationoriented and not context-sensitive. glif (schaefer and kohlhase, 2020) extends grammatical framework to parse english into logical formulas but is not suited for generation either. 3 scalable dataset generation without forward inference 3.1 forward inference previous nli-style fol reasoning datasets (rule-taker, logicnli, fld) generate examples using proof generators that are based on the axioms of fol. this requires domain-specific generation code and introduces unwanted complexity. elimination and introduction rules can cancel each other and create an illusion of reasoning depth. we found that some examples in the proofwriter dataset (tafjord et al., 2021) directly contain the premise in the hypothesis despite having a reasoning depth of 5. when constructing nli pairs, gen-erating neutral examples requires special strategies introducing a sampling bias, and it can be the same for contradiction generation. proof generation techniques enable high reasoning depth but at the cost of breadth (linguistic variety and reasoning variety). ## application to first-order logic (fol) we use unigram to enrich fol problem generation while also avoiding ambiguity, starting as a superset of logicnli (grammar in appendix b). to create a problem, we uniformly sample 1 to 32 sentences as premises and 1 sentence per hypothesis ensuring that all symbols are present in the premise. we exclude non-satisfiable formulas (paradoxes) in premise groups and hypotheses. we label pairs as entailment if (premise ∧ ¬hypothesis) is unsatisfiable, as contradiction if (premise ∧ hypothesis) is unsatisfiable, and as neutral otherwise. following ruletaker and logicnli, we create problems with predicates over named individuals (e.g. mary is young). we generate genderbalanced english surnames with censusname. we now present new logical modeling features absent from the previous comparable datasets: explicit finite and open domains we explicitly mention the domain when using the quantifiers. we introduce two locations, anywhere, and a room with occupants e.g. mary, and paul are the only persons in the room. which logically means ∀x, room(x) → (@xmath0. we can then quantify over the room (everyone in the room) or anywhere (everyone anywhere). by doing this, we can generate induction problems (checking that everyone in the room is happy if mary and paul are happy) and test reasoning with both finite and open domains. this requires handling fol with equality which was not implemented in previous work. ## conclusion we showed that simple declarative grammars paired with solvers can outperform complex proof tree generators for reasoning dataset generations and released a new fol reasoning dataset, models, and ablations. our framework can help future reasoning research, notably on explanation since fully aligned tptp code can be leveraged to model necessity and sufficiency. we plan to extend unigram to planning, constraint satisfaction and modal logic.