Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

Jorryt de Jong; Stefan Moraca; Ettore Cesari; Lasha Abzianidze

cs.CLSep 26, 2026

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

Authors: Jorryt de Jong, Stefan Moraca, Ettore Cesari, Lasha Abzianidze

Organizations: Utrecht University, the Netherlands · Institute for Language Sciences, Utrecht University, the Netherlands

Abstract

Large Language Models (LLMs) are highly capable of natural language reasoning and appear to store a great deal of lexical knowledge, but it is still unclear how much of this knowledge they actually use when reasoning, and whether they use it in the right way. On the other hand, logic-based Natural Language Inference (NLI) systems provide transparent and formally grounded reasoning, but they need to be supplied with rich lexical knowledge to prove inferences beyond purely logical ones. In this paper, we evaluate whether LLMs can identify all lexical knowledge needed to solve NLI problems and how much this knowledge contributes to proof search in a logic-based NLI system. Our research focuses exclusively on structured lexical entailments (e.g., chinchilla $\sqsubseteq$ small animal) as a proxy for structured explanations for NLI problems with an entailment label. First, we curate a dataset for a new task of explaining sentential entailments with a set of lexical entailments. The dataset is used to intrinsically evaluate LLMs on generating structured lexical explanations. Then, we use NLI as an extrinsic evaluation in a simple neuro-symbolic setting, assessing whether LLMs can supply sufficient lexical relations to LangPro, a natural-logic theorem prover for natural language. The results show that the proposed task remains challenging even for hosted proprietary LLMs, and that their contribution to theorem proving is moderate: generated relations are often only partially sound and may be tailored to the specific NLI problem rather than representing generally valid lexical knowledge.

Figures & tables

Figure 1: Overview of the proposed intrinsic and extrinsic evaluation. Given an NLI problem, an LLM is jointly evaluated on the predicted inference label and a structured lexical explanation ( lex ) against human-curated multi-reference lex sets. Extrinsically, the generated lexical relations are supplied to the LangPro theorem prover, which determines whether they suffice to construct a formal proof.

NLI problem with three LEX annotations and an optional 4th alternative LEX

P: A man in a bright yellow shirt juggles while riding a unicycle. H: A man performs a juggling act on a unicycle. \lexboxraw []

\varnothing

\lexboxraw []

\varnothing

\lexboxraw []

\varnothing

P: A young boy wearing safety swimming gear and goggles is in a pool. H: A kid uses eye protection while in the water.

\lexboxraw []

\text{goggles}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{eye protection}

;

\text{pool}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{water}

;

\text{young boy}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{kid}

\lexboxraw []

\text{goggles}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{eye protection}

;

\text{pool}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{water}

;

\text{young boy}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{kid}

\lexboxraw []

\text{goggles}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{eye protection}

;

\text{pool}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{water}

;

\text{young boy}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{kid}

P: A woman observes a rusted antique car. H: A woman looks at an old car.

\lexboxraw []

\text{antique}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{old}

;

\text{observe}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{look}

\lexboxraw []

\text{antique car}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{old car}

;

\text{observe}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{look}

\lexboxraw []

\text{antique}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{old}

;

\text{observe}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{look at}

\lexboxraw [dottedlex]

\text{antique car}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{old car}

;

\text{observe}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{look at}

P: A person rides his bicycle in the sand beside the ocean. H: A person is on a beach. \lexboxraw []

\text{sand}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{beach}

\lexboxraw []

\varnothing

\lexboxraw []

\varnothing

Table 1: Examples of agreement and variation among three independently produced lex annotations. An additional 4th lex , if introduced during adjudication, is marked with a dashed borderline.

\varnothing

stands for an empty lex . The first two problems have unanimous agreement in lex annotations.

Dataset statistics
Total NLI problems			362
SNLI problems / SICK problems			280 / 82
Problems w/ unique lex (unanimous agreement)			223 (61.6%)
Problems with an alternative (4th) lex			22 (6.1%)
Total lex (incl. the added 4th lex )			1108
lex size distribution: 0, 1, 2, 3+			29 / 51 / 14 / 6%

Table 2: Statistics of the final dataset and annotator performance after the adjudication. Annotator-N vs rest is based on the problems annotated by Annotator-N.

