# Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 8 of its 35 references that are in the map.
- First posted on arXiv 2 Apr 2024.

## Placed in

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

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

- [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://mlsanity.com/paper/1907.11692/) (2019)
- [A Multitask, Multilingual, Multimodal Evaluation of ChatGPT on Reasoning, Hallucination, and Interactivity](https://mlsanity.com/paper/2302.04023/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Faithful Chain-of-Thought Reasoning](https://mlsanity.com/paper/2301.13379/) (2023)
- [Reasoning with Language Model Prompting: A Survey](https://mlsanity.com/paper/2212.09597/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [Faithful Reasoning Using Large Language Models](https://mlsanity.com/paper/2208.14271/) (2022)
- [A Survey on Theorem Provers in Formal Methods](https://mlsanity.com/paper/1912.03028/) (2019)

## Abstract (arXiv)

Large language models (LLMs) have achieved significant performance in various natural language reasoning tasks. However, they still struggle with performing first-order logic reasoning over formal logical theories expressed in natural language. This is because the previous LLMs-based reasoning systems have the theoretical incompleteness issue. As a result, it can only address a limited set of simple reasoning problems, which significantly decreases their generalization ability. To address this issue, we propose a novel framework, named Generalizable and Faithful Reasoner (GFaiR), which introduces the paradigm of resolution refutation. Resolution refutation has the capability to solve all first-order logic reasoning problems by extending reasoning rules and employing the principle of proof by contradiction, so our system's completeness can be improved by introducing resolution refutation. Experimental results demonstrate that our system outperforms previous works by achieving state-of-the-art performances in complex scenarios while maintaining performances in simple scenarios. Besides, we observe that GFaiR is faithful to its reasoning process.