Language Models can be Deductive Solvers (2024)

Abstract: Logical reasoning is a fundamental aspect of human intelligence and a key component of tasks like problem-solving and decision-making. Recent advancements have enabled Large Language Models (LLMs) to potentially exhibit reasoning capabilities, but complex logical reasoning remains a challenge. The state-of-the-art, solver-augmented language models, use LLMs to parse natural language logical questions into symbolic representations first and then adopt external logical solvers to take in the symbolic representations and output the answers. Despite their impressive performance, any parsing errors will inevitably result in the failure of the execution of external logical solvers and no answer to the logical questions. In this paper, we introduce LoGiPT, a novel language model that directly internalizes and emulates the reasoning processes of logical solvers and avoids parsing errors by learning strict adherence to solver syntax and grammar. LoGiPT is fine-tuned on a newly constructed instruction-tuning dataset derived from revealing and refining the invisible reasoning process of deductive solvers. Experimental results on two public deductive reasoning benchmarks show that LoGiPT outperforms state-of-the-art solver-augmented LMs and few-shot prompting methods on competitive LLMs like GPT-4. This project is available in https://github.com/Cyril-JZ/LoGiPT.

## introduction logical reasoning is a foundational element of human intelligence, holding a pivotal role in tasks like problem-solving, decision-making, and critical thinking @xcite . recently, substantial advancements have been achieved in the field of nlp through the development of large language models (llms) @xcite @xcite . it has been noted that language models (lms) could potentially display reasoning capabilities when they reach a certain scale threshold (e.g., training compute, model parameters, etc.) @xcite @xcite . to this end, llms can answer logical questions with explicit reasoning steps when prompted with a simple snippet: "let's think step by step." @xcite or step-wise explanations of reasoning (i.e., "chain of thoughts") @xcite . while llms have made significant progress, complex logical reasoning remains challenging @xcite @xcite . some prior works @xcite aimed to enable lms to perform logical reasoning via specialized module fine-tuning, where reasoning is in natural language (nl). however, the ambiguity and complexity of nl can lead to undesired issues such as hallucinations and unfaithful reasoning @xcite . to this end, recent work has begun to augment llms with access to external solvers @xcite @xcite . in this paper, we focus on the logical solvers, which are theorem provers that can be any automated reasoning tool for checking the truth value of logical formulas in symbolic language (sl). invoking logical solvers can guarantee the accuracy of logical reasoning and relieve the burden of llms to execute intricate and precise deductive reasoning. the workflow of the aforementioned solveraugmented lms is depicted in figure 1 @xcite . at the outset, the information on the logical questions is stored in nl. it is subsequently fed into a lm for parsing into a symbolic representation suitable for solver-input format. finally, the sl information is dispatched to a symbolic solver, which yields the truth value of the logical question. however, during this process, any nl-to-sl parsing it is important to note that the nl-to-sl parsing is solely utilized for constructing instruction-tuning data but not for inference process. in our preliminary experiments (refer to in this paper, we introduce logipt, a novel logic-enhanced pre-trained transformer designed to mimic the reasoning process of logical solvers, enabling it to solve deductive reasoning tasks. we first construct an instruction-tuning dataset containing nl logical questions and their corresponding solver's symbolic reasoning process. after filtering out cases having invalid syntax, we fine-tune opensource lms like vicuna or codellama @xcite with this data to create logipt. then, logipt can generate all implied facts given premises and rules, allowing us to determine the truth value of a logical query by matching it with implied facts or outputting "unknown" if it cannot be determined. our pipeline is presented in figure 1 @xcite . we can avoid the syntax or grammatical errors derived from nl-to-sl parsing by directly outputting answers with logipt. our approach is akin to the process of distillation @xcite , whereby we distill knowledge from a symbolic model (i.e., solver) into a neural network (i.e., lm). however, the reasoning process of solvers is invisible to users and we can only obtain the answers without intermediate reasoning steps. we design a pipeline to reveal and formalize solvers' invisible reasoning processes, creating instruction-tuning datasets with visible and interpretable symbolic reasoning steps (see figure 3 ). our main contributions are three-fold: ## logipt in this paper, we aim to remove the dependency on unsatisfactory nl-to-sl parsing and present a novel lm, logipt instructed to imitate the logical reasoning process of solvers for deductive reasoning tasks. to achieve this, we first reveal the solver reasoning process when solving logical problems ( §3.1). then, we construct a solver-derived instruction-tuning dataset, comprising nl logical questions and corresponding sl reasoning steps ( §3.2). finally, we fine-tune open-source llms using this dataset to develop logipt ( §3.3). ## experiments we construct our instruction-tuning data on the training sets of two public deductive reasoning datasets and evaluate logipt on their test sets. ## related work logical reasoning with lms. recent efforts in adapting llms for logical reasoning tasks generally adopt direct fine-tuning specialized modules @xcite @xcite or icl @xcite @xcite , where reasoning in nl is used by both groups of methods. fine-tuning approaches involve training the full model or specialized modules, enhancing llms with module-level logical reasoning skills like proof, enumeration, and abduction @xcite . the icl approaches create specific prompts to encourage llms' step-by-step reasoning skills. common methods encompass cot prompting @xcite , which produces explanations before delivering a final answer, and least-to-most prompting @xcite , which deconstructs a problem into simpler components that can be resolved individually. some recent work has focused on combining neural networks with symbolic reasoning @xcite @xcite , especially the solver-augmented lms that parse nl questions into symbolic representations, then utilizing external logical solvers for answering. despite their impressive performance, parsing errors can lead to solver execution failure and logical question-answering issues. augmented lms for reasoning. recent work has begun to augment lms to overcome their inherent limitations such as the incapacity to access up-to-date information or conduct accurate mathematical reasoning. they augment with external tools and resources, such as the information retriever @xcite , planner @xcite and other pre-trained models @xcite . specifically, to enhance the reasoning capacity, recent work resort to external off-the-shelf solvers including programmatic interpreters @xcite , satisfiability solvers @xcite , logical solvers @xcite or their hybrids @xcite . most of them utilize the lms to parse the nl question to symbolic representations and then invoke solvers to reason in sl. in this paper, we concentrate on logical solvers, automated tools for validating the truth value of logical formulas. ## conclusion in this paper, we propose a novel logipt that can directly act as a logical solver for deductive reasoning tasks. logipt can output all facts implied from nl logical questions, while bypassing the syntax or grammatical errors derived from nl-to-sl parsing of solver-augmented lms. we conducted numerous analytical experiments on two public deductive reasoning benchmarks. evaluation results show that logipt can significantly outperform state-of-the-art solver-augmented lms, and surpass or be comparable with few-shot prompting methods on competitive llms like gpt-4.