验证人工编写的推理参考基准

研究人员提出一种以参考为中心的评估方法，结合蕴涵检查、完整前提复查与失败归因来验证人工编写的推理链及其形式化表达。在 P-FOLIO 评测中，利用大语言模型（LLM）将推导步骤转化为一阶逻辑并用 Z3 SMT 求解器检查，386 条推导中仅 202 条（52.3%）完全符合检查标准。结果表明 AI 与人工参考不一致可能源于人工参考本身或其形式化表达存在缺陷。