Model	Support	Exact match	Micro-F1				Micro- Precision	Micro- Recall
Model	Support	Exact match	Raw $\downarrow$	$\Delta$ Lem.	$\Delta$ Un.	$\Delta$ Lem.+Un.	Micro- Precision	Micro- Recall
Claude Sonnet 4.5	1 00.0	58.2 ( $\pm$ 0.2)	73.1 ( $\pm$ 0.2)	+0.9	+0.6	+1.5	64.5 ( $\pm$ 0.2)	84.2 ( $\pm$ 0.3)
Gemini 3.1 Flash-Lite	1 00.0	57.9 ( $\pm$ 0.4)	72.3 ( $\pm$ 0.5)	+0.4	+0.0	+0.4	64.4 ( $\pm$ 0.4)	82.6 ( $\pm$ 0.6)
Gemini 3.5 Flash	1 00.0	58.1 ( $\pm$ 0.4)	71.9 ( $\pm$ 0.4)	+1.0	+0.4	+1.4	63.6 ( $\pm$ 0.4)	82.6 ( $\pm$ 0.5)
$\blacksquare$ WordNet & Oracle	1 00.0	64.1	70.5	–	–	–	1 00.0	54.4
GPT-5.4	1 00.0	57.5 ( $\pm$ 1.0)	69.3 ( $\pm$ 0.4)	+0.7	+0.4	+1.1	61.0 ( $\pm$ 0.4)	80.2 ( $\pm$ 0.7)

Table 3: LLMs’ results on the lex -NLI task. Values are reported as the mean (

\pm

sample standard deviation) across five runs. Results are sorted by raw Micro-F1, computed without post-processing.

\Delta

Lem.,

\Delta

Un., and

\Delta

Lem.+Un. report gains over raw Micro-F1 under lemmatized, argument-order-agnostic (

\text{A}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{B}

matches

\text{B}\mkern 3.0mu\mathord{\sqsubseteq}\mkern 3.0mu\text{A}

), and combined scoring, respectively. Support is the percentage of problems evaluated; exclusions are due to error responses from API calls.

\blacksquare

denotes baseline and oracle systems.

Model	$\mathrm{LLM}_{1}$	$\mathrm{LLM}_{a}$	$\mathrm{LLM}_{1}^{\text{\!{wn}}}$	$\mathrm{LLM}_{a}^{\!\text{{wn}}}$
Model	\wndeltabox $\Delta_{\text{{wn}}}$	\wndeltabox $\Delta_{\text{{wn}}}$ \agentdeltabox $\Delta_{a}$	\wndeltabox $\Delta_{\text{{wn}}}$	\wndeltabox $\Delta_{\text{{wn}}}$ \agentdeltabox $\Delta_{a}$
Gemini 3.1 Flash-Lite	165 \wndeltabox +8	180 \wndeltabox +23 \agentdeltabox +15	179 \wndeltabox +22	193 \wndeltabox +36 \agentdeltabox +14
Claude Haiku 4.5	165 \wndeltabox +8	176 \wndeltabox +19 \agentdeltabox +11	179 \wndeltabox +22	190 \wndeltabox +33 \agentdeltabox +11
GPT-5.4 Mini	162 \wndeltabox +5	183 \wndeltabox +26 \agentdeltabox +21	178 \wndeltabox +21	199 \wndeltabox +42 \agentdeltabox +21
GPT-OSS-20B	158 \wndeltabox +1	194 \wndeltabox +37 \agentdeltabox +36	174 \wndeltabox +17	212 \wndeltabox +55 \agentdeltabox +38
Gemma 3 4B	163 \wndeltabox +6	163 \wndeltabox 0 +6 \agentdeltabox 0 +0	182 \wndeltabox +25	182 \wndeltabox +25 \agentdeltabox 0 +0

Table 4: LangPro proof coverage on 1,000 SNLI entailment problems when using various sources of the lexical KB.

\mathrm{LLM}_{1}

and

\mathrm{LLM}_{a}

denote one-shot and agentic LLM-generated LEX, while

\mathrm{LLM}_{1}^{\text{\!{wn}}}

and

\mathrm{LLM}_{a}^{\!\text{{wn}}}

are the former two coupled with WordNet, respectively. Values indicate the number of problems proved as entailment. The LangPro+WordNet baseline proves 157 problems . The boxed

\Delta_{\text{{wn}}}

values indicate gains over LangPro+WordNet, while

\Delta_{a}

values indicate the additional gains from agentic inference over the corresponding non-agentic LLM.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Model	Support	Exact match	Micro-F1				Micro- Precision	Micro- Recall
Model	Support	Exact match	Raw $\downarrow$	$\Delta$ Lem.	$\Delta$ Un.	$\Delta$ Lem.+Un.	Micro- Precision	Micro- Recall
Gemini 3.1 Flash-Lite	89.0	65.1 ( $\pm$ 0.5)	77.8 ( $\pm$ 0.6)	+0.4	+0.0	+0.4	70.7 ( $\pm$ 0.5)	86.6 ( $\pm$ 0.7)
Claude Sonnet 4.5	91.7	63.5 ( $\pm$ 0.2)	76.9 ( $\pm$ 0.2)	+1.0	+0.6	+1.5	69.2 ( $\pm$ 0.2)	86.7 ( $\pm$ 0.3)
GPT-5.4	85.7	67.0 ( $\pm$ 0.9)	76.6 ( $\pm$ 0.2)	+0.8	+0.4	+1.2	68.8 ( $\pm$ 0.4)	86.4 ( $\pm$ 0.2)
Gemini 3.5 Flash	95.2	61.0 ( $\pm$ 0.5)	74.3 ( $\pm$ 0.5)	+1.1	+0.4	+1.5	66.0 ( $\pm$ 0.5)	85.0 ( $\pm$ 0.5)
Claude Haiku 4.5	89.0	56.8 ( $\pm$ 0.0)	72.1 ( $\pm$ 0.0)	+1.7	+0.0	+1.7	62.2 ( $\pm$ 0.0)	85.8 ( $\pm$ 0.0)

