What does it take for an LLM to carry a natural-language problem all the way to a valid proof, rather than stopping at plausible steps? One paper tackles logical NLI with a three-stage neurosymbolic pipeline that separates proposing derivations, checking them, and assigning the final label, while another introduces CoRA-Bench for testing how well context selectors preserve evidence under shared token budgets across BABILong, LOONG Financial Spotlight, a NoLiMa diagnostic, and LongMemEval.

Prove What You Can: Hybrid Neurosymbolic Reasoning for Logical Natural Language Inference

For NLI-style reasoning tasks, keep proof search, step validation, and final labelling separate, because a theorem prover plus repair stage beats end-to-end LLM reasoning on the hardest benchmarks.

Logical reasoning over natural language requires both semantic interpretation and deductive search. Large language models (LLMs) can propose plausible intermediate derivations, but they often fail to compose them into a complete proof and overpredict uncertainty. Neurosymbolic methods improve search by translating an entire problem into first-order logic and handing it to a prover, but a single bad clause can make the whole translation nonexecutable. We present Hybrid Reasoning, a three-stage pipeline that decouples proposing a proof, validating its steps, and deciding a label. An LLM proposes a structured proof tree with a raw verdict; a theorem prover validates each derivation locally, keeping only the subset it can prove; and an uncertainty-gated repair attempts to re-derive the label from the premises plus the validated derivations, when the raw verdict is UNCERTAIN. Across four benchmarks (FOLIO, ProofWriter, ProverQA, PrOntoQA) and five contemporary LLMs, Hybrid Reasoning is the top-performing method on the two hardest datasets, improving on the strongest baseline by 5.3 points on FOLIO and 4.9 on ProverQA, and reaches ceiling-level accuracy on the easiest. The repair stage operates at 78-98% precision, producing 326 correct relabellings against 19 regressions.

CoRA-Bench: Evaluating Evidence Preservation by Context Selectors Under Token Budgets

Context selection under fixed token budgets needs task-specific tuning, since BM25, dense retrieval, and reranking preserve different evidence types and their ranking changes between evidence recall and downstream accuracy.

Context selection can reduce input length during long-input inference but can remove evidence required to answer a query. We introduce CoRA-Bench, a benchmark for evaluating evidence preservation under shared token budgets. We compare head and tail truncation, BM25, dense retrieval, dense retrieval with reranking, LLMLingua-2, and Provence across BABILong, LOONG Financial Spotlight, a custom NoLiMa diagnostic, and LongMemEval. Evidence-preservation results reveal task-dependent tradeoffs: BM25 achieves 0.921 supporting-fact recall on BABILong at 128K, dense retrieval and dense reranking each achieve 0.908 needle recall on NoLiMa at 64K, and dense retrieval achieves 0.993 answer-bearing-turn recall on LongMemEval at 64K. Evidence, token retention, and complementary reader evaluations use the same selected contexts. Reader evaluations use dataset-native answer metrics and three runs on the same questions, with paired bootstrap confidence intervals. At a 32K budget, BM25 achieves 46.20% BABILong answer accuracy and dense retrieval achieves 71.13% LongMemEval accuracy. The results show that method rankings vary across evidence types and between evidence recall and downstream accuracy.

Papers announced by arXiv on Monday, 9 November 2026, covering submissions from 6 November to 9 November 2026.