一场残酷的对比：50 微秒 vs 最强 AI
想象这样一个场景：你有一个计算任务，一个 1980 年代设计的基于规则的逻辑求解器，在 50 微秒内跑完，准确率 100%。然后你让当今最强大的大语言模型来做同样的事——它最高拿到 65%，换个表述方式就跌到 23.5%，甚至有个模型 80.9% 的回答根本无法解码。
这不是科幻小说的情节，而是 2026 年 6 月科罗拉多大学博尔德分校 Patrick Cooper 和 Alvaro Velasquez 在 arXiv 上发布的 DeFAb 基准测试结果。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% 准确率解决了所有实例。
而最强前沿语言模型，在最优 Chain-of-Thought 提示下，Level 2 规则溯因的最佳准确率仅为 65%。在渲染鲁棒指标（rendering-robust metric，即同一逻辑内容在四种不同表述方式下的最差准确率）下，这个数字进一步跌至 23.5%。
什么是「可推翻溯因」？
要理解 DeFAb 为何如此重要，需要先理解它所测试的能力。
日常推理中，我们大量依赖默认规则：鸟会飞、蛋白质折叠成固定三维结构、汽车有四个轮子。但我们也知道这些规则存在例外：企鹅不会飞、内在无序蛋白（IDP）没有固定结构却功能完备、三轮汽车也存在。
可推翻溯因的任务是：给定一个包含默认规则和已知事实的理论，当观察到与默认规则预测相矛盾的异常时，构建一个最小化的、保守的假设来解释异常——它必须推翻默认规则（仅针对异常情况），同时保留所有其他预测。
Cooper 和 Velasquez 用一个生物学经典案例来说明：1990 年代之前，教科书教条认为每种蛋白质都折叠成固定三维结构，功能由形状决定（锁钥模型）。但当 p53 蛋白的某个内在无序区域（IDR）被发现既无固定结构又功能完备时，这个教条就被打破了。正确的科学回应不是全盘否定结构-功能范式，而是精准地构建一个"击败者"规则：仅对无序蛋白质推翻默认，同时保留对所有常规蛋白质的预测。
这正是 DeFAb 测试的核心——不是"找到一个解释"，而是"找到一个有纪律的、保守的解释"。
基准设计：四个十年的知识图谱注入一个测试框架
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 的最差值，以剥离表述形式敏感性的干扰。
核心发现：六个让 AI 社区坐立不安的数字
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. 叙事模态的全面崩塌
所有模型在形式化模态（M2–M4）上表现尚可（73–94%），但当同一逻辑内容以自然英语散文呈现（M1 叙事模态）时，全部崩塌至 14–22%。这 55–70 个百分点的差距表明，模型在形式化模态上的"高分"反映的是表面语法模式匹配，而非真正的推理能力。M1 模态下 11,765 次解码器失败（对比 M4 的 4,779 次）进一步证实了这一点。
3. Kimi-K2.5：80.9% 的回答完全无法解码
在 Level 3 直接提示下，Kimi-K2.5 的准确率仅为 0.8%（1/125），且有 80.9% 的回答属于 E1 错误（解码器失败）——模型连可解析的假设都生成不出来。然而，解析条件准确率（成功解码后的准确率）高达 72.5%，说明模型在格式合规上存在严重瓶颈，而非完全缺乏推理能力。相比之下，Claude 的解析条件准确率仅为 16.6%，揭示了真正的推理缺陷。
4. CoT 方差（~36pp）超过任何模型间差距
这可能是论文最具方法论冲击力的发现。Chain-of-Thought 提示在八个（模型 × 层级）单元上的标准差约为 36 个百分点，超过了任意两个模型之间的差距。对 DeepSeek-R1 而言，CoT 将 Level 3 准确率提升了 56 个百分点；对 GPT-5.2 提升了 79 个百分点；但对 Claude 反而降低了 14 个百分点——重现了"过度思考"效应。这意味着提示模板的选择主导了测量的能力差异，任何不做策略分离的单一排行榜数字都被这个混淆变量所支配。
5. DeFAb-Hard：最强模型 53.3% vs 符号 100%
研究团队进一步发布了一个 235 实例的 Level 3 难度变体 DeFAb-Hard。在这个更难的数据集上，最强模型仅达到 53.3%，而符号求解器保持 100%。
6. CONJURE：零发现
CONJURE 是 DeFAb 的一个"变革性创造力"变体，包含 560 个 Lean 4/Mathlib 实例，其黄金答案全部是证明助手内核中此前不存在的定义。在单模型试点中，模型在三级新颖性规范下零发现真正的新概念。这个变体用无评判官的多项式时间验证器确立了一个明确的证伪目标。
污染控制：+19.4pp 的残酷真相
对于建立在知名知识库上的推理基准，预训练污染是一个严重威胁。模型可能只是记住了训练语料中的答案，而非真正推理。DeFAb 通过一个巧妙的合成污染控制来解决这个问题：使用音韵学上合法但在 Common Crawl 中零出现的合成谓词（如 "zorbic"、"flentoid"）生成结构匹配的实例，并通过 infini-gram 验证。
匹配注入消融实验分离出平均 +19.4 个百分点的 Level 3 污染差距——即使在纠正后，最佳模型 Level 3 准确率（52.9%）仍然远低于符号天花板。这个差距的上限说明，即使排除记忆效应，LLM 距离真正的可推翻推理仍有相当距离。
这不只是又一个「AI 被羞辱」的故事
DeFAb 的深层意义远超表面的"AI 又输了"叙事。它的方法论贡献有三个层面：
第一，它用多项式时间可验证的金标准精确度量了"有纪律的理论构建"与"流畅但摧毁理论的散文"之间的差距。 每个假设必须通过三个多项式时间检查：有效推导、保守性（保留所有不相关预期）和最小性。这使得逻辑严谨性成为衡量创造力的工具——评分标准不是模型能否写出通顺的解释，而是能否构建一个保守的例外规则。
第二，它揭示了当前 AI 在需要严谨推理时的根本局限性。 论文将其归结为三个纠缠的能力缺陷：接地的缺失（模型缺乏明确的认知结构来区分严格知识与可修正默认）、新颖性的缺失（不知道哪些信念是可修正的，就无法识别创造性例外可能适用的位置）、以及信念修正的缺失（缺乏形式化机制来确保更新遵循最小变化原则）。
第三，它为未来的训练提供了基础设施。 基准的多项式时间验证器可以作为 DPO、RLVR/GRPO 等偏好优化的精确奖励函数。论文还发布了基于同一验证器的自我博弈搜索（AlphaZero 风格）和对抗辩论（MCTS）基础设施。
一个时代的回响
DeFAb 的构建管道有一个令人感慨的注脚：它激活了从 1980 年代起，由日本 FGCS、英国 Alvey、欧洲 ESPRIT、DARPA 战略计算计划等公共资助项目积累的数十年的形式化知识基础设施。这些努力——Cyc、WordNet、ConceptNet、UMLS、Gene Ontology、Wikidata——在深度学习时代被当作评估背景，而非它们原本被设计成的主动形式化脚手架。
Cooper 和 Velasquez 的立场是：这些基础设施并非过时，而是未被充分利用。将它们激活为验证器支持的评估和训练基板，不是回归符号 AI，而是一种综合——将数十年的形式化公共知识变为使可推翻推理的验证器接地的学习成为可能的基础。
在 2026 年，当 LLM 在各种基准上不断刷新高分，这个来自科罗拉多大学博尔德分校的团队用 50 微秒的符号求解器给出了一个清醒的提醒：在需要真正理解"何时应该推翻一个规则"的推理任务上，最强大的 AI 仍有很长的路要走。
