# Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection

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

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 12 references that are in the map.
- First posted on arXiv 18 Apr 2024.

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

- [Self-Play Fine-Tuning Converts Weak Language Models to Strong Language Models](https://mlsanity.com/paper/2401.01335/) (2024)
- [Why Attentions May Not Be Interpretable?](https://mlsanity.com/paper/2006.05656/) (2020)
- [Exploring Neural Models for Parsing Natural Language into First-Order Logic](https://mlsanity.com/paper/2002.06544/) (2020)
- [Representing Meaning with a Combination of Logical and Distributional Models](https://mlsanity.com/paper/1505.06816/) (2015)

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

- [On Verifiable Legal Reasoning: A Multi-Agent Framework with Formalized Knowledge Representations](https://mlsanity.com/paper/2509.00710/) (2025)
- [Explainable Rule Application via Structured Prompting: A Neural-Symbolic Approach](https://mlsanity.com/paper/2506.16335/) (2025)
- [Are LLMs Good Zero-Shot Fallacy Classifiers?](https://mlsanity.com/paper/2410.15050/) (2024)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving](https://mlsanity.com/paper/2512.23511/) (2025)
- [Towards Verified Code Reasoning by LLMs](https://mlsanity.com/paper/2509.26546/) (2025)
- [Understanding Enthymemes in Argument Maps: Bridging Argument Mining and Logic-based Argumentation](https://mlsanity.com/paper/2408.08648/) (2024)
- [Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy](https://mlsanity.com/paper/2511.11816/) (2025)
- [An Agentic Framework for Neuro-Symbolic Programming](https://mlsanity.com/paper/2601.00743/) (2026)
- [Structured Decomposition for LLM Reasoning: Cross-Domain Validation and Semantic Web Integration](https://mlsanity.com/paper/2601.01609/) (2026)
- [Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning](https://mlsanity.com/paper/2603.17233/) (2026)
- [Evidence-Guided Schema Normalization for Temporal Tabular Reasoning](https://mlsanity.com/paper/2512.00329/) (2025)
- [From Passive Reuse to Active Reasoning: Grounding Large Language Models for Neuro-Symbolic Experience Replay](https://mlsanity.com/paper/2605.09419/) (2026)
- [FOL2NS: Generating Natural Sentences from First-Order Logic](https://mlsanity.com/paper/2605.18155/) (2026)
- [ForEx: A Formal Verification Framework for Explainable Reasoning in Logical Fallacy Detection and Annotation](https://mlsanity.com/paper/2606.21867/) (2026)
- [SoK: Formal Methods for Fact-Checking and Information Integrity](https://mlsanity.com/paper/2609.23239/) (2026)
- [Natural Language to First-Order Logic LLM-based Autoformalization](https://mlsanity.com/paper/2610.12030/) (2026)

## Abstract (arXiv)

Translating natural language into formal language such as First-Order Logic (FOL) is a foundational challenge in NLP with wide-ranging applications in automated reasoning, misinformation tracking, and knowledge validation. In this paper, we introduce Natural Language to First-Order Logic (NL2FOL), a framework to autoformalize natural language to FOL step by step using Large Language Models (LLMs). Our approach addresses key challenges in this translation process, including the integration of implicit background knowledge. By leveraging structured representations generated by NL2FOL, we use Satisfiability Modulo Theory (SMT) solvers to reason about the logical validity of natural language statements. We present logical fallacy detection as a case study to evaluate the efficacy of NL2FOL. Being neurosymbolic, our approach also provides interpretable insights into the reasoning process and demonstrates robustness without requiring model fine-tuning or labeled training data. Our framework achieves strong performance on multiple datasets. On the LOGIC dataset, NL2FOL achieves an F1-score of 78%, while generalizing effectively to the LOGICCLIMATE dataset with an F1-score of 80%.