论文
HOLMES：评估LLM中的高阶逻辑推理
HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs
摘要
逻辑推理对可靠AI至关重要——但既有基准大多以一阶逻辑为中心——聚焦固定谓词上的对象级演绎。这错过许多现实场景——模型必须对规则、谓词、函数、约束与决策过程本身推理。我们介绍HOLMES（高阶逻辑遇见真实世界可解释符号推理）——首个面向LLM高阶符号推理的真实世界基准——含1,379实例。HOLMES建立在高阶逻辑上——把自然语言问题与HOL形式化、真值答案、可验证推理踪迹及跨法律与金融的细粒度可控推理因素配对。实验表明当前LLM在HOLMES上仍然吃力——平均准确率仅50.64%、最佳模型达59.54%。我们的分析进一步揭示：高最终答案准确率可能掩盖冲突消解设定中的捷径推理——而性能在范围条件化与组合推理下急剧下降。这些发现把高阶符号推理识别为构建可靠可验证LLM的关键瓶颈。项目代码与数据集公开于 https://github.com/wuyucheng2002/HOLMES。
