DeFAb基准：大模型可废止溯因推理仅65%，符号求解器100%

大模型在严谨逻辑推理上的“滑铁卢”：DeFAb 基准揭示巨大差距

当规则驱动的逻辑求解器能在 50 微秒 内以 100% 准确率 解决所有推理实例时，最先进的大语言模型（LLM）表现如何？答案是：最高仅 65%，且在严格的渲染鲁棒性评估下，最差成绩跌至 23.5%。

这一数据来自新近发布的 DeFAb（Defeasible Abduction Benchmark）——一个专注于“可废止溯因推理”的严格基准。该研究由 Patrick Cooper 和 Alvaro Velasquez 完成，论文已在 arXiv 上公开。

简单来说，这是一种高级推理形式：面对一个异常现象，你需要提出一个假设来解释它，但这个假设必须在推翻某些默认规则的同时，保留其他无关的预期。它本质上是在进行“理论修订”——既要解释异常，又不能破坏整个知识体系的稳定性。

这种推理对 AI 的“创造力”和“逻辑严谨性”提出了双重要求：不能天马行空地编造故事，而必须在严格约束下进行理论构建。

DeFAb 的核心资产是一个大规模、可验证的基准数据集，其构建方式颇具匠心：

数据来源：整合了来自 OpenCyc、YAGO、Wikidata 等分类学知识库，以及 ConceptNet、UMLS 等行为属性图——总计 18 个数据源，跨越四十年公共资助的知识工程成果。
规模：生成了 372,648+ 个实例，涉及 3375 万条物化规则，分为三个难度等级。
验证机制：每个假设必须通过多项式时间可验证的检查，包括有效推导、保守性和最小性检验。这意味着逻辑严谨性本身就是衡量创造性的标尺。

研究团队测试了四个前沿大模型，结果令人警醒：

Level 2 的渲染鲁棒准确率仅为 7.8% 到 23.5%。所谓“渲染鲁棒”是指用四种不同的表面形式呈现同一问题，取最差结果——这模拟了真实世界中问题表述多样性的挑战。
思维链（CoT）的方差高达约 36 个百分点，超过了任何模型之间的差距，说明模型内部的不稳定性远超模型能力的差异。
通过匹配的污染控制实验，研究人员发现 Level 3 难度下存在 +19.4 个百分点的差距，表明模型可能在某些情况下表现出虚假的能力。

研究团队还额外发布了两个变体：

DeFAb-Hard：包含 235 个 Level 3 难度的实例，最佳模型准确率仅为 53.3%，而符号求解器依然是 100%。
CONJURE：这是一个基于 Lean 4/Mathlib 的“内核验证的变革性创造力”变体，包含 560 个实例。其“黄金答案”是证明内核中之前不存在的定义——也就是说，模型必须真正创造出新的数学概念。初步实验发现，模型未能产生任何新颖概念。

DeFAb 的价值不仅在于评估。研究指出，其验证器可以作为 DPO、RLVR/GRPO 等偏好优化方法 的精确奖励信号。这意味着它不仅能“考试”，还能用于“教学”——直接指导模型学习更严谨的推理。

这一结果再次印证了当前大语言模型在需要严格逻辑约束的任务上的根本性短板。尽管在自然语言生成、常识问答等领域表现惊艳，但在面对“可废止溯因”这种需要平衡创造性与逻辑一致性的任务时，模型往往倾向于产生“流畅但破坏理论”的文本，而非真正严谨的假设。

DeFAb 的发布为 AI 推理能力评估提供了一个新的“压力测试”，也提示研究者：如果想让大模型真正具备科学发现或理论构建的能力，仅仅依靠数据驱动的方法可能远远不够。符号逻辑的严谨性与神经网络的灵活性如何结合，仍是未来需要攻克的核心难题。

该基准已以 MIT 许可证在 GitHub 上开源，代码、数据和评估工具包均可获取。