利用大语言模型能力实现自然语言到一阶逻辑翻译

将自然语言句子翻译为一阶逻辑（NL-FOL 翻译）是 NLP 与形式逻辑文献中的一个长期挑战。本文提出 LogicLLaMA，一个在单块 GPU 上使用 LoRA 微调用于 NL-FOL 翻译的 LLaMA-7B 模型。LogicLLaMA 能够直接将自然语言翻译为 FOL 规则，其性能优于 GPT-3.5。LogicLLaMA 还具备纠正 GPT-3.5 预测的 FOL 规则的能力，并能以极低的成本取得与 GPT-4 相近的性能。这一纠正能力通过一种新颖的监督微调（SFT）+ 基于人类反馈的强化学习（RLHF）框架实现：该框架先在合成扰动的 NL-FOL 对上训练以鼓励思维链推理，随后使用 FOL 验证器作为奖励模型在 GPT-3.5 输出上进行 RLHF 微调。为训练 LogicLLaMA，我们提出 MALLS（大语言 $\textbf{M}$odel gener$\textbf{A}$ted N$\textbf{L}$-FO$\textbf{L}$ pair$\textbf{S}$），一个从 GPT-4 收集的包含 34K 高质量且多样化的句子级 NL-FOL 对的数据集。该数据集通过实现一条提示 GPT-4 生成配对并动态调整提示以确保收集到具有不同复杂度下丰富多样语境的配对、并验证所生成 FOL 规则有效性的流水线创建。代码、权重与数据可在 $\href{https://github.com/gblackout/LogicLLaMA}{{\small \text{https://github.com/gblackout/LogicLLaMA}}}$ 获取。