Formal Proofs as Structured Explanations: Proposing Several Tasks on Explainable Natural Language Inference
In this position paper, we propose a way of exploiting formal proofs to put forward several explainable natural language inference (NLI) tasks. The formal proofs will be produced by a reliable and high-performing logic-based NLI system. Taking advantage of the in-depth information available in the generated formal proofs, we show how it can be used to define NLI 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 will suffer with substantially fewer shortcomings than the existing explainable NLI tasks (or datasets).
Code (0)
등록된 구현이 없습니다.
Tasks
Natural Language InferencePositionSimilar Papers 제목 키워드 기반
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few exp…
Automated Theorem ProvingLanguage ModelingLanguage ModellingMathematical ProofsFrom Scientific Texts to Verifiable Code: Automating the Process with Transformers
Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying…
VEL: A Formally Verified Reasoner for OWL2 EL Profile
Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of…
Knowledge GraphsLearning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries
Large language models (LLMs) have recently demonstrated impressive performance on complex, multi-step reasoning tasks, especially when post-trained with outcome-rewarded reinforcement learning Guo et al. 2025. However, i…
Reinforcement LearningMathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
Formalizing mathematical proofs using computerized verification languages like Lean 4 has the potential to significantly impact the field of mathematics, it offers prominent capabilities for advancing mathematical reason…
Abstract AlgebraAutomated Theorem ProvingMathMathematical Proofs+1