Neuro-Symbolic Logical Reasoning with Textual Entailment

1 Introduction

Reasoning-based question answering (QA) is the task of answering a question about a paragraph of text by help of logical deduction. We focus more specifically on yes/no questions, as in the following example:

Context: If someone likes bread, then they like chocolate or cheese. Anyone who likes eating tomatoes hates even the idea of cheese. Lisa is the biggest tomato lover I know, but she is also a fan of bread.

Question: Is Lisa fond of chocolate?

This task is useful not only for answering complex questions, but also for gauging whether a system goes beyond a surfacelevel comprehension of the text. Large Language Models (LLMs) are relatively good at such reasoning tasks, in particular with chain-of-thought prompting. However, LLMs remain black-boxes: chains-of-thought can contain erroneous reasoning steps even when the final answer is correct [Golovneva et al., 2023; Sadeddine and Suchanek, 2025]. Purely symbolic reasoners, in contrast, can deliver a formal proof for their answer. However, they get derailed by phrase variations. In our example, they are unable to see that "is a fan of bread" has the same meaning as "likes bread", jeopardizing the proof.

In this demo paper, we propose a neuro-symbolic method to answer such questions. Our idea is to build on VANESSA a method to verify the reasoning steps of LLMs [Sadeddine and Suchanek, 2025]. The central principle of VANESSA is to use textual entailment to find correspondences between phrases, e.g., to find that "is a fan of bread" entails "likes bread". Once these correspondences have been established, VANESSA runs a symbolic prover to find the answer. The answer is accompanied by a formal proof, in which the only fallible components are the entailment steps.

In this paper, we adapt VANESSA to perform reasoningbased question answering directly. Our method produces answers that are accompanied by transparent reasoning steps and a proof tree. Our experiments on multiple logical QA benchmarks compare our adapted VANESSA to black-box and neuro-symbolic competitors, and show that VANESSA is competitive in overall performance with purely neural methods, while additionally delivering a proof tree. Our graphical user interface allows the audience to interact with the system, pose questions, and inspect the answers and proof trees.

2 RelatedWork

LLMs have been used extensively for all kinds of reasoning problems. Chain-of-thought prompting [Wei et al., 2022] has further increased model performance while giving the user access to a proof, but hallucinations and formal errors still can be present [Golovneva et al., 2023; Sadeddine and Suchanek, 2025]. To address these issues, several works have investigated neuro-symbolic methods that use external tools such as calculators or knowledge bases in combination with LLMs, increasing performance on a variety of tasks [Wang et al., 2023; Fang et al., 2024; Ge et al., 2025; Suchanek and Luu, 2023]. For logical reasoning on text, the most common approach has been to make an LLM parse the input into a machine-readable format such as Prolog [Lee and Hwang, 2024; Borazjanizadeh and Piantadosi, 2024; Yang et al., 2023] or First-Order Logic [Olausson et al., 2023], and then perform reasoning over these structures with theorem provers. However, the parsing into a logical formalism is a black-box step: If we don't trust the LLM on formal reasoning in a chain-of-thought, then there is no reason to trust it on the translation to formal logic.

Our work, in contrast, builds transparent proof trees, in which the only non-symbolic (and hence fallible) components are the textual entailment steps. Thereby, the area of distrust is reduced to a single atomic task, on which LLMs usually perform well. Besides, an entailment step is usually easy to verify manually.

3 VANESSA

VANESSA is a method to verify the reasoning within a chainof-thought [Sadeddine and Suchanek, 2025]. The input to VANESSA is a context, a boolean question, and a chain-ofthought that answers the question. The chain-of-thought is a sequence of reasoning steps, each of which consists of one or more premises and a conclusion. VANESSA then checks every single reasoning step and outputs "Correct" if every step is valid and every premise is grounded in the context or in previous conclusions. VANESSA operates in three phases: (1) a shallow symbolic parsing of the context and the question, (2) an augmentation of the logical forms through textual entailment, and (3) symbolic reasoning. Step (2) can be performed symbolically by string matching (resulting in a fully symbolic variant of VANESSA) or with an LLM (yielding a neuro-symbolic variant, which is more robust to variations in phrasing).

The present work adapts VANESSA to perform question answering directly, without requiring a given chain-of-thought. The input to our adapted method is a context, consisting of simple rules and facts in natural language, and a boolean question (as in the example in the introduction). The context has to be self-contained, i.e., no external knowledge is needed to answer the question (in particular, no mathematical knowledge). There are three possible answers to the question: "Yes", "No" and "Unknown" (if the context does not permit a definite conclusion).

