Elamur Research⌕
☰
home / papers / 2026 / NL2Logic: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models

NL2Logic: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models

Paper · 2026 · Rizky Ramadhana Putra, Raihan Sultan Pasha Basuki, Yutong Cheng et al.

Summary

Converting natural-language premises into first-order logic (FOL) lets automated solvers check claims transparently, which matters in fields like law and policy. Current LLM-based translators, such as GCD and CODE4LOGIC, still produce formulas that fail to execute or misrepresent the source meaning. One reason is that they map whole passages to logic in a single step.

NL2Logic splits the task in two. First, the SaT model segments the text into sentences. An LLM-driven parser then works recursively, clause by clause. It picks among specialised sub-parsers (atomic, quantified, logical) and emits schema-constrained JSON that builds a FOL abstract syntax tree (FOLAST). Next, a deterministic two-pass generator compiles this tree into solver code for Z3 or SMT-LIB. It first registers constants, variables and relation signatures, then assembles scoped expressions.

The authors tested open models from 0.5B to 27B parameters on FOLIO, LogicNLI and ProofWriter. The approach reaches about 99% syntactic validity and roughly 30% higher semantic accuracy than GCD. Because the intermediate layer does not depend on any particular engine, NL2Logic can serve as a drop-in module for neuro-symbolic pipelines.

Key points

  • Results: About 99% syntactic accuracy and an average semantic gain of roughly 30% over the strongest baseline (GCD), measured on FOLIO, LogicNLI and ProofWriter with the Z3 engine.
  • Logic-LM integration: Swapping Logic-LM's few-shot FOL translation for NL2Logic raised executable rates from a range of 0.01–0.94 to 0.99 for every model. Downstream accuracy improved by about 31% on average.
  • Biggest gains on small models (ProofWriter): gemma-2-2b rose from 0.01 to 0.58, llama-3.2-3b from 0.03 to 0.68, and qwen-2.5-7b from 0.08 to 0.90. Model counts differ within the paper: 12 in the main text, 13 in the Logic-LM tables.
  • Limitations: Sentences are translated independently, so cross-sentence co-reference is not resolved. For example, "father" and "parent" become unrelated predicates. The method also requires structured JSON output support, such as vLLM or OpenAI; llama.cpp needs lm-format-enforcer.
  • Code: Released at github.com/peng-gao-lab/nl2logic.

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

🎓Virginia TechBlacksburg · United States36 works · 43,036 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 Rizky Ramadhana Putra, Raihan Sultan Pasha Basuki, Yutong Cheng and Peng Gao. 2026. NL2Logic: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models. Findings of the Association for Computational Linguistics: EACL 2026.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.findings-eacl.317

