# Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference

arXiv: https://arxiv.org/abs/2311.08637 · HTML: https://mlsanity.com/paper/2311.08637/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 15 of its 26 references that are in the map.
- First posted on arXiv 15 Nov 2023.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 15 of 15)

- [A large annotated corpus for learning natural language inference](https://mlsanity.com/paper/1508.05326/) (2015)
- [Annotation Artifacts in Natural Language Inference Data](https://mlsanity.com/paper/1803.02324/) (2018)
- [e-SNLI: Natural Language Inference with Natural Language Explanations](https://mlsanity.com/paper/1812.01193/) (2018)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Hypothesis Only Baselines in Natural Language Inference](https://mlsanity.com/paper/1805.01042/) (2018)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [Breaking NLI Systems with Sentences that Require Simple Lexical Inferences](https://mlsanity.com/paper/1805.02266/) (2018)
- [The Fact Extraction and VERification (FEVER) Shared Task](https://mlsanity.com/paper/1811.10971/) (2018)
- [Performance Impact Caused by Hidden Bias of Training Data for Recognizing Textual Entailment](https://mlsanity.com/paper/1804.08117/) (2018)
- [PRover: Proof Generation for Interpretable Reasoning over Rules](https://mlsanity.com/paper/2010.02830/) (2020)
- [SemEval-2020 Task 4: Commonsense Validation and Explanation](https://mlsanity.com/paper/2007.00236/) (2020)
- [Do Neural Models Learn Systematicity of Monotonicity Inference in Natural Language?](https://mlsanity.com/paper/2004.14839/) (2020)
- [ConjNLI: Natural Language Inference Over Conjunctive Sentences](https://mlsanity.com/paper/2010.10418/) (2020)
- [LangPro: Natural Language Theorem Prover](https://mlsanity.com/paper/1708.09417/) (2017)

## Built on by (most cited first, 1 of 1)

- [Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs](https://mlsanity.com/paper/2609.32491/) (2026)

## Abstract (arXiv)

In this position paper, we propose a reasoning framework that can model the reasoning process underlying natural language inferences. The framework is based on the semantic tableau method, a well-studied proof system in formal logic. Like the semantic tableau, the framework is driven by refutation -- something is proved if and only if its counterexample was not refuted. Despite being rooted in formal logic, the framework shares similarities with the mental models, a theory on the psychology of reasoning. We will show how the reasoning framework can facilitate the collection of comprehensive and structured explanations for existing naturalistic inference problems. To make the suggestion more concrete, we propose a method of semi-automatically obtaining structured explanations from the formal proofs of a reliable and high-performing logic-based inference system. Taking advantage of the in-depth information available in the generated formal proofs, we show how it can be used to define natural language reasoning tasks with structured explanations. The proposed tasks can be ordered according to difficulty defined in terms of the granularity of explanations. We argue that the tasks that contain a natural sketch of the proofs will suffer from substantially fewer shortcomings than the existing explainable reasoning tasks (or datasets).