We transform this input into a pseudo-reasoning step, which has the entire context as premises, and the question (in the form of an affirmative sentence) as the conclusion. Like in the original VANESSA, we try to validate the reasoning step. If this succeeds, the answer to the question is "Yes". If it fails, our adapted method then negates the conclusion and tries to validate it. If that succeeds, the answer is "No". Otherwise the answer is "Unknown". When VANESSA successfully finds an answer, it automatically constructs a proof tree, which is presented as an explanation supporting the answer.

4 Experiments

We evaluate our method on several logical reasoning datasets: ProofWriter [Tafjord et al., 2021] ("Depth 5, Open World Assumption" Dev set), ProntoQA [Saparov and He, 2023] (using the 100 first instances of the 4-hop Composed Random set from ProntoQA-OOD [Saparov et al., 2023]), FOLIO [Han et al., 2022], and LogicBench [Parmar et al., 2024]. The latter does not consider the Open World Assumption, and thus makes no distinction between "No" and "Unknown". Hence we manually relabeled negative ground truth examples as either "No" or "Unknown" for the BD, CD, DD and HS subsets, and subsampled those (except HS) to achieve balance between the possible answers.

We compare several approaches: Black-box methods use prompt-instructed LLMs - either to obtain directly an answer to the question, or to obtain a chain-of-thought that answers the question. Gray-box approaches are neuro-symbolic, i.e., they deliver a formal proof, albeit with fallible components. We use LINC [Olausson et al., 2023] and the neuro-symbolic VANESSA. Finally, white-box approaches are fully symbolic, and we use the symbolic VANESSA.

Table 1 shows that, as expected, the black-box approaches generally perform best. In general, the chain-of-thought prompting outperforms direct prompting approach - albeit only on 3 out of the 5 datasets. None of the black-box methods offers a proof tree.

Turning to the white-box approach, the symbolic VANESSA

also performs as expected: Whenever it delivers results, these consistently have the highest precision. It even reaches best overall accuracy on ProofWriter. However, the method falls behind on recall because of its inability to deal with phrasing variations. On the LogicBench datasets, this issue goes so far that the method fails to deliver any verdict at all, always outputting "unknown", which results in an accuracy of 50%

on subsets where half the ground truth labels are "unknown".

Among the gray-box approaches, the neuro-symbolic VANESSA consistently achieves higher accuracy than LINC. On several datasets, VANESSA beats even the black-box approaches, a feat that LINC does not achieve. Overall, our experiments thus show that symbolic and neuro-symbolic meth-

ods can compete with black-box models in terms of accuracy - while additionally providing a symbolic explanation. The neuro-symbolic VANESSA emerges as the best-performing gray-box method.

5 Demo

A demonstration of our system is available at https:// vanessa-demo.org/, and it can be used online or downloaded for local use. The user can input premises and a conclusion for a logical reasoning problem, and run VANESSA in either symbolic or neuro-symbolic mode (Figure 1). The neuro-symbolic variant uses LLaMa3.2-3B. It is somewhat slow in the online interface due to computational requirements, but is usually faster when run locally.

When VANESSA finds a solution to the reasoning problem, the interface displays a proof tree (Figure 2). Green arrows indicate logical deduction, i.e., trustworthy steps. Gray arrows are the potentially erroneous entailment steps, which the user has to check. The interface also shows the parsed input sentences, the detected entailments and a linearized textual proof (Figure 3), allowing users to trace the reasoning process.

In the demo, users can play around with the preset examples that the GUI offers from several benchmarks. Users can also modify the examples, for example by rephrasing sentences to test the system's robustness, adding negations or changing conclusions. Finally, they can also submit their own reasoning

Reasoning Graph

problems and see if the system can give the correct response.

6 Conclusion

We have presented an adaptation of VANESSA for answering natural language questions. Our method capitalizes on the key principle of VANESSA, which uses a formal reasoner and bridges differences in phrasing by textual entailment. Our experiments show that our adaptation of VANESSA can compete with black-box models on the task of reasoning-based question answering, while also providing a proof tree. In a hands-on demo, users can play with the system, explore its capabilities, and submit their own logical riddles.

We hope that this work paves the way for the development of more explainable and transparent logical reasoning systems. All code and data is available at https: //github.com/dig-team/VANESSA/tree/demo, with a video at https://youtu.be/K426slpttaE.

Acknowledgements

This work was partially funded by the NoRDF project (ANR20-CHIA-0012-01).