Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation (2024)

Abstract: Advancements in logical reasoning, utilizing LLMs to convert natural language into logical symbolism, combined with the use of external theorem provers, have repositioned the symbolic approach as a central point of interest. The main challenge within this paradigm lies in the LLMs’ capability to accurately translate natural language (NL) statements into first-order-logic (FOL) expressions. Although LLMs have shown notable success, there remains a gap in understanding the limitations and challenges they encounter in NL-FOL translation. This is primarily due to the absence of datasets and evaluation test beds at the required fine-grained level. We present MALLS, a dataset of 28K diverse and verified sentence-level NL-FOL pairs collected from GPT4. We utilize a combined strategy of FOL rule parsing, human annotation, and automatic filtering to ensure quality. We also present LogicLLaMA, a LLaMA2-7B/13B fine-tuned on MALLS for NL-FOL translation, which can be used standalone or to correct previously generated rules by GPT3.5 after being further fine-tuned via a novel reinforcement learning with human feedback (RLHF) framework. We benchmark a wide range of LLMs on MALLS and previous datasets, highlighting weaknesses in them in NL-FOL translation and demonstrating the advantages of MALLS. We also show that LogicLLaMA achieves GPT4-level performance and can generalize to other datasets. Project repo is available at https://github.com/gblackout/LogicLLaMA

## introduction the traditional logic-based approaches to reasoning @xcite @xcite , once regarded as foundational for many core nlp tasks, lost popularity due to their limited scalability and coverage. the rise of end-to-end deep neural networks has garnered significant attention because of their impressive downstream performance @xcite , although at the cost of losing interpretability. the recent remarkable progress of large language models (llms) has revitalized interest in logic, placing it once again at the forefront of reasoning. one straightforward approach to harness the power of llms such as gpt4 @xcite is to first translate natural language (nl) statements (e.g., premises and conclusions in textual entailment task) to first-order logic (fol) formula via incontext learning, and then pass the symbolic forms to symbolic mathematical theory (smt) solvers. this approach has significantly surpassed the performance of llm-only methods such as chainof-thought @xcite and has established new state-of-the-art for complex deductive reasoning tasks @xcite @xcite . despite the success of this new promising direction, very little is understood about the difficulties current llms face in the nl-fol translation task itself. this is mainly due to the absence of finegrained curated data of nl statements and their corresponding fol, with controlled complexity and diversity that enables a categorical study of the capabilities and shortcomings of llms in translation. this is crucial to understand what exact kinds of complexity the model builders should target to improve. annotating the fol rules for nl statements is expensive and requires domain expertise. most of the existing logic reasoning datasets do not have parallel fol annotations. logicnli @xcite and folio @xcite are the few exceptions that provide nl-fol pairs with sentence-level fol annotation ( nl: if people order takeout from delivery services often, then they grow their own fresh vegetables in their home garden. fol: ∀x (takeout(x) → garden(x)). error: oversimplified fol; does not align with nl malls nl: a car must have a motor and wheels to be considered functional. fol: ∀x car(x) ∧ functional(x) → (hasmotor(x)∧ haswheels(x))). error: none nl: a grocery store sells food and household items. fol: ∀x∃y∃z(grocerystore(x) ∧ food(y) ∧ householditem(z) ∧ sells(x, y)∧ (sells(x, z)). error: none we present malls (large language model generated nl-fol pairs), a 28k real-world, diverse, and verified sentence-level nl-fol pairs collected from gpt4. compared to prior datasets ( on top of malls, we present logicllama, a llama2-7b/13b model family @xcite for nl-fol translation fine-tuned with lora @xcite . logicllama can be used for (1) directly translating nl to fol as a standalone translator and (2) can be used in combination with more powerful general-purpose models such as gpt3.5, where it serves a "correction model" that corrects outputs from gpt3.5, which we found yields better performance with a fraction of the cost of gpt4 1 . in particular, we propose a novel data augmentation and reinforcement learning with human feedback (rlhf) framework that 1 as of feb 2024, gpt3.5 costs @xmath00.06/1k. we summarize our contributions as follows: (1) we present malls, a 28k real-world, diverse, and verified sentence-level nl-fol pairs collected from gpt4, which, to the best of our knowledge, is the largest dataset to date in this category. (2) we also present logicllama, a llama2-7b/13b model family fine-tuned on malls, which, in the experiments, achieves gpt4 level performance on nl-fol translation tasks on three benchmarks. traditionally, nl-fol translation is addressed via rule-based methods @xcite @xcite . due to the complexity of natural language, these methods are difficult to scale to real-world applications. recently, there has been an increasing interest in approaching this task via neural approaches @xcite @xcite @xcite , which gives rise to a new paradigm of using llms for translation. recent works @xcite @xcite have successfully used gpt models for translation via in-context learning (icl). while they demonstrate impressive downstream task performance, it is crucial to study how these llms perform in fine-grained categories. more importantly, gpt-based icl methods come with several limitations: (1) as of feb 2024, gpt-4 costs $0.06/1k tokens and can be expensive to run; gpt-3.5, while costs less, struggles with complex translation ( §5); (2) they are closedsource and subject to constant updates, making it difficult for privacy-sensitive use cases and reproducing results for academic purposes; (3) they lack extendability for future integration with downstream tasks such as nli and qa. therefore, is it valuable to have small and open-source llms with gpt-level performance while preserving privacy and extendability. ## malls creating a dataset of diverse nl statements with faithfully aligned fol annotations is crucial to evaluating and fine-tuning llms for logic-based reasoning. existing datasets ( ## logicllama nl-fol translation besides evaluation, malls makes it possible to fine-tune local llms such as llama2-7b/13b to reach gpt4-level performance, which we refer to as logicllama. unlike typical nlp tasks, where one fine-tunes with a naive autoregressive objective, fine-tuning for nl-fol translation is nontrivial. in §4.1 and §4.2, we present three ways to train logicllama. and in §4.3, we propose two metrics for evaluating an fol rule against the ground truth. ## experiments we address the following questions in the experiment section: (q1) how good is malls for evaluating existing llms? does it provide better insights into the shortcomings? (q2) how good is malls for fine-tuning? can we train logi-cllama that also generalizes to other datasets such as folio? (q3) how well does the logi-cllama perform in direct translation mode and correction mode? dataset. for malls, we use the humanannotated subset (1k) as the test set; we hold out 2k samples as the valid set, and the rest samples are used for training (t1-3); we also include 1k pairs from the training set of logicnli since it has a different rule distribution where rules are mostly grounded rules (i.e., many of them do not contain any variables) instead of fol rules. we evaluate the llms on malls test set as well as the full folio dataset and the test set of logicnli. methods. to answer (q1) and (q2), we evaluate logicllama together with a wide range of llms on the task of nl-fol translation: llama2-7b/13b, mistral-7b, mixtral, gemini metrics. we use the logical equivalence (le) introduced §4.3 as the main metric for fol rules evaluation. apart from this, it is also preferred that the generated fol rule has the matching predicate names, so we measure the fol bleu between the predicted fol and the ground-truth fol. note that bleu is a noisy metric: bleu is computed over the fol text tokens and does not recognize the underlying logic structures, thus can have a low score even if the rules are equivalent.