文章总结与翻译
一、主要内容
本文针对大型语言模型（LLMs）在自然语言到形式逻辑翻译任务中存在的幻觉问题（生成错误输出），提出了一种名为Lang2Logic的新型框架。该框架的核心目标是将英文自然语言语句准确转换为合取范式（CNF），为可满足性求解（SAT）等逻辑推理任务提供机器可处理的逻辑表示，适用于软件系统中的自动推理、调试、循环不变量查找等场景。
Lang2Logic框架包含三个核心模块：
- 自然语言到逻辑表达式转换：利用ChatGPT o1-mini模型API，结合NLTK工具进行句子分词预处理，将输入文本转化为结构化逻辑表达式；
- 逻辑表达式到CNF转换：通过Lark解析器和预定义语法生成解析树，再借助Sympy库将其转化为CNF格式；
- CNF简化与幻觉消除：使用Sympy的逻辑简化方法去除冗余子句，并通过自定义上下文无关文法（CFG）、NLTK句法分析构建幻觉检测机制，结合反馈循环对模型进行微调，实现幻觉的识别与修正。
实验结果显示，该框架能将自然语言段落分解为独立句子并完成端到端的CNF转换，针对相同类型的幻觉输入，微调后的模型可实现100%的修正效果。
二、创新点
- 一体化逻辑转换框架：首次构建了从自然语言到CNF的完整流水线，整合了NLP工具、符号计算库和自定义语法，实现无人工干预的端到端转换，降低了SAT求解器在现实场景中的应