Appendix

Table 5: LLMs’ results on the lex -NLI task. These scores are more favorable to the models, as examples assigned a non-entailment label are omitted from evaluation; in contrast, Table 3 penalizes predictions on those examples. Support is the percentage of problems evaluated; exclusions mostly result from models labeling problems as non-entailment.

\blacksquare

denotes baseline and oracle systems.

Model	$\mathrm{LLM}_{1}$ %	$\mathrm{LLM}_{a}$ %	$\mathrm{LLM}_{1}^{\text{\!{wn}}}$ %	$\mathrm{LLM}_{a}^{\!\text{{wn}}}$ %
Model	\wndeltabox $\Delta_{\text{{wn}}}$	\wndeltabox $\Delta_{\text{{wn}}}$ \agentdeltabox $\Delta_{a}$	\wndeltabox $\Delta_{\text{{wn}}}$	\wndeltabox $\Delta_{\text{{wn}}}$ \agentdeltabox $\Delta_{a}$
Claude Sonnet 4.5	25.4 \wndeltabox +7.2	32.0 \wndeltabox +13.8 \agentdeltabox +6.6	30.1 \wndeltabox +11.9	35.4 \wndeltabox +17.1 \agentdeltabox +5.2
Gemini 3.1 Flash-Lite	24.9 \wndeltabox +6.6	31.8 \wndeltabox +13.5 \agentdeltabox +6.9	29.3 \wndeltabox +11.0	34.8 \wndeltabox +16.6 \agentdeltabox +5.5
Gemini 3.5 Flash	23.5 \wndeltabox +5.2	33.4 \wndeltabox +15.2 \agentdeltabox +9.9	28.2 \wndeltabox + 1 9.9	37.0 \wndeltabox +18.8 \agentdeltabox +8.8
GPT-5.4	24.3 \wndeltabox +6.1	30.7 \wndeltabox +12.4 \agentdeltabox +6.4	29.3 \wndeltabox +11.0	35.6 \wndeltabox +17.4 \agentdeltabox +6.4
Claude Haiku 4.5	25.7 \wndeltabox +7.5	31.2 \wndeltabox +13.0 \agentdeltabox +5.5	30.9 \wndeltabox +12.7	35.6 \wndeltabox +17.4 \agentdeltabox +4.7

Appendix

Table 6: LangPro proof coverage on the test set (of 362 entailment problems) when using various sources of the lexical KB. LLM and

\mathrm{LLM}_{a}

denote one-shot and agentic LLM-generated LEX, while

\mathrm{LLM}_{1}^{\text{\!{wn}}}

and

\mathrm{LLM}_{a}^{\!\text{{wn}}}

are the former two coupled with WordNet, respectively. Values indicate the percentage of problems proved as entailment. The LangPro+WordNet baseline proves 66 problems (18.2%). The boxed

\Delta_{\text{{wn}}}

values indicate gains over LangPro+WordNet, while

\Delta_{a}

values indicate the additional gains from agentic inference over the corresponding non-agentic LLM. GPT-OSS-20B is omitted because the model host was unresponsive when the experiments were conducted.

Premise	Hypothesis	Added/changed relations	Judgment
Two skiers stand near a snowy mountain.	Some humans standing.	stand $\sqsubseteq$ standing ; standing $\sqsubseteq$ stand	Poor: inflection only; no new lexical knowledge
A black dog is running along the beach.	a dog is running on the beach	black dog $\sqsubseteq$ dog ; running along $\sqsubseteq$ running on ; run along $\sqsubseteq$ run on ; along $\sqsubseteq$ on	Poor: modifier dropping plus invalid general substitution
Safety officers standing outside.	Safety officers outdoors.	standing outside $\sqsubseteq$ outdoors ; stand outside $\sqsubseteq$ outdoors	Poor: semantically plausible but non-minimal
A female is wearing a big purple flower in her hair and has some beads around her neck.	a girl with a flower in her hair	wear $\sqsubseteq$ with ; have $\sqsubseteq$ with	Good: unusual pairs but specific to SNLI & SICK datasets
A man wearing a black hat, white shirt, red vest, black tie, and face makeup is swallowing a sword, while a man wearing a cowboy hat behind him is watching.	A man is performing.	swallow $\sqsubseteq$ perform	Poor: valid only in the staged context
A little girl is petting her white, fluffy cat.	The girl has a pet.	little girl $\sqsubseteq$ girl ; petting $\sqsubseteq$ has ; pet $\sqsubseteq$ have	Poor: modifier dropping plus false possession inference

