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

1 Introduction

• Frontier models have saturated common NLI benchmarks, but the soundness of their reasoning when they predict correct labels remains unknown.NLI asks whether a hypothesis is entailed by, contradicted by, or neutral with respect to a premise.Source: §1 · p. 1
• The paper introduces an explainable NLI task in which models produce structured lexical relations supporting an inference label.The evaluation also uses LLM-generated relations as knowledge for LangPro, a natural-logic theorem prover.Source: §1 · p. 2
• The authors curate entailment problems with necessary and sufficient lexical entailments, then evaluate multiple LLMs on identifying those relations.Their analysis considers model family and size.Source: §1 · p. 2
• The paper evaluates high-performing LLMs as knowledge-base generators by testing whether LangPro can use their relations to prove NLI problems.The authors present this integration as an interpretable combination of LLMs and a symbolic reasoner.Source: §1 · p. 2

2 Related Work

• Free-text explanation progress is hindered by the lack of precise, adequate metrics for comparing generated explanations with references.Span highlights are too noisy to serve as a gold standard for lexical knowledge.Source: §2 · p. 2
• Formal-reasoning and synthetic-dataset approaches rely on simpler language or narrower reasoning patterns than standard NLI benchmarks such as SNLI and SICK.Other work has supplied theorem provers with lexical knowledge using neural models, embeddings, or generated axioms.Source: §2 · p. 2
• Existing entailment problems from SNLI and SICK are augmented with curated, multiple-reference lexical explanations rather than synthetic sentences or simple reasoning patterns.The task is restricted to entailment.Source: §2 · p. 2
• The paper formulates lexical knowledge-base prediction as an independent explainable task, judging relations by whether they explain an inference rather than whether a system can import them.This makes the relations independent of third-party systems and their representation languages.Source: §2 · pp. 2–3

3 Structured Explanation with Lexical Entailments

• The task focuses on entailment because word- or phrase-level relations often represent needed knowledge, whereas neutral and contradiction cases may depend on absence, negation, or other factors.The paper notes that some entailments instead follow from syntactic and compositional reasoning alone.Source: §3 · p. 3
• A lexical entailment is a directed relation from a semantically more specific or equal expression to a more general one.The explicit format supports comparison across annotators and models and direct use by symbolic reasoning systems.Source: §3 · p. 3
• Lexical items include single- and multi-word concepts, with multi-word expressions needed when a component alone yields an invalid or insufficient relation.For example, chinchilla ⊑animal is insufficient for a hypothesis about a small animal; chinchilla ⊑small animal is required.Source: §3 · p. 3
• Relations are normalized to lemmas and exclude determiners, auxiliary verbs, infinitival markers, prepositional phrases, and uninformative modifier-dropping relations.For example, tall man ⊑man is excluded because compositionality licenses the entailment by discarding tall.Source: §3 · p. 3
• LEX sets collect lexical entailments that form the lexical basis of an NLI explanation, but they are not complete formal proofs.They proxy the lexical knowledge that a complete structured explanation must account for.Source: §3 · p. 3

4 Curating a Test Set

• The manually annotated test set draws entailment problems from SICK and SNLI, datasets selected because they heavily depend on lexical knowledge.All four authors served as data curators and annotators.Source: §4 · p. 3
• Each selected problem received three independently produced LEX annotations after initial selection by an author-annotator.The procedure was designed to assess reproducibility and how much annotators identify the same explanatory lexical knowledge.Source: §4 · p. 4
• 44% of 365 annotated problems had unanimous LEX annotations initially, rising to 62% after adjudication.Disagreements could reflect legitimate differences in relation choice, granularity, or how much lexical knowledge was considered necessary.Source: §4 · p. 4
• 139 disagreements could not be reduced to a single canonical LEX, so multiple variants were retained as reference answers.Adjudication sometimes added a fourth variant, suggesting some variation is inherent to the task rather than solely annotator inconsistency.Source: §4 · pp. 4–5
• The test set pairs SICK and SNLI entailment problems with one to four reference LEX sets, including empty sets; 20% contain multiple relations and 29% are empty.Mean annotator performance is 80.9% exact match and 84.9% micro-F1.Source: §4 · p. 5

5 Lexical Entailments for Formal Proofs

