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⊑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 [] ∅ \lexboxraw [] ∅ \lexboxraw [] ∅
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 [] goggles⊑eye protection ; pool⊑water ; young boy⊑kid \lexboxraw [] goggles⊑eye protection ; pool⊑water ; young boy⊑kid \lexboxraw [] goggles⊑eye protection ; pool⊑water ; young boy⊑kid
P: A woman observes a rusted antique car. H: A woman looks at an old car.
\lexboxraw [] antique⊑old ; observe⊑look \lexboxraw [] antique car⊑old car ; observe⊑look \lexboxraw [] antique⊑old ; observe⊑look at \lexboxraw [dottedlex] antique car⊑old car ; observe⊑look at
P: A person rides his bicycle in the sand beside the ocean. H: A person is on a beach. \lexboxraw [] sand⊑beach \lexboxraw [] ∅ \lexboxraw [] ∅
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. ∅ 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
Raw ↓
Δ Lem.
Δ Un.
Δ Lem.+Un.
Claude Sonnet 4.5
1 00.0
58.2 ( ± 0.2)
73.1 ( ± 0.2)
+0.9
+0.6
+1.5
64.5 ( ± 0.2)
84.2 ( ± 0.3)
Gemini 3.1 Flash-Lite
1 00.0
57.9 ( ± 0.4)
72.3 ( ± 0.5)
+0.4
+0.0
+0.4
64.4 ( ± 0.4)
82.6 ( ± 0.6)
Gemini 3.5 Flash
1 00.0
58.1 ( ± 0.4)
71.9 ( ± 0.4)
+1.0
+0.4
+1.4
63.6 ( ± 0.4)
82.6 ( ± 0.5)
■ WordNet & Oracle
1 00.0
64.1
70.5
–
–
–
1 00.0
54.4
GPT-5.4
1 00.0
57.5 ( ± 1.0)
69.3 ( ± 0.4)
+0.7
+0.4
+1.1
61.0 ( ± 0.4)
80.2 ( ± 0.7)
Table 3: LLMs’ results on the lex -NLI task. Values are reported as the mean ( ± sample standard deviation) across five runs. Results are sorted by raw Micro-F1, computed without post-processing. Δ Lem., Δ Un., and Δ Lem.+Un. report gains over raw Micro-F1 under lemmatized, argument-order-agnostic ( A⊑B matches B⊑A ), and combined scoring, respectively. Support is the percentage of problems evaluated; exclusions are due to error responses from API calls. ■ denotes baseline and oracle systems.
Model
LLM1
LLMa
LLM1wn
LLMawn
\wndeltabox Δwn
\wndeltabox Δwn \agentdeltabox Δa
\wndeltabox Δwn
\wndeltabox Δwn \agentdeltabox Δ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. LLM1 and LLMa denote one-shot and agentic LLM-generated LEX, while LLM1wn and LLMawn 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 Δwn values indicate gains over LangPro+WordNet, while Δ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
Raw ↓
Δ Lem.
Δ Un.
Δ Lem.+Un.
Gemini 3.1 Flash-Lite
89.0
65.1 ( ± 0.5)
77.8 ( ± 0.6)
+0.4
+0.0
+0.4
70.7 ( ± 0.5)
86.6 ( ± 0.7)
Claude Sonnet 4.5
91.7
63.5 ( ± 0.2)
76.9 ( ± 0.2)
+1.0
+0.6
+1.5
69.2 ( ± 0.2)
86.7 ( ± 0.3)
GPT-5.4
85.7
67.0 ( ± 0.9)
76.6 ( ± 0.2)
+0.8
+0.4
+1.2
68.8 ( ± 0.4)
86.4 ( ± 0.2)
Gemini 3.5 Flash
95.2
61.0 ( ± 0.5)
74.3 ( ± 0.5)
+1.1
+0.4
+1.5
66.0 ( ± 0.5)
85.0 ( ± 0.5)
Claude Haiku 4.5
89.0
56.8 ( ± 0.0)
72.1 ( ± 0.0)
+1.7
+0.0
+1.7
62.2 ( ± 0.0)
85.8 ( ± 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. ■ denotes baseline and oracle systems.
Model
LLM1 %
LLMa %
LLM1wn %
LLMawn %
\wndeltabox Δwn
\wndeltabox Δwn \agentdeltabox Δa
\wndeltabox Δwn
\wndeltabox Δwn \agentdeltabox Δ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 LLMa denote one-shot and agentic LLM-generated LEX, while LLM1wn and LLMawn 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 Δwn values indicate gains over LangPro+WordNet, while Δ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 ⊑ standing ; standing ⊑ 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 ⊑ dog ; running along ⊑ running on ; run along ⊑ run on ; along ⊑ on
Poor: modifier dropping plus invalid general substitution
Safety officers standing outside.
Safety officers outdoors.
standing outside ⊑ outdoors ; stand outside ⊑ 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 ⊑ with ; have ⊑ 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 ⊑ perform
Poor: valid only in the staged context
A little girl is petting her white, fluffy cat.
The girl has a pet.
little girl ⊑ girl ; petting ⊑ has ; pet ⊑ 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 LLMaWN agentic refinement over LLM1WN . 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 ⊑ animal ; stream ⊑ water
Good: both relations are generally valid; black dog ⊑ animal is non-minimal but sound
Two skiers stand near a snowy mountain.
Some humans standing.
stand ⊑ standing ; standing ⊑ 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 ⊑ dog ; running along ⊑ running on ; run along ⊑ run on ; along ⊑ 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 ⊑ women ; women ⊑ woman ; in ⊑ wear ; floral wedding dress ⊑ wedding dress ; floral wed dress ⊑ 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 ⊑ woman
Good: generally valid lexical entailment
Safety officers standing outside.
Safety officers outdoors.
standing outside ⊑ outdoors ; stand outside ⊑ 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 LLMa agentic refinement over LLM1 . We judge 3 cases good, 1 mixed, and 11 poor.
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.
Qili Zhang, Qianren Mao, Hanze Cai +11
Zhongguancun Laboratory · Beihang University · Nanyang Technological University +1
Natural language understanding requires interleaving textual and logical reasoning, yet large language models often fail to perform such reasoning reliably. Existing neurosymbolic systems combine LLMs with solvers but remain limited to fully formalizable tasks such as math or program synthesis, leaving natural documents with only partial logical structure unaddressed. We introduce Logitext, a neurosymbolic language that represents documents as natural language text constraints (NLTCs), making partial logical structure explicit. We develop an algorithm that integrates LLM-based constraint evaluation with satisfiability modulo theory (SMT) solving, enabling joint textual-logical reasoning. Experiments on a new content moderation benchmark, together with LegalBench and Super-Natural Instructions, show that Logitext improves both accuracy and coverage. This work is the first that treats LLM-based reasoning as an SMT theory, extending neurosymbolic methods beyond fully formalizable domains.
Hyunseok Oh, Sam Stern, Youngki Lee +1
Seoul National University · U. Mass. Amherst · Microsoft
Real-world arguments in text and dialogues are normally enthymemes (i.e. some of their premises and/or claims are implicit). Natural language processing (NLP) methods for handling enthymemes can potentially identify enthymemes in text but they do not decode their underlying logic, whereas logic-based approaches for handling them assume a knowledgebase with sufficient formulae that can be used to decode them via abduction. There is therefore a lack of a systematic method for translating textual components of an enthymeme into a logical argument and generating the logical formulae required for their decoding, and thereby showing logical entailment. To address this, we propose a pipeline that integrates: (1) a large language model (LLM) to generate intermediate implicit premises based on the explicit premise and claim; (2) another LLM to translate the natural language into logical formulas; and (3) a neuro-symbolic reasoner based on a SAT solver to determine entailment. We evaluate our pipeline on two enthymeme datasets, demonstrating promising performance in selecting the correct implicit premise, as measured by precision, recall, F1-score, and accuracy.
Xuyao Feng, Anthony Hunter
Department of Computer Science, University College London, United Kingdom