用微调大模型减少逻辑翻译幻觉，提升代码验证准确性
Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic
- 结合自定义语法与符号计算，微调LLM进行自然语言到逻辑表达式转换
- 在实验中显著减少原模型的逻辑错误，生成可验证的合取范式（CNF）
- 适合需要高精度形式化验证的软件工程与自动化推理场景
近年来，自然语言处理（NLP）特别是大语言模型（LLMs）的发展推动了无需人工干预的自然语言到形式逻辑的自动翻译。这有助于实现自动化推理，支持软件系统的调试、循环不变量发现和规范符合性检查。然而，大模型产生的幻觉——即错误输出——在要求高精度的逻辑翻译任务中构成挑战。本文提出一种新框架：输入英文句子，将其转化为逻辑表达式，并进一步转为合取范式（CNF）以用于可满足性求解。该框架结合经典NLP技术、自定义语法、符号计算库以及微调后的语言模型，有效降低幻觉。初步实验表明，不同语法设置下训练的微调模型能够有意识地纠正原始模型产生的同类错误，从而提供可靠的CNF生成。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。