LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models

Propositional logic employs a collection of statements or propositions (denoted as $\mathcal{P}={p_{1},p_{2},...,p_{n}}$, where $p_{i}$ represents a proposition) and builds upon them using logical connectives such as ‘$\land$’, ‘$\lor$’, ‘$\to$’, ‘$\leftrightarrow$’, and ‘$\neg$’. Several inference rules for propositional logic have been defined using which given a set of premises, one can derive a sound conclusion. For example, let’s consider two propositions: $p_{1}$, which states "It is raining," and $p_{2}$, which states "It is cloudy." From these propositions, we can construct a context/knowledge base (KB) with two premises: (1) $p_{1}\to p_{2}$ and (2) $p_{1}$. With this KB, we can conclude $p_{2}$. This inference rule is written as $((p_{1}\to p_{2})\land p_{1})\vdash p_{2}$ and is known as ‘Modus Ponens’. In our study, we explore nine distinct inference rules of propositional logic, extensions of seven of them with one-variable and a universal quantifier, and two axioms of first-order logic as shown in Table 2. These inference rules provide a proper framework for deriving valid conclusions.

In this work, we consider a restricted set of logical axioms for FOL that utilize quantifiers, $\forall$ (universal quantifier) and $\exists$ (existential quantifier). The universal quantifier ($\forall$) denotes that a statement holds true for all instances within a specific category. In contrast, the existential quantifier ($\exists$) indicates that a statement is true for at least one instance within its scope. For instance, a simple extension of propositional ‘Modus Ponens’ is an inference rule where given the premises $\forall(p(x)\rightarrow q(x))$ and $p(a)$, we conclude $q(a)$ (e.g., given “All kings are greedy” and “Sam is a king”, we can conclude “Sam is greedy”). Here, we explore two axioms (EG and UI - in detail in App. C.3) and various inference rules that incorporate the quantifiers (shown in Table 2).

In this work, we analyze a range of logical reasoning templates in NM logics involving “Default Reasoning,” “Reasoning about Unknown Expectations,” and “Reasoning about Priorities.” These templates are inspired by the compilation (Lifschitz, 1989) made in 1989 to evaluate the abilities of various non-monotonic logics that were being developed at that time. Below Table 3 shows examples of NM reasoning. Additional examples are given in App. C.4.

A key aspect of NM logics is to formalize notions such as “normally,” “typically,” and “usually” that are not directly formalizable using classical quantifiers in the first-order setting. The general rule “Heavy blocks are normally located on the table” does not imply that “All heavy blocks are always located on the table”. Rather, this rule allows for exceptions. Our work explores various NM reasoning patterns, as depicted in Figure 1, to delve deeper into the nuances of this type of reasoning.

We introduce two versions of our proposed dataset: LogicBench(Eval)_BQA and LogicBench(Eval)_MCQA. Statistics of both versions are presented in Table 5. For LogicBench(Eval)_BQA, out of 1520, 520 samples are for ‘yes’ and 1000 samples are for ‘no’ labels. For LogicBench(Eval)_MCQA, there are 20 unique samples present for each rule, thus in total 500 unique samples. Furthermore, we synthetically augmented LogicBench(Eval) for training purposes (i.e., LogicBench(Aug)) which consists of 150 unique data samples for each rule for BQA, resulting in a total of 12908 data samples including variations.

Throughout the data generation phase of LogicBench(Eval), the authors conduct a review of the logical formations to ensure they follow the intended logical structure. We examine each narrative for any potential discrepancies, ensuring that they are logically sound and correctly represent the intended relationships between propositions. In addition to the logical formation, we also dedicated considerable effort to eliminating typos and validating the grammar. We also analyze the diversity in terms of different ontology and the logical nature of the LogicBench(Eval) (presented in App. C.1). We mitigate errors encountered during the validation step (presented in App. F).

For BQA, let us consider a set of data instances $\mathcal{I}_{r,L}$ corresponding to the inference rule $r$ and logic type $L$. In this set, $i^{th}$ instance is represented as $\mathcal{I}^{i}_{r,L}=\{(c_{i},Q_{i})\}$ where $c_{i}$ represents narrative context and $Q_{i}=\{q_{1},q_{2},...,q_{n}\}$ represents set of question and its variations corresponding to $i^{th}$ instance. As discussed in §3, each context ($c$) represents logical rules (e.g., All cats have fur. Tom is a cat.) and question ($q$) represents the conclusion (e.g., Does Tom have fur?). To each context and question pair, i.e., $<c,q>$, we assign a label from the set $\mathcal{Y}=\{Yes,No\}$. We assign a label $Yes$ if the conclusion logically entails the context, otherwise, assign a label $No$. To evaluate any LLMs on this setup, we provide $<p,c,q>$ as input to predict a label from $\mathcal{Y}$ where $p$ is a natural language prompt. In the set $\mathcal{I}_{r,L}$ for MCQA, $i^{th}$ instance is represented as $\mathcal{I}^{i}_{r,L}=\{(c_{i},q_{i},O_{i})\}$ where $c_{i}$ represents narrative context and $q_{i}$ represents question and $O_{i}=\{o_{1},o_{2},o_{3},o_{4}\}$ represents four option choices. To each context and question pair, i.e., $<c,q>$, we assign a label from the set $\mathcal{Y}=\{o_{1},o_{2},o_{3},o_{4}\}$. We assign a label $o_{1}$ if the correct conclusion is presented in the first option, and likewise for other labels. To evaluate any LLMs on this setup, we provide $<p,c,q,o>$ as input to predict a label from $\mathcal{Y}$.

We evaluate a range of prompting models including GPT-4, ChatGPT (GPT-3.5-Turbo), Google Gemini-Pro, Llama-2-7B-Chat, and Mistral-7B-Instruct-v0.2. Each model is evaluated in a zero-shot setting where the chain-of-thought prompt is provided to the model without any in-context examples. This approach allows us to determine LLM’s inherent ability to do logical reasoning (based on pre-training), as we can not expect that various logical inference rules/patterns will always be made part of prompts. However, we do evaluate these models in a few-shot setting, and present the results in App. G.

Here, we evaluate performance in terms of accuracy for both tasks, BQA and MCQA. For the BQA, we measure accuracy corresponding to each label, i.e., $A(Yes)$ and $A(No)$. We evaluate each model on three different chain-of-thought prompts and report average results across these prompts. All prompts used for experiments are described in App. H.