分解与形式化：可递归验证的自然语言推理
计算与语言
2026-01-28 v1
摘要
近期研究表明，在神经符号流水线中将大型语言模型与定理证明器集成，有助于自然语言推理中的蕴涵验证和基于证明的解释精炼。然而，将这种精炼扩展到自然场景下的NLI仍然困难：长句、句法丰富的输入以及深层的多步论证放大了自动形式化错误，其中单个局部不匹配就可能导致证明无效。此外，由于难以从证明器诊断信息中定位有问题的片段或步骤，当前方法通常通过代价高昂的全局重新生成来处理失败。针对这些问题，我们提出了一个分解与形式化框架，该框架：(i) 将前提-假设对分解为原子步骤的蕴涵树，(ii) 自底向上验证该树以将失败隔离到特定节点，以及(iii) 执行局部诊断引导的精炼，而不是重新生成整个解释。此外，为了提高自动形式化的忠实度，我们在基于事件的逻辑形式中引入了θ-替换，以强制执行一致的角色-论元绑定。在使用五个LLM骨干的一系列推理任务中，我们的方法实现了最高的解释验证率，相较于最先进水平分别提高了26.2%、21.7%、21.6%和48.9%，同时减少了精炼迭代次数和运行时间，并保持了强大的NLI准确性。
引用
@article{arxiv.2601.19605,
title = {Decompose-and-Formalise: Recursively Verifiable Natural Language Inference},
author = {Xin Quan and Marco Valentino and Louise A. Dennis and André Freitas},
journal= {arXiv preprint arXiv:2601.19605},
year = {2026}
}