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

2024/04/18 by Abhinav Lalwani, Lalwani, Abhinav, Tasha Kim +9 · 14 voices · 9 citations
Computer Science · #Artificial intelligence #Computer science #Economics #Fallacy #Formal Methods in Verification #Fuzzy Logic and Control Systems #History #Linguistics #Logic, Reasoning, and Knowledge #Logical consequence #Natural (archaeology) #Natural language processing #Order (exchange) #Philosophy #cs.AI #cs.CL #cs.LG #cs.LO

paper · pdf · doi:10.48550/arxiv.2405.02318

published in arXiv (Cornell University) (Cornell University)

openalex publication_date 2024/04/18 · openalex created_date 2024/05/10 · openalex updated_date 2026/07/28

Abstract

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

Cited by

• Structured Decomposition for LLM Reasoning: Cross-Domain Validation and Semantic Web Integration
• Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy
• VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks
• Towards Verified Code Reasoning by LLMs
• Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs
• On Verifiable Legal Reasoning: A Multi-Agent Framework with Formalized Knowledge Representations
• Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
• Explainable Rule Application via Structured Prompting: A Neural-Symbolic Approach
• Logic Jailbreak: Efficiently Unlocking LLM Safety Restrictions Through Formal Logical Expression

Discussions

• Translating natural language to first-order logic for logical fallacy detection [hn, 258 points, 143 comments]
• "Translating natural language to first-order logic for logical fallacy detection" Turning everyday language into logical rules is harder than it sounds. Many think complex meanings can't be simply re [bsky, 2 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection #HackerNews https://arxiv.org/abs/2405.02318 [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection https://arxiv.org/abs/2405.02318 https://news.ycombinator.com/item?id=43257719 [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection https://arxiv.org/abs/2405.02318 [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection https://arxiv.org/abs/2405.02318 [comments] [129 points] [telegram] [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection https://arxiv.org/abs/2405.02318 (https://news.ycombinator.com/item?id=43257719) [bsky, 0 points, 0 comments]
• https://bsky.app/profile/news.ycombinator.com.web.brid.gy/post/3ljlcivghqx62 [bsky, 0 points, 0 comments]
• Translating natural language to first-order logic for logical fallacy detection https://arxiv.org/abs/2405.02318 (http://news.ycombinator.com/item?id=43257719) [bsky, 0 points, 0 comments]
• Translating natural language to first-order logic for logical fallacy detection https://arxiv.org/abs/2405.02318 (http://news.ycombinator.com/item?id=43257719) [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection (arxiv.org) Main Link | Discussion [bsky, 0 points, 0 comments]
• ⚡ Hackernews Top story: Translating Natural Language to First-Order Logic for Logical Fallacy Detection [bsky, 0 points, 0 comments]
• Translating Natural Language to First-Order Logic for Logical Fallacy Detection https://arxiv.org/abs/2405.02318 (https://news.ycombinator.com/item?id=43257719) [bsky, 0 points, 0 comments]

Related

• FOLIO: Natural Language Reasoning with First-Order Logic
• Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs
• Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification
• FOL-Traces: Verified First-Order Logic Reasoning Traces at Scale
• FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference