# Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 13 of its 18 references that are in the map.
- First posted on arXiv 24 Sep 2024.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

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

- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [NeuroLogic A*esque Decoding: Constrained Text Generation with Lookahead Heuristics](https://mlsanity.com/paper/2112.08726/) (2021)
- [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)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [PiVe: Prompting with Iterative Verification Improving Graph-based Generative Capability of LLMs](https://mlsanity.com/paper/2305.12392/) (2023)
- [Are LLMs Rigorous Logical Reasoners? Empowering Natural Language Proof Generation by Stepwise Decoding with Contrastive Learning](https://mlsanity.com/paper/2311.06736/) (2023)

## Built on by (most cited first, 10 of 10)

- [VerifiAgent: a Unified Verification Agent in Language Model Reasoning](https://mlsanity.com/paper/2504.00406/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Do Large Language Models Excel in Complex Logical Reasoning with Formal Language?](https://mlsanity.com/paper/2505.16998/) (2025)
- [Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning](https://mlsanity.com/paper/2604.19459/) (2026)
- [Logical Reasoning with Outcome Reward Models for Test-Time Scaling](https://mlsanity.com/paper/2508.19903/) (2025)
- [Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs](https://mlsanity.com/paper/2509.22338/) (2025)
- [Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy](https://mlsanity.com/paper/2511.11816/) (2025)
- [LOGICPO: Efficient Translation of NL-based Logical Problems to FOL using LLMs and Preference Optimization](https://mlsanity.com/paper/2506.18383/) (2025)
- [Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling](https://mlsanity.com/paper/2606.02837/) (2026)
- [Natural Language to First-Order Logic LLM-based Autoformalization](https://mlsanity.com/paper/2610.12030/) (2026)

## Abstract (arXiv)

Logical reasoning is a fundamental task in natural language processing that presents significant challenges to Large Language Models (LLMs). The inherent characteristics of logical reasoning makes it well-suited for symbolic representations such as first-order logic (FOL). Research in symbolic logical reasoning explored FOL generation using state-of-the-art LLMs (i.e., GPT-4) to produce FOL translations of natural language (NL) statements, but errors in translation are usually not the focus. We address this by categorizing the translation errors in FOL statements generated by LLMs. To make progress towards improving the quality of FOL translations for smaller language models such as LLaMA-2 13B and Mistral 7B, we create ProofFOL, a high-quality FOL-annotated subset of ProofWriter dataset using GPT-4o. The models fine-tuned on this silver standard data achieve a significant gain in performance when compared to larger language models such as LLaMA-2 70B. In addition to improving the model using large data, we also tackle the issue of data scarcity and introduce an incremental framework encompassing of data augmentation and verification steps. In the augmentation process, a single pair of (premises, conclusion) is split into multiple new instances based on the predicates and FOLs. This data is used for fine-tuning, and the inference on this model generates FOLs with fewer errors over the model trained on the original data. Our investigation on the translation errors leads to generation of a perturbation dataset, which is used to train a verifier that corrects potential syntactic and semantic FOL translation errors. We demonstrate an efficient method for making the most of a limited existing human-annotated dataset. Our results show state-of-the-art performance for ProofWriter and ProntoQA datasets using ProofFOL on LLaMA-2 and Mistral models.