大型语言模型（LLMs）在推理任务上表现出色，但其是否反映出忠实的逻辑推理或仅为启发式近似仍不明确。我们通过比较三种范式研究这一问题，包括纯LLM分类、基于LLM的形式推理以及使用Z3 SMT求解器的求解器基础形式推理，分析了ContractNLI重新注释的子集，涵盖五种LLM。我们的重新注释揭示了实用法律解释与严格形式蕴涵之间存在系统性和可测量的差距，其中相当一部分法律上合理的推理在没有额外未声明假设的情况下并未得到形式支持。尽管引入形式结构提高了准确性，LLM基础的形式推理达到了最高的基准性能，但我们表明，这种提升并不意味着忠实的推理。我们识别出三种反复出现的失败模式：
- 范围漂洗：LLMs报告与求解器不一致的分类，而未执行基础的形式推理，得出似乎逻辑上合理但实际上不成立的结论；
- 隐式约束盲点：LLMs忽视形式表示中存在的逻辑约束；
- 程序合成失败：尽管有结构化提示，LLMs仍生成错误的Z3代码。
值得注意的是，范围漂洗在所有模型中普遍存在，这引发了对基于LLM的形式推理作为符号执行代理的忠实性的严重担忧。这些结果揭示了基准准确性与逻辑忠实性之间的根本差距。
博主点评： 本文深入探讨了LLMs在法律推理中的应用局限，尤其是在形式推理的准确性与逻辑严谨性之间的矛盾，值得法律科技领域的研究者关注。如何确保模型输出的法律推理不仅准确且合乎逻辑，是未来的研究方向。