Elamur Research⌕
☰
home / papers / 2024 / Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection

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

Paper · 2024 · Abhinav Lalwani, Tasha Kim, Lovish Chopra et al.

Summary

The paper addresses automatically translating ordinary-language arguments into First-Order Logic (FOL) so that symbolic tools can check whether they actually hold. The authors propose NL2FOL, a neurosymbolic pipeline in which few-shot prompted LLMs translate gradually. They first split an argument into claims and implications, then extract entities, and then use zero-shot Natural Language Inference (NLI) to find relations between entities, such as subset or equality. These relations guide quantifier choice and add implicit background knowledge. The negated formula is compiled into an SMT file and checked with the CVC solver. If the negation is satisfiable, the argument is invalid, and an LLM explains the counter-model in plain language. Logical fallacy detection is the test case. The system needs no fine-tuning or labelled training data. It reaches an F1 of 78% on LOGIC and 80% on LOGIC-CLIMATE. It also produces inspectable intermediate steps, which makes it a transparent alternative to purely neural fallacy classifiers.

Key points

  • The architecture has three modules. Module A converts text to FOL and adds background knowledge. Module B builds an SMT file with typed sorts. Module C runs CVC and interprets any counterexample.
  • With GPT-4o inside NL2FOL, the SMT-based decision gives F1 0.78 on LOGIC and 0.80 on LOGIC-CLIMATE. Asking GPT-4o directly for the classification gives 0.66 and 0.73.
  • On the LOGIC-CLIMATE challenge set, the authors report a 22% improvement over existing models.
  • The most frequent error source is missing or wrongly added background knowledge. Other errors come from the NLI step only comparing two properties at a time and from imprecise LLM translations.
  • The stated limitations are short premises only, no testing beyond English or beyond FOL, and high compute and API costs. Code is available at github.com/lovishchopra/NL2FOL.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States434 works · 314,419 citations🎓ETH ZurichZurich · Switzerland72 works · 5,176 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 works

Cite

Cite as Abhinav Lalwani, Tasha Kim, Lovish Chopra, Christopher Hahn, Zhijing Jin and Mrinmaya Sachan. 2024. Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection. arXiv:2405.02318.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2405.02318 · arXiv 2405.02318

@misc{lalwani2024autoformalizing,
  title = {{Autoformalizing Natural Language to First-Order Logic: A Case Study in Logical Fallacy Detection}},
  author = {Abhinav Lalwani, Tasha Kim, Lovish Chopra, Christopher Hahn, Zhijing Jin and Mrinmaya Sachan},
  year = {2024},
  doi = {10.48550/arxiv.2405.02318},
  eprint = {2405.02318},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2405.02318}
}

References

