验证人工撰写的推理参考

对 AI 系统的推理能力进行评估通常依赖人工撰写的推理链作为参考，然而，这些推理链中各个步骤的逻辑支持却很少得到验证。尽管先前的神经符号方法已经对推理进行了形式化和检查，但其报告的评估并未系统地考察人工撰写的参考推导中各步骤的结论是否由其所引用的前提集合蕴涵，也未探究这些参考推导失败的原因。为弥补这些局限，我们提出了一种以参考推导为中心的新型评估方法，用于评估人工撰写的推导。该方法结合了针对所引用前提集合的蕴涵检查、完整前提复核以及失败归因，以考察这些推导及其形式化表示的可靠性。我们在 P-FOLIO 上对该方法进行了评估，使用大型语言模型（LLM）将步骤结论翻译为一阶逻辑（FOL），并使用 Z3 SMT solver 检查蕴涵关系。在所检查的 386 个推导中，有 202 个（52.3%）满足我们的全部检查标准，这意味着每个经过翻译的步骤都能由其所声明的支持蕴涵，并且在现有 FOL 表示下能够推出所需目标。在 230 个无法由其所声明支持蕴涵的步骤中，有 191 个在使用完整的原始前提进行检查时变得可被蕴涵，这表明大多数初始失败源于支持信息不完整或不匹配，而非结论缺乏支持。对剩余 39 个案例的人工分析发现，其中有 21 个属于人工推理错误，11 个属于 FOL 翻译错误，7 个属于数据集标注错误。对随机抽取的 50 个通过蕴涵检查的步骤进行的另一项人工审查发现，其中 46 个具有忠实的 FOL 翻译（92%）。这些发现表明，与人工撰写的推理参考不一致，可能源于参考本身或其形式化表示，而不一定是被评估的 AI 系统所致。