← 返回 PaperDaily 大模型与智能体

北大最新基准HOLMES：LLM高阶逻辑推理平均仅50.64%，最佳模型也才59.54%！

我们评估模型推理能力，还在用“答没答对”来一锤定音？北大等机构的最新研究HOLMES告诉你，答案对了，但推理过程可能全是“捷径”！这个首个面向高阶逻辑推理的真实世界基准，无情地揭露了GPT-5.4、DeepSeek、Qwen等一众顶级大模型，处理起需要“规则打架”、“跨范围组合”的现实问题时，表现有多拉胯。是时候关注推理过程的“忠信度”了。

龙哥读论文发布于 2026-08-14 09:10:44 阅读 4 查看原文

#大语言模型 #AI金融 #AI应用

北大最新基准HOLMES：LLM高阶逻辑推理平均仅50.64%，最佳模型也才59.54%！

🐉 龙哥读论文知识星球来了！
公众号每日8篇拆解不够看？星球无上限更AI领域论文、资讯、招聘、招博、开源代码，一站式干货，每日2分钟刷完即赚！ 👇扫码加入「龙哥读论文」知识星球，前沿干货、实用资源一站式拿捏～ xingqiu_header

龙哥推荐理由：
我们评估模型推理能力，还在用“答没答对”来一锤定音？北大等机构的最新研究HOLMES告诉你，答案对了，但推理过程可能全是“捷径”！这个首个面向高阶逻辑推理的真实世界基准，无情地揭露了GPT-5.4、DeepSeek、Qwen等一众顶级大模型，处理起需要“规则打架”、“跨范围组合”的现实问题时，表现有多拉胯。是时候关注推理过程的“忠信度”了。

原论文信息如下：

论文标题:
HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs

发表日期:
2026年06月
发表单位:
北京大学（北京大学多媒体信息处理国家重点实验室、计算机学院、人工智能研究院），北京人工智能研究院，新加坡国立大学，YiXin-AILab
原文链接:
https://arxiv.org/pdf/2606.23238v1.pdf
开源代码链接:
https://github.com/wuyucheng2002/HOLMES

直觉不一定正确：LLM高阶推理的“捷径”真相

各位有没有想过一个细思极恐的问题：当你问一个AI“张三有没有罪”并且得到正确答案时，它到底是真的仔细推敲了所有法条，还是仅仅蒙对了一个关键规则？最近北大等机构的一项新研究HOLMES，就像一面照妖镜，让所有大模型“走捷径”的行为原形毕露。

传统的逻辑推理基准（比如一阶逻辑的ProofWriter或FOLIO）只考察模型在固定谓词下对物体的演绎。但现实中，法律条文有冲突时要判断优先级，财务报销要按不同人员等级选择规则——这时模型需要把规则本身当作推理对象，这就是高阶逻辑（Higher-Order Logic，HOL）的核心思想。本文发现：即使答案正确，模型的推理过程也常常是残缺的捷径，而不是完整的规则推导。

图1：一阶逻辑（FOL）与高阶逻辑（HOL）推理的对比。FOL在固定谓词下对对象进行演绎；HOL可以将谓词、函数和规则本身作为推理对象。

图1清晰展示了区别：左侧在一阶逻辑下，只能问“猫在垫子上吗？”；右侧在高阶逻辑下，可以直接问“规则P比规则Q更宽松吗？”——规则成了被推理的对象。

HOLMES：首个高阶逻辑推理的真实世界“试炼场”

要揭穿模型的捷径，必须先有一个能全面考核高阶推理能力的数据集。这就是HOLMES（全称Higher-Order Logic Meets real-world Explainable Symbolic reasoning）的使命。它包含了1379个实例，来自两个高风险领域：法律和金融。每个实例都配有人类可读的自然语言问题、严格的高阶逻辑形式化（HOL形式化）、正确答案、可验证的推理链，以及精细的推理因素标注。

图3：HOLMES构建流程。自然语言文档被形式化为HOL规则，实例化为案例逻辑框架，再渲染为自然语言案例。HOL求解器产生验证过的正确答案，用于评估LLM。