42 references, 18 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Meta AI. 2024a. Llama 3.2-11b model card. Accessed: 2025-02-15. find
  2. Mistral AI. 2024b. Ministral-8b-instruct-2410 model card. Accessed: 2025-02-15. find
  3. Tariq Alhindi, Tuhin Chakrabarty, Elena Musi, and Smaranda Muresan. 2022. Multitask instruction-based prompting for fallacy recognition. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pages 8172–8187, Abu Dhabi, United Arab Emirates. Association for Comput… find
  4. Rami Aly, Marek Strong, and Andreas Vlachos. 2023. QA-natver: Question answering for natural logic-based fact verification. In The 2023 Conference on Empirical Methods in Natural Language Processing. find
  5. Gabor Angeli and Christopher D Manning. 2014. Naturalli: Natural logic inference for common sense reasoning. In Proceedings of the 2014 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 534–545.
  6. Bing Bai, Jian Liang, Guanhua Zhang, Hao Li, Kun Bai, and Fei Wang. 2020. Why attentions may not be interpretable? Proceedings of the 27th ACM SIGKDD Conference on Knowledge Discovery & Data Mining. find
  7. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. Cvc4. In Computer Aided Verification, pages 171–177, Berlin, Heidelberg. Springer Berlin Heidelberg. find
  8. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2009. Satisfiability modulo theories. Communications of the ACM, 52(9):69–77. find
  9. Iz Beltagy, Stephen Roller, Pengxiang Cheng, Katrin Erk, and Raymond J. Mooney. 2016. Representing meaning with a combination of logical and distributional models. Computational Linguistics, 42(4):763–808.
  10. Samuel R. Bowman, Gabor Angeli, Christopher Potts, and Christopher D. Manning. 2015. A large annotated corpus for learning natural language inference. In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 632–642, Lisbon, Portugal. Association for Computati…
  11. Tom B Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chri… — Language Models are Few-Shot Learners
  12. Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang. 2023. Sparks of artificial general intelligence: Early experiments with gpt-4.
  13. Zixiang Chen, Yihe Deng, Huizhuo Yuan, Kaixuan Ji, and Quanquan Gu. 2024. Self-play fine-tuning converts weak language models to strong language models. find
  14. Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In Computer Aided Verification. find
  15. CAV 2023. Lecture Notes in Computer Science, volume 13965, Cham. Springer. find
  16. Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie, Hannah Smith, Leighanna Pipatanangkura, and Peter Clark. 2021. Explaining answers with entailment trees. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 7358–7370, Online and Punta Cana, Domin…
  17. Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, page 337–340, Berlin, Heidelberg. Springer-Verlag. find
  18. Francesco Fuggitti and Tathagata Chakraborti. 2023. Nl2ltl - a python package for converting natural language (nl) instructions to linear temporal logic (ltl) formulas. In AAAI Conference on Artificial Intelligence. find
  19. Gaël Gendron, Qiming Bao, Michael Witbrock, and Gillian Dobbie. 2024. Large language models are not strong abstract reasoners.
  20. Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, Amy Yang, Angela Fan, Anirudh Goyal, Anthony Hartshorn, Aobo Yang, Archi Mitra, Archie Sravankumar, Artem Korenev, Arthur Hinsvark, Arun Rao,… — The Llama 3 Herd of Models
  21. Ivan Habernal, Henning Wachsmuth, Iryna Gurevych, and Benno Kiesel. 2018a. "dummy, grandpa, do you know anything?": Identifying and characterizing ad hominem fallacies in the wild. In Proceedings of the 12th International AAAI Conference on Web and Social Media (ICWSM), pages 206–215. find
  22. Ivan Habernal, Henning Wachsmuth, Iryna Gurevych, and Benno Stein. 2018b. Before name-calling: Dynamics and triggers of ad hominem fallacies in web argumentation. In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Tech…
  23. Christopher Hahn, Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. 2022. Formal specifications from natural language. find
  24. Patrick M. Haluptzok, Matthew Bowers, and Adam Tauman Kalai. 2022. Language modexrls can teach themselves to program better. ArXiv, abs/2207.14502. find
  25. Zhijing Jin, Abhinav Lalwani, Tejas Vaidhya, Xiaoyu Shen, Yiwen Ding, Zhiheng Lyu, Mrinmaya Sachan, Rada Mihalcea, and Bernhard Schoelkopf. 2022. Logical fallacy detection. In Findings of the Association for Computational Linguistics: EMNLP 2022, pages 7180– 7198, Abu Dhabi, United Arab Emirates. As…
  26. Mike Lewis, Yinhan Liu, Naman Goyal, Marjan Ghazvininejad, Abdelrahman Mohamed, Omer Levy, Veselin Stoyanov, and Luke Zettlemoyer. 2020. BART: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension. In Proceedings of the 58th Annual Meeting of the…
  27. Jason Xinyu Liu, Ziyi Yang, Benjamin Schornstein, Sam Liang, Ifrah Idrees, Stefanie Tellex, and Ankit Shah. 2022. Lang2LTL: Translating natural language commands to temporal specification with large language models. In CoRL Workshop on Language and Robot Learning. find
  28. B. MacCartney and C. D. Manning. 2014. Natural logic and natural language inference. In H. Bunt, J. Bos, and S. Pulman, editors, Computing Meaning: Volume 4, pages 129–147. Springer Netherlands, Dordrecht. find
  29. Callistus Ireneous Nakpih and Simone Santini. 2020. Automated discovery of logical fallacies in legal argumentation. International Journal of Artificial Intelligence & Applications. find
  30. Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natural Lan…
  31. OpenAI. 2024. Gpt-4o mini: Advancing cost-efficient intelligence. Accessed: 2025-02-15. find
  32. OpenAI, Aaron Hurst, Adam Lerer, Adam P. Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, Aleksander M adry, Alex Baker-Whitcomb, Alex Beutel, Alex Borzunov, Alex Carney, Alex Chow, Alex Kirillov, Alex Nichol, Alex Paino, Alex Renzin, Alex Ta… — GPT-4o System Card
  33. OpenAI, Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, Alex Iftimie, Alex Karpenko, Alex Tachard Passos, Alexander Neitz, Alexander Prokofiev, Alexander Wei, Allison Tam, Ally Bennett, Ananya Kumar, Andre Sar… — OpenAI o1 System Card
  34. Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore. Association for Computational Lingui…
  35. William C Purdy. 1991. A logic for natural language. Notre Dame Journal of Formal Logic, 32(3):409–425. find
  36. Hrituraj Singh, Milan Aggarwal, and Balaji Krishnamurthy. 2020. Exploring neural models for parsing natural language into first-order logic. ArXiv, abs/2002.06544. — [arXiv:2002.06544](https://arxiv.org/abs/2002.06544) find
  37. Zhivar Sourati, Vishnu Priya Prasanna Venkatesh, Darshan Deshpande, Himanshu Rawlani, Filip Ilievski, Hông-Ân Sandlin, and Alain Mermoud. 2022. Robust and explainable identification of logical fallacies in natural language arguments. Knowledge Based Systems, 266:110418. find
  38. Christian Stab and Iryna Gurevych. 2017. Recognizing insufficiently supported arguments in argumentative essays. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers, pages 980–990, Valencia, Spain. Association for Comp… find
  39. Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller,… — Llama 2: Open Foundation and Fine-Tuned Chat Models
  40. Jason Wei, Xuezhi Wang, Dale Schuurmans, et al. 2022. Chain of thought prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems.
  41. Adina Williams, Nikita Nangia, and Samuel Bowman. 2018. A broad-coverage challenge corpus for sentence understanding through inference. In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Pa…
  42. Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2024. Harnessing the power of large language models for natural language to first-order logic translation. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), page… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lalwani-2024-autoformalizing-natural-language-first-order/