@inproceedings{putra2026nl2logic,
  title = {{NL2Logic: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models}},
  author = {Rizky Ramadhana Putra, Raihan Sultan Pasha Basuki, Yutong Cheng and Peng Gao},
  booktitle = {Findings of the Association for Computational Linguistics: EACL 2026},
  year = {2026},
  doi = {10.18653/v1/2026.findings-eacl.317},
  url = {https://doi.org/10.18653/v1/2026.findings-eacl.317}
}

References

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

  1. Lasha Abzianidze. 2017. Langpro: Natural language theorem prover. arXiv preprint arXiv:1708.09417. find
  2. V Aho Alfred, S Lam Monica, and D Ullman Jeffrey. 2007. Compilers principles, techniques & tools. pearson Education. find
  3. Dave Barker-Plummer, Richard Cox, and Robert Dale. 2009. Dimensions of difficulty in translating natural language into first order logic. International Working Group on Educational Data Mining. find
  4. Clark Barrett, Aaron Stump, Cesare Tinelli, and 1 others. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14. find
  5. Stefan Behnel, Robert Bradshaw, Craig Citro, Lisandro Dalcin, Dag Sverre Seljebotn, and Kurt Smith. 2010. Cython: The best of both worlds. Computing in Science & Engineering, 13(2):31–39. find
  6. Johan Bos and Katja Markert. 2005. Recognising textual entailment with logical inference. In Proceedings of Human Language Technology Conference and Conference on Empirical Methods in Natural Language Processing, pages 628–635.
  7. Samuel R. Bowman, Christopher Potts, and Christopher D. Manning. 2015. Recursive neural networks can learn logical semantics. In Proceedings of the 3rd Workshop on Continuous Vector Space Models and their Compositionality, pages 12–21, Beijing, China. Association for Computational Linguistics. find
  8. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D 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, and… find
  9. Ruisheng Cao, Su Zhu, Chen Liu, Jieyu Li, and Kai Yu. 2019. Semantic parsing with dual learning. arXiv preprint arXiv:1907.05343. find
  10. Antonia Creswell, Murray Shanahan, and Irina Higgins. 2022. Selection-inference: Exploiting large language models for interpretable logical reasoning. Preprint, arXiv:2205.09712. find
  11. 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
  12. Herbert B Enderton. 2001. A mathematical introduction to logic. Elsevier. find
  13. Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. 2018. Can neural networks understand logical entailment? In International Conference on Learning Representations. find
  14. Markus Frohmann, Igor Sterner, Ivan Vulić, Benjamin Minixhofer, and Markus Schedl. 2024. Segment any text: A universal approach for robust, efficient and adaptable sentence segmentation. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 11908–11941, Mi… find
  15. Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, and 1 others. 2024. Folio: Natural language reasoning with first-order logic. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processi…
  16. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. Large language models are zero-shot reasoners. Advances in neural information processing systems, 35:22199– 22213.
  17. Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles.
  18. Junnan Liu. 2025. Few-shot natural language to first-order logic translation via code generation. In Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pages 10939–10960, Alb… find
  19. Xuantao Lu, Jingping Liu, Zhouhong Gu, Hanwen Tong, Chenhao Xie, Junyang Huang, Yanghua Xiao, and Wenguang Wang. 2022. Parsing natural language into propositional and first-order logic with dual reinforcement learning. In Proceedings of the 29th International Conference on Computational Linguistics,… find
  20. Mitchell Philip Marcus. 1978. A theory of syntactic recognition for natural language. Ph.D. thesis, Massachusetts Institute of Technology. find
  21. W. McCune. 2005–2010. Prover9 and mace4. http://www.cs.unm.edu/~mccune/prover9/. ↗
  22. Benjamin Minixhofer, Jonas Pfeiffer, and Ivan Vulić. 2023. Where’s the point? self-supervised multilingual punctuation-agnostic sentence segmentation. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 7215–7235, Toronto, Canada… find
  23. Terufumi Morishita, Gaku Morio, Atsuki Yamaguchi, and Yasuhiro Sogawa. 2024. Enhancing reasoning capabilities of llms via principled synthetic logic corpus. Advances in Neural Information Processing Systems, 37:73572–73604. find
  24. Nikita Kitaev, Steven Cao, and Dan Klein. 2019. Multilingual constituency parsing with self-attention and pre-training. In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics, pages 3499–3505, Florence, Italy. Association for Computational Linguistics.
  25. 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…
  26. Nikita Kitaev and Dan Klein. 2018. Constituency parsing with a self-attentive encoder. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 2676–2686.
  27. 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…
  28. Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA. As…
  29. Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2025. Faithful and robust LLM-driven theorem proving for NLI explanations. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 17734–17755, Vienna, Austria. Associati… find
  30. Federico Raspanti, Tanir Ozcelebi, and Mike Holen-derski. 2025. Grammar-constrained decoding makes large language models better logical parsers. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 6: Industry Track), pages 485–499. find
  31. William A Woods. 1970. Transition network grammars for natural language analysis. Communications of the ACM, 13(10):591–606. find
  32. Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. 2024. Faithful logical reasoning via symbolic chain-of-thought. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 13326–13365, Bangkok, Thailand. Associat…
  33. 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
  34. Luke S Zettlemoyer and Michael Collins. 2012. Learning to map sentences to logical form: Structured classification with probabilistic categorial grammars. arXiv preprint arXiv:1207.1420.
  35. Tim Rocktaschel, Edward Grefenstette, Karl Moritz Hermann, Tomas Kocisky, and Phil Blunsom. 2016. Reasoning about entailment with neural attention. In International Conference on Learning Representations (ICLR).
  36. Soumya Sanyal, Harman Singh, and Xiang Ren. 2022. FaiRR: Faithful and robust deductive reasoning over natural language. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1075–1093, Dublin, Ireland. Association for Computational… find
  37. Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634, Online. Association for Computational Linguistics.
  38. Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. 2021. Diagnosing the first-order logical reasoning ability through logicnli. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 3738–3747.
  39. Bailin Wang, Zi Wang, Xuezhi Wang, Yuan Cao, Rif A Saurous, and Yoon Kim. 2023. Grammar prompting for domain-specific language generation with large language models. Advances in Neural Information Processing Systems, 36:65030–65055. find
  40. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, and 1 others. 2022. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824– 24837.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/putra-2026-nl2logic-ast-guided-translation-natural/