图3展示了构造流程：从真实或虚构的规则文档出发，用Isabelle/HOL（一个高阶逻辑的机械证明助手）进行形式化，然后通过受控生成机制产生案例，确保每个案例都有唯一正确的推理路径。同时，HOL求解器会输出完整的推理链作为黄金标准。

HOLMES的数据集统计信息见图4：法律部分有300个实例，涉及285条规则，强调冲突解决；金融部分有1079个实例，涉及58条规则，强调范围条件和组合推理。总体规模适中，但难度不容小觑。

图4：HOLMES数据集统计。左表总结法律和金融部分的关键统计量；中间饼图显示各领域和任务类型的实例分布；右条形图显示按冲突数量（法律）和范围数量（金融）的实例计数。

图4告诉我们，法律案例中最多涉及20个冲突规则，金融案例中推理深度最高达到75步。这可不是简单的问答，而是真正的烧脑任务。

法律对决：当“优先级”和“例外”成为推理对象

在法律领域，典型的场景是：多条法律条文同时适用于一个案件，但它们之间可能有冲突。比如，一条重罪条文规定“盗窃超过10万元处10年以上”，另一条轻罪条文规定“初次盗窃且退赃的减刑”，还有一条优先级规则说“特别法优于一般法”。模型需要判断哪条规则最终生效。

图2：法律和金融示例。从左到右：事实和关键规则触发候选结论，HOL机制解决冲突，产生最终答案。法律示例展示规则层级推理，优先级和例外关系击败竞争条文，保留C条文；金融示例展示范围限制约束检查，两个申请通过相同初审但在650元/晚住宿上限处分歧。

图2左侧的法律案例（读法：从左到右）演示了规则层级的推理：事实A、B和规则1、2、3触发候选结论，优先级关系（≺）和例外关系击败了A、B，最终只有C没有被击败，模型必须得出C有效。

HOLMES的法律部分构建了两类冲突：优先级冲突（Priority conflict，两个规则同时触发，优先级高的生效）和例外冲突（Exemption conflict，例外规则击败否则适用的规则）。这些冲突都经过Isabelle/HOL验证，确保逻辑一致性。

结果怎么样？从主结果表（表1）看，法律部分的准确率看起来还不错——最好的模型Qwen3.6-Flash达到了86.33%，最差的也有63.33%。但这真的代表模型会执行完整的冲突解决过程吗？图5和深度分析给出了答案。

图5：不同冲突数量下的性能。(A)案例准确率随冲突数量变化不大；(B)黄金冲突解决规则的召回率随冲突增加急剧下降，而精确率略有上升，表明选择性且不完全的规则覆盖；(C)ROUGE-L和SRMR F1得分稳步下降，显示在最终准确率稳定的同时推理质量下降。

图5A显示，冲突数量从1增加到6时，准确率并没有显著下降，反而略有波动。这很奇怪：按理说规则越多越难，为什么模型反而能答对？图5B揭示了原因：当冲突规则增加时，模型对黄金冲突解决规则的召回率急剧下降（从约0.8降到0.3），而精确率反而上升。这说明模型只记住了最关键的几条规则（比如最高优先级的规则），忽略其他冲突规则，直接跳向答案。它们走的不是法律人的严谨路径，而是“找老大”的捷径。图5C显示推理质量（ROUGE-L和SRMR F1）持续下降，证实了这一点。

金融难题：范围约束和规则组合导致“思维断链”

如果说法律部分让模型暴露了“偷懒”，那金融部分则是彻底击穿了模型的推理天花板。金融报销场景要求模型根据员工类别（教授、研究员、学生等）应用不同的住宿、餐饮、差旅标准，还要进行金额计算和合规检查。图2右侧演示了一个具体例子：赵某和林某同时申请报销，初始检查都通过，但在住宿费650元/晚上限处，赵某的申请获得全额批准，林某只获得部分批准——因为林某超出了限额。

