论文
认识你的极限：LLM作为法律推理求解器与自动形式化器的忠实性
Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning
摘要
大语言模型（LLM）在推理任务上表现强劲——但这是否反映忠实的逻辑推断抑或启发式近似仍不清楚。我们在法律蕴含中研究该问题——在重新标注的ContractNLI子集上跨五个LLM比较三种范式：纯LLM分类、基于LLM的形式推理与使用Z3 SMT求解器的基于求解器的形式推理。我们的重新标注揭示语用法律解释与严格形式蕴含之间系统且可测的差距——相当比例法律上成立的推断在无额外未声明假设时并无形式根据。虽然引入形式结构提升准确率——基于LLM的形式推理取得最高基准性能——但我们表明该增益不意味着忠实推理。我们识别三种反复出现的失败模式：范围洗白——LLM未执行底层形式推理却报告与求解器不一致的分类——产出貌似有逻辑根据实则不然的结论；隐式约束盲区——LLM忽视形式表示中的逻辑约束；程序综合失败——LLM在结构化提示下仍生成错误的Z3代码。关键的是——范围洗白跨所有模型持续存在——对以基于LLM的形式推理作为符号执行代理的忠实性提出严重关切。这些结果揭示基准准确率与逻辑忠实性之间的根本差距。