Appendix

Table 7: Quality judgments for the 14 additional problems obtained by Gemini 3.1 Flash-Lite in

\mathrm{LLM}^{\mathrm{WN}}_{a}

agentic refinement over

\mathrm{LLM}^{\mathrm{WN}}_{1}

. We judge 1 case good, 0 mixed, and 13 poor.

Premise	Hypothesis	Added/changed relations	Judgment
A black dog is walking through a stream of water.	An animal is walking through water.	black dog $\sqsubseteq$ animal ; stream $\sqsubseteq$ water	Good: both relations are generally valid; black dog $\sqsubseteq$ animal is non-minimal but sound
Two skiers stand near a snowy mountain.	Some humans standing.	stand $\sqsubseteq$ standing ; standing $\sqsubseteq$ stand	Poor: inflection only; no new lexical knowledge
A black dog is running along the beach.	a dog is running on the beach	black dog $\sqsubseteq$ dog ; running along $\sqsubseteq$ running on ; run along $\sqsubseteq$ run on ; along $\sqsubseteq$ on	Poor: modifier dropping plus invalid general substitution
An Asian woman in a floral wedding dress poses on a bridge close to her bridesmaids.	An asian women is wearing a wedding dress.	woman $\sqsubseteq$ women ; women $\sqsubseteq$ woman ; in $\sqsubseteq$ wear ; floral wedding dress $\sqsubseteq$ wedding dress ; floral wed dress $\sqsubseteq$ wed dress	Poor: inflection, context dependence, modifier dropping, and malformed forms
A lady walking down stairs with a green poster pod on her back.	A woman walking down stairs with a green thing on her back.	lady $\sqsubseteq$ woman	Good: generally valid lexical entailment
Safety officers standing outside.	Safety officers outdoors.	standing outside $\sqsubseteq$ outdoors ; stand outside $\sqsubseteq$ outdoors	Poor: semantically plausible but non-minimal

Appendix

Table 8: Quality judgments for the 15 additional problems obtained by Gemini 3.1 Flash-Lite in

\mathrm{LLM}_{a}

agentic refinement over

\mathrm{LLM}_{1}

. We judge 3 cases good, 1 mixed, and 11 poor.

Explore similar work

Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
Sep 29, 2026Qili Zhang, Qianren Mao, Hanze Cai +11Logical Reasoning RL for Language Model Reasoning
Zhongguancun Laboratory · Beihang University · Nanyang Technological University +1
Neurosymbolic Language Reasoning as Satisfiability Modulo Theory
Feb 20, 2026Hyunseok Oh, Sam Stern, Youngki Lee +1Neuro-Symbolic Reasoning Satisfiability Modulo Theories
Seoul National University · U. Mass. Amherst · Microsoft
Making Implicit Premises Explicit in Logical Understanding of Enthymemes
Mar 6, 2026Xuyao Feng, Anthony HunterNatural Language Inference Implicit Reasoning in Language Models
Department of Computer Science, University College London, United Kingdom

Sep 29, 2026J/K move · Enter open · S save

Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning

Qili Zhang, Qianren Mao, Hanze Cai, Kaiming Zhao+10

Zhongguancun Laboratory · Beihang University · Nanyang Technological University+1

Logical Reasoning RL for Language Model Reasoning

Open paper AskPDF arXiv

Large language models (LLMs) are increasingly deployed for natural-language logical reasoning, where the final answer is easy to check but the proof behind it is not. In natural-language logical reasoning, an intermediate conclusion should follow from its premises, and the resulting derivation should support the final answer. Existing methods lack machine-checkable verification of intermediate conclusions and answer-supporting proof dependencies, so they may assign credit to invalid or answer-irrelevant steps. We propose Proof-R1, an RL framework from formal verification that trains LLMs to construct verifiable proofs for natural-language logical reasoning. Proof-R1 admits a generated conclusion into the verified proof state only when the corresponding reasoning action satisfies the proof obligations through UNSAT-based machine-checkable formal verification. Proof-R1 also recovers the answer-supporting dependency closure to trace the proof structure of the final answer and align outcome credit with the proof dependencies. Experiments demonstrate that Proof-R1 improves answer accuracy across three logical reasoning benchmarks and four backbone models and outperforms training-free agents and training-based methods in terms of reasoning-process verifiability.

Abstract

Explore similar work

Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

Making Implicit Premises Explicit in Logical Understanding of Enthymemes