# Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation

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

## Key facts

- Cited by 59 papers in the map (data through 14 Oct 2026).
- Placed in Process reward models for reasoning, one of 10 directions in LLM alignment / RLHF / preference optimisation.
- Builds on 22 of its 33 references that are in the map.
- First posted on arXiv 24 May 2023.

## Placed in

- LLM alignment / RLHF / preference optimisation / [Process reward models for reasoning](https://mlsanity.com/alignment/process-reward-models-for-reasoning/)

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [ReClor: A Reading Comprehension Dataset Requiring Logical Reasoning](https://mlsanity.com/paper/2002.04326/) (2020)
- [Retrieve, Program, Repeat: Complex Knowledge Base Question Answering via Alternate Meta-learning](https://mlsanity.com/paper/2010.15875/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [NeuroLogic Decoding: (Un)supervised Neural Text Generation with Predicate Logic Constraints](https://mlsanity.com/paper/2010.12884/) (2020)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Improving Coherence and Consistency in Neural Sequence Models with Dual-System, Neuro-Symbolic Reasoning](https://mlsanity.com/paper/2107.02794/) (2021)
- [Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text](https://mlsanity.com/paper/2105.03659/) (2021)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Semantic Parsing with Dual Learning](https://mlsanity.com/paper/1907.05343/) (2019)
- [Exploring Neural Models for Parsing Natural Language into First-Order Logic](https://mlsanity.com/paper/2002.06544/) (2020)
- [LangPro: Natural Language Theorem Prover](https://mlsanity.com/paper/1708.09417/) (2017)

## Built on by (most cited first, 30 of 59)

- [Large Language Models Can Learn Temporal Reasoning](https://mlsanity.com/paper/2401.06853/) (2024)
- [A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languages](https://mlsanity.com/paper/2410.03981/) (2024)
- [Symbol-LLM: Towards Foundational Symbol-centric Interface For Large Language Models](https://mlsanity.com/paper/2311.09278/) (2023)
- [DELTA: Decomposed Efficient Long-Term Robot Task Planning using Large Language Models](https://mlsanity.com/paper/2404.03275/) (2024)
- [Graph Machine Learning in the Era of Large Language Models (LLMs)](https://mlsanity.com/paper/2404.14928/) (2024)
- [Semantic-Aware Logical Reasoning via a Semiotic Framework](https://mlsanity.com/paper/2509.24765/) (2025)
- [Logical Phase Transitions: Understanding Collapse in LLM Logical Reasoning](https://mlsanity.com/paper/2601.02902/) (2026)
- [MedHalu: Hallucinations in Responses to Healthcare Queries by Large Language Models](https://mlsanity.com/paper/2409.19492/) (2024)
- [Frontier LLMs Still Struggle with Simple Reasoning Tasks](https://mlsanity.com/paper/2507.07313/) (2025)
- [Ontology engineering with Large Language Models](https://mlsanity.com/paper/2307.16699/) (2023)
- [Dissecting Logical Reasoning in LLMs: A Fine-Grained Evaluation and Supervision Study](https://mlsanity.com/paper/2506.04810/) (2025)
- [Logic Jailbreak: Efficiently Unlocking LLM Safety Restrictions Through Formal Logical Expression](https://mlsanity.com/paper/2505.13527/) (2025)
- [ToolGate: Contract-Grounded and Verified Tool Execution for LLMs](https://mlsanity.com/paper/2601.04688/) (2026)
- [Can LLMs Reason in the Wild with Programs?](https://mlsanity.com/paper/2406.13764/) (2024)
- [Beyond Math: Stories as a Testbed for Memorization-Constrained Reasoning in LLMs](https://mlsanity.com/paper/2412.14368/) (2024)
- [Synergistic Integration of Large Language Models and Cognitive Architectures for Robust AI: An Exploratory Analysis](https://mlsanity.com/paper/2308.09830/) (2023)
- [Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification](https://mlsanity.com/paper/2409.16461/) (2024)
- [EventGround: Narrative Reasoning by Grounding to Eventuality-centric Knowledge Graphs](https://mlsanity.com/paper/2404.00209/) (2024)
- [A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters](https://mlsanity.com/paper/2406.00284/) (2024)
- [Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition](https://mlsanity.com/paper/2510.06774/) (2025)
- [Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving](https://mlsanity.com/paper/2512.23511/) (2025)
- [PathWise: Planning through World Model for Automated Heuristic Design via Self-Evolving LLMs](https://mlsanity.com/paper/2601.20539/) (2026)
- [Entailment-Preserving First-order Logic Representations in Natural Language Entailment](https://mlsanity.com/paper/2502.16757/) (2025)
- [NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models](https://mlsanity.com/paper/2602.13237/) (2026)
- [Speak It Out: Solving Symbol-Related Problems with Symbol-to-Language Conversion for Language Models](https://mlsanity.com/paper/2401.11725/) (2024)
- [Can Large Language Models Understand DL-Lite Ontologies? An Empirical Study](https://mlsanity.com/paper/2406.17532/) (2024)
- [Assessing the Sensitivity and Alignment of FOL Closeness Metrics](https://mlsanity.com/paper/2501.08613/) (2025)
- [Do Large Language Models Excel in Complex Logical Reasoning with Formal Language?](https://mlsanity.com/paper/2505.16998/) (2025)
- [Graph Generation Powered with LLMs for Boosting Multivariate Time-Series Representation Learning](https://mlsanity.com/paper/2403.03645/) (2024)
- [forallutoexistsval: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks](https://mlsanity.com/paper/2403.18327/) (2024)

## Abstract (arXiv)

Translating natural language sentences to first-order logic (NL-FOL translation) is a longstanding challenge in the NLP and formal logic literature. This paper introduces LogicLLaMA, a LLaMA-7B model fine-tuned for NL-FOL translation using LoRA on a single GPU. LogicLLaMA is capable of directly translating natural language into FOL rules, which outperforms GPT-3.5. LogicLLaMA is also equipped to correct FOL rules predicted by GPT-3.5, and can achieve similar performance as GPT-4 with a fraction of the cost. This correction ability was achieved by a novel supervised fine-tuning (SFT) + reinforcement learning with human feedback (RLHF) framework, which initially trains on synthetically perturbed NL-FOL pairs to encourage chain-of-thought reasoning and then fine-tunes with RLHF on GPT-3.5 outputs using a FOL verifier as the reward model. To train LogicLLaMA, we present MALLS (large language Model generAted NL-FOL pairS), a dataset of 34K high-quality and diverse sentence-level NL-FOL pairs collected from GPT-4. The dataset was created by implementing a pipeline that prompts GPT-4 for pairs, and dynamically adjusts the prompts to ensure the collection of pairs with rich and diverse contexts at different levels of complexity, and verifies the validity of the generated FOL rules. Codes, weights, and data are available at hrefhttps://github.com/gblackout/LogicLLaMAsmall https://github.com/gblackout/LogicLLaMA.