Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Lasha Abzianidze

TL;DR

This paper addresses explainable natural language inference (NLI) by bridging formal proof systems and NLP. It introduces a refutation-based framework based on the semantic tableau, where inferences are validated by counterexample search and accompanied by structured proofs. The authors argue that extracting explanations from these proofs enables reliable automatic evaluation and offers four new explainable NLI tasks with varying granularity. They leverage LangPro as a proof-generating engine and propose a proof bank to scale data collection beyond existing datasets, aiming to reduce reliance on unstructured free-text explanations. The work advances principled, verifiable reasoning traces that align with cognitive notions of rationality and has potential for more trustworthy NLI benchmarks.

Abstract

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).

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

TL;DR

This paper addresses explainable natural language inference (NLI) by bridging formal proof systems and NLP. It introduces a refutation-based framework based on the semantic tableau, where inferences are validated by counterexample search and accompanied by structured proofs. The authors argue that extracting explanations from these proofs enables reliable automatic evaluation and offers four new explainable NLI tasks with varying granularity. They leverage LangPro as a proof-generating engine and propose a proof bank to scale data collection beyond existing datasets, aiming to reduce reliance on unstructured free-text explanations. The work advances principled, verifiable reasoning traces that align with cognitive notions of rationality and has potential for more trustworthy NLI benchmarks.

Abstract

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).
Paper Structure (22 sections, 2 equations, 3 figures, 1 table)

This paper contains 22 sections, 2 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. State of the art in explainable natural language reasoning
  3. Free-text explanations in e-SNLI
  4. Word highlights as explanations in e-SNLI
  5. Fact-rule proofs
  6. Entailment Bank
  7. Chain-of-thought method
  8. Refutation-based reasoning framework
  9. Designing new explainable NLI tasks
  10. Natural language theorem prover
  11. From proofs to explainable NLI tasks
  12. Answering several concerns
  13. Is it feasible to get a substantial amount of proofs?
  14. Will not the proved NLI problems be homogeneous?
  15. But human reasoning is different from deductive reasoning
  16. ...and 7 more sections

Figures (3)

  • Figure 1: A tableau-based proof for the NLI problem in \ref{['ex:rte_problem']}. The nodes with green and red backgrounds are natural language representations and their role is to assist the reader in understanding the machine-readable representations (in blue font color), which are formatted in terms of character offsets. The green and red colors stand for the true and false signs, which are explicated in the machine-readable representation. Each branching is annotated with a rule application that is responsible for the expansion of the tree. Each rule application consists of a rule name and the ID(s) of entries to which the rule was applied. The tableau represents a proof for the entailment of \ref{['ex:rte_problem']} as both branches are closed due to inconsistencies in the branches, representing a failure to refute the entailment relation.
  • Figure 2: The tableau proves that "many birds hover high" contradicts "few birds fly" and vice versa.
  • Figure 3: The unlabeled proof represents the simplified version of the proof from \ref{['fig:tableau_proof']}. Note that all word forms in the nodes are identical to those in the premise and the hypothesis.