Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic
作者: Muyu Pan, Dheeraj Kodakandla, Mahfuza Farooque
分类: cs.CL, cs.AI
发布日期: 2025-12-02
备注: IEEE ISNCC 2025
DOI: 10.1109/ISNCC66965.2025.11250432
💡 一句话要点
提出Lang2Logic框架，利用微调大语言模型减少逻辑翻译中的幻觉问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 逻辑翻译 大语言模型 幻觉减少 合取范式 自然语言处理 形式化验证 微调
📋 核心要点
- 现有大语言模型在逻辑翻译任务中容易产生幻觉，导致输出不准确，影响后续的自动推理和验证。
- 论文提出Lang2Logic框架，通过结合经典NLP技术和微调LLM，将自然语言转换为逻辑表达式和CNF，减少幻觉。
- 实验表明，微调模型能够纠正原始模型的幻觉，从而更可靠地生成CNF，提升逻辑翻译的准确性。
📝 摘要（中文）
本文提出了一种新颖的框架，旨在将自然语言语句自动翻译成形式逻辑，无需人工干预。该框架将英语句子作为输入，将其转换为逻辑表达式，然后翻译成合取范式（CNF）以进行可满足性求解。通过结合经典自然语言处理技术、自定义语法、符号计算库和微调的语言模型，该框架能够有效减少大语言模型（LLM）在逻辑翻译任务中产生的幻觉——即不正确的输出。初步实验表明，在不同语法设置下训练的微调模型能够有意识地纠正原始模型产生的同类型幻觉，从而提供可靠的CNF生成。
🔬 方法详解
问题定义：论文旨在解决自然语言到形式逻辑的自动翻译问题，特别是大语言模型在此过程中产生的幻觉问题。现有方法，尤其是直接使用未经特殊设计的LLM，在处理需要高精度的逻辑翻译任务时，容易产生不正确的输出，这严重影响了后续的自动推理、调试和验证等应用。
核心思路：论文的核心思路是结合经典NLP技术和微调的大语言模型，利用经典NLP技术（如自定义语法和符号计算库）来约束LLM的输出空间，减少其产生幻觉的可能性。通过微调LLM，使其能够更好地理解和生成符合逻辑规则的表达式。
技术框架：该框架包含以下主要阶段：1) 接收英文句子作为输入；2) 将其转换为逻辑表达式，这一步可能涉及到语法分析和语义理解；3) 将逻辑表达式翻译成合取范式（CNF）；4) 使用可满足性求解器对CNF进行求解。其中，微调的LLM主要负责逻辑表达式的生成和转换，而经典NLP技术则用于约束LLM的输出，并进行后续的CNF转换和求解。
关键创新：该论文的关键创新在于将经典NLP技术与微调的LLM相结合，用于减少逻辑翻译中的幻觉。与直接使用LLM进行翻译的方法相比，该方法能够更好地控制输出的质量，并利用经典NLP技术的优势来保证逻辑表达式的正确性。
关键设计：论文中一个关键的设计是针对不同语法设置对LLM进行微调。通过在特定语法规则下训练LLM，使其能够更好地理解和生成符合这些规则的逻辑表达式。此外，论文还可能涉及到损失函数的设计，例如，可以使用交叉熵损失函数来训练LLM，使其能够更准确地预测下一个逻辑符号。
🖼️ 关键图片
📊 实验亮点
实验结果表明，经过微调的大语言模型能够有效地减少逻辑翻译中的幻觉。具体来说，微调后的模型能够有意识地纠正原始模型产生的同类型错误，从而提高了CNF生成的可靠性。虽然论文中没有给出具体的性能数据，但强调了微调模型在纠正幻觉方面的显著效果。
🎯 应用场景
该研究成果可应用于软件验证、自动推理、智能合约等领域。通过将自然语言需求转化为形式逻辑，可以实现对软件系统行为的自动验证，提高软件质量。此外，该技术还可以用于智能合约的自动生成和验证，确保合约的正确性和安全性。未来，该技术有望在更多需要形式化验证的领域发挥重要作用。
📄 摘要（原文）
Recent advances in natural language processing (NLP), particularly large language models (LLMs), have motivated the automatic translation of natural language statements into formal logic without human intervention. This enables automated reasoning and facilitates debugging, finding loop invariants, and adhering to specifications in software systems. However, hallucinations-incorrect outputs generated by LLMs are challenging, particularly for logical translation tasks requiring precision. This work introduces a novel framework that inputs English sentences, converts them into logical expressions, and then translates them into Conjunctive Normal Form (CNF) for satisfiability solving. It employs classical NLP techniques with self-defined grammar, symbolic computation libraries, and a fine-tuned language model to reduce hallucinations. In the early experiments, we observed that the fine-tuned model, trained on different grammar settings, could intentionally correct the same types of hallucinations made by the original model. Thus, it provides reliable CNF generation.