论文
NL2LOGIC：用大语言模型实现 AST 引导的自然语言到一阶逻辑翻译
NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models
摘要
自动推理在法律与治理等领域至关重要，这些领域对照文档中的事实核验主张既要求准确性又要求可解释性。近来工作采用结构化推理流水线，把自然语言翻译为一阶逻辑并将推理委托给自动求解器。随着大语言模型的兴起，GCD 与 CODE4LOGIC 等方法利用其推理与代码生成能力改进逻辑解析。然而，这些方法存在语法控制脆弱的问题——全局语法约束执行不力——以及语义忠实度低的问题——子句级语义理解不足。我们提出 NL2LOGIC，一个引入抽象语法树作为中间表示的一阶逻辑翻译框架。NL2LOGIC 结合递归的基于大语言模型的语义解析器与 AST 引导的生成器，后者确定性地产出求解器可执行的逻辑代码。在 FOLIO、LogicNLI 与 ProofWriter 基准上的实验表明，NL2LOGIC 达到99%的语法准确率，语义正确性较最先进基线最多提升30%。此外，把 NL2LOGIC 集成进 Logic-LM 后可获得近乎完美的可执行性，下游推理准确率较 Logic-LM 原有的少样本无约束翻译模块提升31%。