四个模型在不同表述下的最差准确率不超过 23.5%
当一个默认规则遇到例外，模型能否修改规则，同时保留其他仍然成立的结论？DeFAb 用一组可验证的逻辑任务测试这种能力。论文报告，符号求解器处理每个实例不到 50 微秒，准确率为 100%；四个受测大模型对表述方式和输出格式则较为敏感。
这项基准由科罗拉多大学博尔德分校 Patrick Cooper 和 Alvaro Velasquez 于 2026 年 6 月发布在 arXiv。DeFAb（Defeasible Abduction Benchmark）测试的是一种名为「可推翻溯因」（defeasible abduction）的推理能力——在异常出现时构建解释性假设，并在此过程中推翻默认规则，同时保持所有不相关预期的能力。
论文开篇报告："A rule-based logic solver resolves every instance in our benchmark in under 50 microseconds with 100% accuracy." 一个基于 Answer Set Programming（ASP）的符号求解器，运行与生成基准相同的可推翻推理算法，在 50 微秒内以 100% 准确率解决了所有实例。
论文摘要还报告了 65% 的最佳准确率，但正文表 3 的任务标签与数值呈现存在不一致，不宜将其直接用于跨设置比较。下文重点看较明确的「表述稳健性」指标：同一逻辑内容采用四种表述时，取最差准确率。四个受测模型在这一指标上的最高分为 23.5%。
解释异常时，只修改与例外有关的默认规则
DeFAb 所测的能力，可以从日常默认规则和例外的关系来理解。
日常推理中，我们大量依赖默认规则：鸟会飞、蛋白质折叠成固定三维结构、汽车有四个轮子。但我们也知道这些规则存在例外：企鹅不会飞、内在无序蛋白（IDP）没有固定结构却功能完备、三轮汽车也存在。
可推翻溯因的任务是：给定一个包含默认规则和已知事实的理论，当观察到与默认规则预测相矛盾的异常时，构建一个最小化的、保守的假设来解释异常——它必须推翻默认规则（仅针对异常情况），同时保留所有其他预测。
Cooper 和 Velasquez 用一个生物学经典案例来说明：1990 年代之前，教科书教条认为每种蛋白质都折叠成固定三维结构，功能由形状决定（锁钥模型）。但当 p53 蛋白的某个内在无序区域（IDR）被发现既无固定结构又功能完备时，这个教条就被打破了。正确的科学回应不是全盘否定结构-功能范式，而是精准地构建一个"击败者"规则：仅对无序蛋白质推翻默认，同时保留对所有常规蛋白质的预测。
因此，DeFAb 对解释提出两项要求：能消除当前异常，也不破坏其他仍成立的结论。
18 个知识源生成 37.2 万余个实例，分为三类任务
DeFAb 从已有知识库生成测试实例。研究团队将 18 个知识源中的 3375 万条规则转化为可推翻理论，产出了超过 37.2 万个评估实例。这些知识源横跨四十年：从 1984 年的 Cyc 项目（DARPA 资助），到 2025 年的 UMLS 2025AB，涵盖了政府 AI 项目、百科全书式知识库（Wikidata、YAGO、DBpedia）、生物医学本体（Gene Ontology、MeSH）以及法律推理框架（LKIF Core）。
管道将分类学层级结构（OpenCyc、YAGO、Wikidata）与行为属性图（ConceptNet、UMLS）配对，通过一个参数化分区函数 κ 将确定逻辑程序转化为可推翻理论。每个实例的黄金标准答案都经过多项式时间可验证的推导、保守性和最小性检查。
基准分为三个难度层级：
- Level 1（事实补全）：从理论中移除一个事实，模型需要识别缺失的观察。
- Level 2（规则溯因）：移除一条可推翻规则，模型从六个候选（含干扰项）中选择正确的规则。
- Level 3（击败者溯因）：移除一条击败者规则，理论错误地预测了与观察矛盾的结论。模型必须从头构建一条保守的例外规则。
每个实例可以在五种表述模态（M1–M5）下呈现，从最自然的叙事形式（M1）到纯形式化符号（M4），再到视觉接地的 M5 模态。渲染鲁棒准确率取 M1–M4 的最差值，用于衡量模型在不同表述下能否稳定作答。论文的主要模型结果来自 Tier 0 的 409 个专家筛选实例，其中 Level 2 为 374 个、Level 3 为 35 个，并非对全部 37.2 万余个实例逐一测试。
表述、输出格式和提示模板都会影响测试结果
1. 按四种表述中的最差结果计分，准确率为 7.8%–23.5%
四个前沿模型在渲染鲁棒 Level 2 准确率上的表现——Kimi-K2.5 7.8%、GPT-5.2-chat 9.1%、Claude Sonnet 4.6 15.5%、DeepSeek-R1-Distill-Llama-70B 23.5%——全部远低于 ASP 符号求解器的 100% 天花板。论文也列出六选一随机猜测的正确率 16.7%，但它与四种表述取最差值并非同一统计口径，比较时需要区分。
2. 改用自然语言叙述后，准确率降至 14%–22%
所有模型在形式化模态（M2–M4）上表现尚可（73–94%），但当同一逻辑内容以自然英语散文呈现（M1 叙事模态）时，降至 14–22%。论文将这 55–70 个百分点的差距解释为模型对表面形式的依赖。M1 模态下有 11,765 次解码器失败，M4 为 4,779 次，也说明输出解析会显著影响最终得分，不能只据总分推断内部推理机制。
3. Kimi-K2.5 的输出解析失败较多，需与推理错误分开看
论文报告 Kimi-K2.5 在 Level 3 直接提示下准确率为 0.8%（1/125），另报告其 E1 错误（解码器失败）占比为 80.9%，解析成功后的条件准确率为 72.5%。这些数据的聚合范围没有在该段交代清楚，不能直接相乘来还原整体准确率，但都提示输出格式需要单独检查。Claude 的解析条件准确率为 16.6%，论文将其更多归为推导失败。作者也注明，部分解析失败可能来自沿用其他层级的提示模板，因此不能把全部失败都算作模型能力缺失。
4. 加入逐步推理提示后，各模型得分变化不同
提示方式也是一个明显的影响因素。Chain-of-Thought 提示在八个（模型 × 层级）单元上的标准差约为 36 个百分点，超过了任意两个模型之间的差距。对 DeepSeek-R1 而言，CoT 将 Level 3 准确率提升了 56 个百分点；对 GPT-5.2 提升了 79 个百分点；但对 Claude 反而降低了 14 个百分点。这些变化提示，比较模型时应分别报告直接作答和逐步推理的成绩，避免将提示策略差异混入模型能力排名。
5. 在 235 个更难实例中，模型最高分为 53.3%
研究团队进一步发布了一个 235 实例的 Level 3 难度变体 DeFAb-Hard。在这个更难的数据集上，最强模型仅达到 53.3%，而符号求解器保持 100%。
6. CONJURE 单模型试点未发现符合标准的新概念
CONJURE 是 DeFAb 的一个"变革性创造力"变体，包含 560 个 Lean 4/Mathlib 实例，其标准答案是此前未包含在所用形式系统中的定义。在单模型试点中，模型在三级新颖性规范下零发现真正的新概念。该变体使用程序验证器评分，减少对另一模型主观评分的依赖；零发现仍只代表这次单模型试点。
合成词控制实验用于检查模型是否依赖已见知识
对于建立在知名知识库上的推理基准，预训练污染是一个严重威胁。模型可能只是记住了训练语料中的答案，而非真正推理。DeFAb 为此增加了合成污染控制：使用音韵学上合法但在 Common Crawl 中零出现的合成谓词（如 "zorbic"、"flentoid"）生成结构匹配的实例，并通过 infini-gram 验证。
匹配注入消融实验分离出平均 +19.4 个百分点的 Level 3 污染差距——即使在纠正后，最佳模型 Level 3 准确率（52.9%）仍然远低于符号天花板。这组差距与部分记忆效应相符，但陌生词也可能增加理解负担，不能视为彻底排除其他因素后的纯推理能力测量。
可验证评分有助于区分解释是否有效、保守且最小
DeFAb 提供了三类可供后续研究使用的方法：
第一，用程序检查解释是否符合规则。 每个假设必须通过三个多项式时间检查：有效推导、保守性（保留所有不相关预期）和最小性。这使得逻辑严谨性成为衡量创造力的工具——评分标准不是模型能否写出通顺的解释，而是能否构建一个保守的例外规则。
第二，区分规则理解、例外构建与信念修改。 论文将所测问题解释为三类相互关联的能力不足：接地的缺失（模型缺乏明确的认知结构来区分严格知识与可修正默认）、新颖性的缺失（不知道哪些信念是可修正的，就无法识别创造性例外可能适用的位置）、以及信念修正的缺失（缺乏形式化机制来确保更新遵循最小变化原则）。
第三，它为未来的训练提供了基础设施。 基准的多项式时间验证器可以作为 DPO、RLVR/GRPO 等偏好优化的精确奖励函数。论文还发布了基于同一验证器的自我博弈搜索（AlphaZero 风格）和对抗辩论（MCTS）基础设施。
既有知识库可继续用于评估和训练
DeFAb 的实例生成使用了从 1980 年代起，由日本 FGCS、英国 Alvey、欧洲 ESPRIT、DARPA 战略计算计划等公共资助项目积累的数十年的形式化知识基础设施。这些努力——Cyc、WordNet、ConceptNet、UMLS、Gene Ontology、Wikidata——在深度学习时代被当作评估背景，而非它们原本被设计成的主动形式化脚手架。
Cooper 和 Velasquez 的立场是：这些基础设施并非过时，而是未被充分利用。这些知识库提供规则、默认结论与例外，可以与程序验证器结合，用于生成评估实例和训练信号。
对使用者而言，DeFAb 的主要参考价值是把「解释看起来合理」拆成可检查的条件。评估时还需同时报告任务层级、提示方式、格式解析失败率和样本规模，才能判断错误究竟发生在哪一步。