金融部分还特别构造了两种高阶组合场景：并行推理（Paralle cross scopes）和规则组合（Composition across rules）。并行要求模型同时处理多类人员的报销，然后汇总——比如在同一场景下为教授和研究生分别计算报销结果。规则组合要求输入中包含多个异构报销场景，每个适用不同规则，模型需分别推理后聚合答案。

表1的结果让人大跌眼镜：金融部分整体准确率不到50%，最好的模型Qwen3.6-Flash也只有52.09%。而且模型在生成推理链时，ROUGE-L得分普遍在21%-25%之间，说明生成的推理步骤与黄金推理链匹配度极低。即使是语义上的BERTScore也只有0.83左右。

图6比较了Instruct（标准指令模型）和Thinking（思维链模型）两类变体。Qwen3-30B-Instruct与Qwen3-30B-Thinking的表现差异揭示了重要规律。

图6：Instruct和Thinking模型在不同任务类型上的准确率。(A)Thinking模型在大多数原子任务上优于Instruct；(B)并行任务中，Instruct在低类别数时表现更好，而Thinking在高复杂度时获得优势；(C)组合场景下，两种模型的准确率都急剧下降。

图6A显示，在原子任务（单个简单报销）上，Thinking模型整体更好，特别是在数值计算（金额计算）上从0.15提升到0.57。图6B的并行任务中，当只有2-3个类别时，Instruct反而更好，说明Thinking在简单场景下可能带来不必要的干扰；但当类别增加到4-5个时，Thinking优势明显，说明复杂并行任务中显式推理有助协调。图6C的组合场景则是最致命的：当组合场景数增加到5时，两个模型准确率都趋近于0。这意味着组合多分支推理对当前模型来说几乎是不可能的。

这种“思维断链”现象说明，当前LLM在需要同时保持多个独立规则应用链、并在最后聚合时显得力不从心。即使给了思考时间（Thinking模型），也逃不过组合爆炸的困难。

深度诊断：最终答案准确率为何会“骗人”？

综合法律和金融两个领域的分析，HOLMES论文给出了两个关键诊断：

诊断一：最终答案准确率掩盖了“捷径推理”。在冲突解决场景中，模型通过识别最高优先级或最关键的例外规则直接跳向答案，而不完整处理所有冲突规则。这导致准确率看似稳定，但召回率暴跌、推理质量下降。如果只盯着“答对率”，会误以为模型逻辑能力过关，其实只是蒙对了关键规则。

诊断二：范围条件和组合推理是当前LLM的真正瓶颈。金融部分的实验表明，当推理深度增加、数值计算出现、需要同时应用多条规则并聚合时，模型性能断崖式下跌。尤其是组合场景，从2个组合到5个组合，准确率从约0.52降至0.03，几乎丧失能力。这说明LLM不具备可靠的规则级组合能力，即使加入了思维链也无济于事。

这两个诊断直接指向一个结论：要构建可验证、可信赖的AI，光靠“答案正确”是不够的，必须把推理过程作为诊断指标。HOLMES正是这样一个提供了完整推理链标注的测试床，让研究者能像照CT一样看清楚模型的逻辑病灶在哪里。

此外，论文还评估了11个开源和商用模型，平均准确率仅50.64%。最佳模型Qwen3.6-Flash综合表现59.54%——这还是达到了及格线？实际上远未及格，因为金融部分严重拉低了总分。所有模型在推理一致性上都有巨大提升空间。

龙迷三问

下面是龙哥对于大家可能的一些问题的解答：

HOLMES与已有的逻辑推理基准（如FOLIO、ProofWriter）有何本质区别？已有的基准主要基于一阶逻辑（FOL），让模型在固定谓词下对个体进行演绎，例如“如果所有人都会死，苏格拉底是人，那么苏格拉底会死”。而HOLMES基于高阶逻辑（HOL），要求模型把规则、谓词、函数本身作为推理对象。例如判断“规则P是否比规则Q更严格”或者“在冲突的规则中哪个应该优先适用”——这更贴近律师或合规官的真实工作。另外，HOLMES提供可验证的推理链标注，能诊断模型是真正推理还是走捷径。

