使用LLM改进NL到FOL翻译的策略：数据生成、增量微调与验证
Strategies for Improving NL-to-FOL Translation with LLMs: Data Generation, Incremental Fine-Tuning, and Verification
AI总结：
本文针对LLM在自然语言到一阶逻辑翻译中的错误，构建了ProofFOL数据集，并提出包含数据增强与验证的增量微调框架，使LLaMA-2和Mistral等小模型在ProofWriter和ProntoQA上达到SOTA。
摘要：
逻辑推理是自然语言处理中的一项基本任务，对大型语言模型（LLMs）提出了重大挑战。逻辑推理的固有特性使其非常适合一阶逻辑（FOL）等符号表示。符号逻辑推理的研究探索了使用最先进的LLM（即GPT-4）来生成自然语言（NL）语句的FOL翻译，但翻译中的错误通常不是研究重点。我们通过对LLM生成的FOL语句中的翻译错误进行分类来解决这一问题。为了在LLaMA-2 13B和Mistral 7B等较小语言模型上提高FOL翻译质量，我们使用GPT-4o创建了ProofFOL，这是ProofWriter数据集的一个高质量FOL标注子集。在此银标准数据上微调的模型，与LLaMA-2 70B等较大语言模型相比，取得了显著的性能提升。除了使用大量数据改进模型外，我们还解决了数据稀缺问题，并引入了一个包含数据增强和验证步骤的增量框架。在增强过程中，一对（前提，结论）基于谓词和FOL被拆分为多个新实例。此数据用于微调，并且在该模型上的推理生成的FOL比在原始数据上训练的模型错误更少。我们对翻译错误的调查促使生成了一个扰动数据集，用于训练一个验证器来纠正潜在的语法和语义FOL翻译错误。我们展示了一种有效的方法，以充分利用有限的现有人工标注数据集。我们的结果显示，在LLaMA-2和Mistral模型上使用ProofFOL，在ProofWriter和ProntoQA数据集上达到了最先进的性能。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
