In the Mood for Inference: Logic-Based Natural Language Inference with Large Language Models (2025)

Abstract: In this paper we explore challenging Natural Language Inference datasets with a logic-based approach and Large Language Models (LLMs), in order to assess the validity of this hybrid strategy. We report on an experiment which combines an LLM meta-prompting strategy, eliciting logical representations, and Prover9, a first-order logic theorem prover. In addition, we experiment with the inclusion of (logical) world knowledge. Our findings suggest that (i) broad performance is sometimes on par, (ii) formula generation is rather brittle, and (iii) world knowledge aids performance relative to data annotation. We argue that these results explicate the weaknesses of both approaches. As such, we consider this study a source of inspiration for future work in the field of neuro-symbolic reasoning.

## introduction natural language inference (nli) is a core task in natural language processing (nlp) and is often presented as a proxy measure of the reasoning capabilities of nlp models. briefly, a model is presented with a premise sentence and a hypothesis sentence and must decide whether the hypothesis is entailed by the premise (e), contradicts it (c), or is neutral with respect to it (n). although many nli datasets have been developed, starting with the sick dataset of @xcite and the snli dataset of @xcite , more attention has recently been put on using nli to measure specific linguistic phenomena. the med dataset, for example, tests for monotonic reasoning @xcite . the curriculum benchmark @xcite is a notable aggregation of nlu tasks (including things like question answering) that have been uniformly formulated as nli tasks. 1 one often heard criticism of nli as a task is that datasets often contain biases and annotation artifacts, and that models trained on them exhibit poor generalization capabilities. it is shown by @xcite for english, and corroborated by @xcite for dutch, that models have a tendency to overtune, and that they fail to properly address negation. that models seem to exploit relatively shallow heuristics such as lexical overlap and sentence length, is confirmed in prior work @xcite , and an effort to repair an existing dataset is done by @xcite . finally, nli models don't necessarily transfer gracefully to other nli datasets @xcite . many of the mentioned datasets and results were achieved with encoder-only models like bert, which can narrowly generalize through finetuning; gradually, this has been replaced by decoder-only large language models (gpt-3 onward), allowing for the nli task to be stated as a text-to-text problem. though this avoids some of the abovementioned pitfalls, the results of @xcite show that generative language models still suffer from bias and additionally are a source of hallucinations, an issue that is persistent for models that are effectively next-word predictors. in order to control the output of model prompting, one method is to specifically constrain model output as a part of the decoding scheme; additionally this has the benefit of guaranteeing syntactic correctness over prompting results, leading to more effective prompting strategies. constrained decoding approaches can work either through vocabulary filters (e.g. only 'e', 'n' and 'c' are valid prompt continuations), or through more sophisticated strategies like generating vocabulary filters determined by finite state automata (aka regular expressions) (willard and louf, 2023) or contextfree grammars @xcite . while these approaches provide some control over model output, they are nevertheless limited to syntactic correctness, meaning they will not fully avoid hallucinations. in this work we use vocabulary filters. mixing llm prompting with logic-based approaches is an emerging field with a number of precedents in nlp. a recent example is the study of @xcite , which combines llm prompting with theorem proving for logical reasoning, with the downside of returning incorrect representations back to the llm to repeat the prompting procedure. another work suggests constrained decoding for a variety of (structured) nlp tasks @xcite , but unfortunately doesn't provide a concrete implementation for most examples. while there is some recent work attempting to bring logical representations in the loop in order to formalize the (chain-of-thought) prompting process @xcite , logic-based approaches to nli are rare, and were mostly performed in the era before llms, typically in a multimodal setting or following a pipeline where sentences are first encoded using a syntactic and semantic parser, after which a classification is made (abzianidze, 2020; @xcite @xcite . in this work we set out to provide a pilot study mixing the above approaches to tackle complex nli test sets with a variety of strategies, including prompting llms for first-order logical representations. foot_1 2 logic-based nli with an llm concretely, our pipeline works as follows: we prompt a model to generate logical representations for a given premise-hypothesis pair, after which we re-prompt the model to generate a (constrained) answer on the (non-)entailment between the premise and hypothesis. whenever relevant, we feed the generated formulas to a theorem prover foot_2 to assess which path is more performant. as a baseline we consider a label only strategy where the model is not prompted for any logical representations but must directly generate the nli label. datasets we evaluate our approach on six different sections of the curriculum benchmark @xcite . the comparative, conditional, negation, and quantifiers datasets are drawn from @xcite and follow the nli format. the lexical entailment section has test set items drawn from @xcite and @xcite , and the monotonicity section has test set items drawn from @xcite and @xcite . these later two sections use the rte format. prompt setup our prompting approach is an example of meta-prompting, i.e., the outcome of the first prompt is included in a second prompt. we distinguish three alternatives: firstly, the label only prompt asks the model to directly generate an nli label, constrained to the three possibilities (e, n, c). second, the formula prompt asks the model to first generate formulas in first-order logic (in a modelfriendly format) for the premise and hypothesis and then is asked to generate a label, hence incorporating both textual and logical representations of the nli instance. finally, there is the formulas and world knowledge setting where the intermediate generation prompt provides formulas and relevant world knowledge in logical form. model choice given that we strive for full transparency in our experiments, we set four desiderata (in order of importance) and choose such that the model (1) has freely available architecture code; (2) has fully specified training data; (3) has a reasonable performance baseline; and (4) is as small as possible modulo the preceding points. given these constraints, we work with zephyr foot_3 , which strikes a balance between performance and model size, and is fully transparent in terms of architecture code and training data. for this dataset, it seems that generating formulas causes the model to predict a logical relationship between sentences where in fact none exists. priming the model to generate formulas for relevant world knowledge helps in some cases, but the effect is much more mixed. for example, it is beneficial for entailments in the comparative and quantifier datasets, but detrimental for the other two labels in the same datasets. it is possible that in these cases, asking the model to generate world knowledge biases it more towards finding an entailment in general. theorem proving we secondly note that the labels inferred from the generated formulas are not always an improvement over the model's direct answer. for the neutral (or non-entailment) columns, we see that the prover9-inferred label accuracy is typically higher than the direct answer (often much higher), but recall that we infer a neutral label whenever prover9 cannot find a proof of the hypothesis (or its negation) from the premise and any relevant world-knowledge formulas, so these apparently good results for neutral items may just be evidence that the generated formulas don't fully capture the logical relationships that would be required to draw an inference if there were one. this can happen when the model produces formulas that are unrelated to each other for the wrong reasons (e.g., inconsistently translated predicates). there are, however, several other cases where the inferred label accuracy shows a notable performance improvement over the direct answer. prover9 accuracy is significantly better for contradiction-labeled items in the negation dataset, and it is somewhat better for entailments of the lexical dataset in the prompt scheme that includes world-knowledge formulas. overall, while there are some cases in which the label inferred from the generated formulas outperforms the direct-answer label, there are even more cases where generating the formulas improves the direct answer but the formulas themselves cannot be used to infer the correct label. this suggests that the utility of prompting the model for formulas is mostly in priming it to attend to the logical relationships between the natural language sentences. upon closer inspection, we suspect that the logical representations for the premise and hypothesis are often not linked together logically, pushing the theorem prover towards neutral. ## conclusion this work investigates the use of constrained decoding and llm prompting for natural language inference. we specifically test three setups: (1) an llm is prompted to solve the task directly; limitations we consider this work a pilot study investigating the applicability of constrained decoding to support nli systems based on llm prompting. this leads to a number of lessons of this work: (1) priming an llm by asking for logical representations increases performance on challenging nli test sets; (2) generating logical representations with only prompt examples as gold standard is too primitive to use in combination with theorem proving; (3) adding world knowledge can mitigate the gold standard issue; (4) with the adequate combination of representation format, language model, and prompt setup one may push the limits of nli; (5) constrained decoding can play a role in controlling llm output and overall performance. future work the findings in this paper warrant a lot of future work; for example, the lack of gold standard data in the test sets we used makes it difficult for the model to tune its generated logical representations, so ideally a gold standard is required. another underrepresented concept is a change in representation format, where predicate logic formulas could be encoded in formats more represented in llm training data, such as python code, or z3 statements. natural logic may also be a promising output format for llms due to its closeness to natural language @xcite . figures 1 , 2 , and 3 show the three different prompt templates used to elicit nli classifications from the llm. only the item_premise and item_hypothesis vary by item, whereas the dataset_labels and example_* fields vary by dataset. the lm_* fields are filled in by the llm. given a pair of sentences, the task is to parse each sentence into first-order logic formulas and ↩→ then determine whether sentence a entails sentence b by labeling the pair with ↩→ <dataset_labels>. the grammar of first-order logic formulas is defined as follows: 1) logical conjunction of expr1 and expr2: expr1 & expr2 2) logical disjunction of expr1 and expr2: expr1 | expr2 3) logical negation of expr1: -expr1 5) expr1 implies expr2: expr1 -> expr2 6) expr1 if and only if expr2: @xmath0: forall x. expr1 8) logical existential quantification over expr1: exists x. expr1 sentence a: <@xmath1: <@xmath2: <@xmath3::: <@xmath4: <@xmath5::: <@xmath6: <@xmath7: <@xmath8: <@xmath9: <@xmath10::: <@xmath11: <@xmath12::: <@xmath13: <@xmath14: the prompt asking the model for first-order logic formulas for the premise and hypothesis, as well as a direct answer. <@xmath15, depending on whether the task at hand uses binary (rte) or ternary (nli) classification; <@xmath16; the three few-shot examples are specific to the dataset the item comes from (see figures 4 5 6 7 8 9 ). given a pair of sentences, the task is to parse each sentence into first-order logic formulas, then ↩→ write first-order logic formulas that capture any relevant lexical knowledge, and finally ↩→ determine whether sentence a entails sentence b by labeling the pair @xmath17. 1) logical conjunction of expr1 and expr2: expr1 & expr2 2) logical disjunction of expr1 and expr2: expr1 | expr2 3) logical negation of expr1: -expr1 5) expr1 implies expr2: expr1 -> expr2 6) expr1 if and only if expr2: @xmath18: forall x. expr1 8) logical existential quantification over expr1: exists x. expr1 sentence a: <@xmath19: <@xmath20: <@xmath21::: <@xmath22: <@xmath23::: <@xmath24: <@xmath25. . . <@xmath26: <@xmath27: <@xmath28: <@xmath29: <@xmath30::: <@xmath31: <@xmath32::: <@xmath33: <@xmath34: <@xmath35: the prompt asking the model for first-order logic formulas for the premise and hypothesis, as well as a direct answer. <@xmath36, depending on whether the task at hand uses binary (rte) or ternary (nli) classification; <@xmath37; <@xmath38; the three few-shot examples are specific to the dataset the item comes from (see figures 4 5 6 7 8 9