HOLMES中的“推理深度”指的是什么？推理深度（Reasoning Depth）指从给定事实出发，经过规则应用、中间推导、条件判断直到最终答案所经历的推理步骤数量。法律案例中，每应用一条规则或解决一次冲突就算一步，深度范围3-20；金融案例中，细粒度条件检查（如金额比较、违规判断）也计入步骤，深度可达75步。深度越大，模型犯错的概率越高，论文的实验也证实了这一点。

HOLMES的结果是否可以推广到其他领域（如医疗、程序验证）？论文目前只聚焦法律和金融，但高阶逻辑普遍存在于其他高风险领域——医疗诊断（需考虑多种治疗指南的优先级）、程序验证（函数和模块的组合推理）、政策合规（多层级法规的交叉约束）。HOLMES的构建方法论（规则形式化→受控生成→HOL求解器验证）具有领域迁移性，但需要领域专家参与设计规则束和形式化编码。论文也提及了向更多领域扩展的展望。

如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

龙哥点评

论文创新性分数：★★★★★ 首次将高阶逻辑引入LLM推理评估，填补了关键空白。不仅提出了基准，还提供了完整的推理链标注，使诊断成为可能。

ZZZ

实验合理度：★★★★✰ 评估了11个主流模型，覆盖开源和商用，并进行了细致的冲突解析和组合分析。但金融部分只用了单一报销政策，通用性稍弱。

学术研究价值：★★★★★ 给LLM推理研究提供了一个全新的诊断维度，提醒社区不要被答案准确率欺骗。对构建可验证的AI系统具有里程碑意义。

稳定性：★★★✰✰ 当前模型在高阶推理中极不稳定，尤其是组合场景下几乎失效。即使同一模型在不同案例上表现差异也很大。

适应性以及泛化能力：★★★✰✰ 只覆盖法律和金融两个领域，泛化到其他领域还需要额外工作。但构建方法论是可迁移的。

硬件需求及成本：★★★★✰ 作为评估基准，不需要特定硬件。但用Isabelle/HOL验证需要一定计算资源，不过一次性。

复现难度：★★★★✰ 论文已开源代码和数据集（GitHub: wuyucheng2002/HOLMES），但需要理解Isabelle/HOL和一些定制化构建，有一定学习成本。

产品化成熟度：★★✰✰✰ 当前是研究性质的基准，还不能直接用于产品。但它揭示的模型弱点对落地关键决策系统（如法律辅助、财务合规）有重要警示价值。

可能的问题： 金融部分数据量较大但问题类型有限（仅报销场景）；法律部分包含虚构规则，是否完全反映真实法律推理还有待验证。另外，论文没有对“捷径推理”给出解决方案，只做了诊断。希望后续工作能提出改进方法。

主要参考文献

[1] HOLMES: Evaluating Higher-Order Logical Reasoning in LLMs. Yucheng Wu et al., 2026. arXiv:2606.23238.

[2] ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language. Tafjord et al., 2021. ACL.

[3] FOLIO: Natural Language Reasoning with First-Order Logic. Han et al., 2024. EACL.

[4] Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Nipkow et al., 2002. Springer.

[5] DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. DeepSeek-AI, 2025. arXiv:2501.12948.

[6] Qwen3 Technical Report. Yang et al., 2025. arXiv:2505.xxxxx.

*本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～想了解更多原文细节的小伙伴，可以点击"阅读原文"，查看更多原论文细节哦！

大模型在复杂的法律条文和金融报销规则面前，可能还不如一个初入职场的新人？请速将你的思考心得分享到龙哥读论文粉丝群，一起探讨LLM高阶推理的瓶颈究竟在哪！
欢迎加入龙哥读论文粉丝群，扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。一定要备注：研究方向+地点+学校/公司+昵称（如图像处理+上海+清华+龙哥），根据格式备注，可更快被通过且邀请进群。
『龙哥读论文』微信群目前包含：图像处理、大模型及智能体、自动驾驶及机器人、AI医疗及AI金融5个群
wechat_helper