• A LEX set can serve as both a structured explanation of an inference and a small, problem-specific knowledge base that may enable a formal proof.For example, chinchilla ⊑small animal represents that every chinchilla is a small animal.Source: §5 · p. 5
• LangPro uses a lexical knowledge base alongside logical rules, but WordNet lacks some relations required by NLI problems.When a required relation is missing, a tableau may remain open even if LangPro’s linguistic analysis and proof rules are otherwise sufficient.Source: §5 · p. 5
• LangPro tests entailment by building a tableau from the premise and negated hypothesis; a proof is established when every branch closes.The resulting tableau is a formal proof whose inference steps can be inspected.Source: §5 · p. 5
• LLMs propose missing lexical knowledge for LangPro; the prover, not the LLM, decides whether that knowledge supports a proof.The setup evaluates whether generated lexical entailments are relevant to formal proof construction.Source: §5 · p. 5

6 Experiments

• The paper evaluates LLMs intrinsically on predicting lexical explanation sets and extrinsically on how much those predictions help LangPro prove NLI problems.The extrinsic evaluation tests whether prover feedback followed by a critical reassessment can improve generated knowledge on a second attempt.Source: §6 · p. 5, §6.2 · p. 6

6.1 Predicting Lexical Explanations

• Eight instruction-following LLMs from four model families are tested to compare higher-capability hosted models with smaller, cheaper alternatives and open-weight models.Each model is run five times with the same prompt, and raw responses are evaluated without automatic post-processing.Source: §6.1 · p. 5
• Exact Match requires a predicted LEX set to equal a reference set, while micro-F1 provides finer-grained matching.Additional lemmatized and argument-unordered F1 scores assess normalization and relation-direction errors.Source: §6.1 · p. 6

6.2 Supplying Knowledge to LangPro

• LangPro is tested on 1,000 randomly sampled SNLI training entailments using WordNet, LLM-generated knowledge, or their combination; LLM settings are one-shot or agentic.After a failed proof, the agentic setup uses a critic diagnosis and revised knowledge base before LangPro tries again.Source: §6.2 · p. 6

7.1 Predicting Lexical Explanations

• Gemma 3 4B performs worst overall, falling below WordNet & Rules on both EM and micro-F1 and below Empty LEX on EM.Model ranking generally follows size, with Gemini 3.1 Flash-Lite an exception that outperforms Gemini 3.5 Flash.Source: §7.1 · pp. 6–7
• Models overgenerate: the top five average 1.4 predicted relations versus 1.0 in reference sets, and produce fewer empty sets (15% vs 29%) and more sets of size 2 (25% vs 14%) and 3+ (11% vs 6%).The substantially higher recall than precision suggests systematic overgeneration, making WordNet & Oracle a strong baseline.Source: §7.1 · p. 7
• Ignoring argument order changes scores by at most 0.6 points, while lemmatization raises micro-F1 by at most 1.6 points for the top five models and at least 4.5 for the remaining models.The latter pattern suggests lemmatized arguments are not a major difficulty for better-performing models.Source: §7.1 · p. 7
• The best model trails annotator performance by 22.7 points in EM and 11.8 points in micro-F1; even the more model-friendly evaluation leaves gaps of 13.9 and 7.1 points, respectively.The model-friendly evaluation excludes problems classified as non-entailment rather than penalizing them.Source: §7.1 · p. 7

7.2 Using LEX to Prove Entailments

• Extrinsic model rankings differ from LEX-NLI rankings, and every LLM still adds relations that enable proofs when combined with WordNet.Gemini 3.1 Flash-Lite and Claude Haiku 4.5 are strongest in one-shot mode but are outperformed in the other configurations.Source: §7.2 · pp. 7–8
• 157 of 1,000 SNLI entailments are proved by LangPro with WordNet alone; agentic GPT-OSS-20B reaches 212 proofs with WordNet.Table 4 reports proof coverage across lexical-knowledge sources; its Δ values indicate gains over WordNet and additional gains from agentic inference.Source: §7.2 · pp. 7–8, Table 4 · p. 8
• Agentic generation improves proof coverage for every model except Gemma 3 4B; GPT-OSS-20B gains 36 proofs without WordNet and 38 with WordNet over one-shot generation.Gemma 3 4B does not successfully revise the relations produced in its initial attempt.Source: §7.2 · p. 8
• On the LEX test set, proof coverage is typically 1.5–1.9 times as high as on the SNLI sample, and all but one model in the LLM-plus-WordNet setting exceed the 34% LangPro-LEX oracle accuracy.The authors note that the LEX test set appears easier and that this extrinsic evaluation is coarser-grained than LEX-NLI.Source: §7.2 · p. 8

