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

TL;DR

The 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, and an efficient method for making the most of a limited existing human-annotated dataset.

Abstract

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.

Figures (9)

• Figure 1: The overall flow of the incremental generation and verification at inference time. Here $\text{P}_i$s and $\text{C}$ denote Premises and Conclusion. For predicate and FOL generation, the output is run through the corresponding verifier.
• Figure 2: Error distribution of LLaMA-2 70B (top) and LLaMA-2 13B (bottom) post fine-tuning on ProofFOL.
• Figure 3: Overview of the Data Generation Pipeline and Key Statistics
• Figure 4: Few shot example with instruction for Data Generation process
• Figure 5: Standard Generation Few-shot examples for FOLIO: For brevity, we highlighted the format and the instructions and minimized the content in the few-shot examples.