Abstract
Translating natural language into formal language such as First-Order Logic(FOL) is a foundational challenge in NLP with wide-ranging applications inautomated reasoning, misinformation tracking, and knowledge validation. In thispaper, we introduce Natural Language to First-Order Logic (NL2FOL), a frameworkto autoformalize natural language to FOL step by step using Large LanguageModels (LLMs). Our approach addresses key challenges in this translationprocess, including the integration of implicit background knowledge. Byleveraging structured representations generated by NL2FOL, we useSatisfiability Modulo Theory (SMT) solvers to reason about the logical validityof natural language statements. We present logical fallacy detection as a casestudy to evaluate the efficacy of NL2FOL. Being neurosymbolic, our approachalso provides interpretable insights into the reasoning process anddemonstrates robustness without requiring model fine-tuning or labeled trainingdata. Our framework achieves strong performance on multiple datasets. On theLOGIC dataset, NL2FOL achieves an F1-score of 78%, while generalizingeffectively to the LOGICCLIMATE dataset with an F1-score of 80%.