8.1 Predicting Lexical Explanations

• Models often overgenerate inflectional variants of the same relation, lowering precision and micro-F1 without affecting recall.This occurs in roughly half of the analyzed cases; more prompt instructions might reduce variant overgeneration but would not improve recall.Source: §8.1 · p. 8
• Models often produce phrasal relations where LEX-NLI expects lexical ones, and no model predicted the expected paint ⊑create and picture ⊑art relations in the example.The prompt’s annotation guidelines deliberately avoided syntax-heavy terminology despite the syntactic distinction between lexical and phrasal relations.Source: §8.1 · p. 8
• Some predictions are unfairly penalized because reference sets contain incorrect relations, omit valid ones, or lack acceptable variants.Examples include look out ⊑view instead of look out over ⊑view, and the omitted make ⊑cause relation.Source: §8.1 · pp. 8–9

8.2 Supplying Knowledge to LangPro

• Only five analyzed problems had an added relation judged semantically reasonable in isolation; in other cases, relations helped compensate for parser errors or weaknesses in LangPro.In one example, adding stand ⊑standing allowed a proof when the hypothesis’s “standing” had been parsed as a noun.Source: §8.2 · p. 9
• Agentic refinement can improve proof success by repairing parser-induced lexical mismatches when reasonable lexical knowledge alone is insufficient.The example proof required both stand ⊑standing and skier ⊑human.Source: §8.2 · p. 9

• The paper introduces LEX sets as structured explanations of inference-specific lexical knowledge and manually annotates a test set that retains multiple references when needed.Source: §9 · p. 9
• 73.1 micro-F1 and 58.2 EM left the best LLM 11.8 and 22.7 points below annotators, respectively, on the primary LEX-NLI evaluation.Source: §9 · p. 9
• LLM-generated knowledge enabled LangPro to find additional proofs, but much of the gain came from semantically unsound relations that compensated for syntactic-analysis errors.Source: §9 · p. 9
• Future work will expand LEX-NLI to more SICK and SNLI problems, use valid overgenerated relations to refine annotations, and extend explanations to other NLI labels and richer structures.Source: §9 · p. 9

• The study covers only entailment, leaving contradiction and neutral cases unexplored, where reasoning may depend on more than directed lexical entailments.Source: Limitations · p. 10
• LEX sets omit syntax, argument structure, quantification, coreference, event relations, and other compositional or world-knowledge phenomena, so they are not complete NLI explanations.Source: Limitations · p. 10
• Although adjudication retains multiple valid LEX variants, the reference set may not include every semantically acceptable explanation.Source: Limitations · p. 10

A LLM Inference Setup

• Each model was evaluated five times with the same nine-example prompt; requested temperature 0 did not ensure identical outputs across provider routes.Source: A LLM Inference Setup · p. 13

B Annotation Guidelines and LLM Prompt

• LEX explanations require minimal, factually acceptable directed relations over lemmatized short phrases, excluding event or social implications unless they are direct paraphrases.Source: B Annotation Guidelines and LLM Prompt · pp. 13–14

C Prompt Selection

• 69.2 mean micro-F1 selected the few-shot precision prompt, compared with 43.8 for zero-shot base, 53.5 for zero-shot constrained, and 65.2 for few-shot base.Source: C Prompt Selection · p. 15

D Mixture of Figures and Tables

• Table 5 evaluates LEX-NLI after excluding examples labeled non-entailment, whereas Table 3 penalizes predictions on those examples.Support is the percentage of problems evaluated; exclusions mostly result from models labeling problems as non-entailment.Source: Table 5 · p. 16
• Table 6 reports LangPro proof coverage on 362 entailment problems using various lexical-KB sources; LLM and LLMa denote one-shot and agentic LLM-generated LEX.Source: Table 6 · p. 16
• LangPro+WordNet proves 66 of 362 entailment problems (18.2%), and the table reports gains over this baseline and additional gains from agentic inference.GPT-OSS-20B is omitted because its model host was unresponsive during the experiments.Source: D Mixture of Figures and Tables · p. 16, Table 6 · p. 16
• The 14 additional problems from Gemini 3.1 Flash-Lite in LLMWN 1 were judged 1 good, 0 mixed, and 13 poor.Source: Table 7 · p. 17
• For 15 additional problems from Gemini 3.1 Flash-Lite after agentic refinement over LLM1, judgments were 3 good, 1 mixed, and 11 poor.Source: Table 8 · p. 18