DeFAb: 基础模型中可废止溯因的可验证基准

# DeFAb：面向基础模型的可废止溯因可验证基准

**来源：** https://arxiv.org/html/2606.18557

**Patrick Cooper**  
科罗拉多大学博尔德分校  
patrick\.cooper@colorado\.edu  

**Alvaro Velasquez**  
科罗拉多大学博尔德分校  
alvaro\.velasquez@colorado\.edu  

###### 摘要

一个基于规则的逻辑求解器在不到50微秒内以100%的准确率解决基准中的每个实例。最先进的前沿语言模型最高达到65%，而在渲染鲁棒性评估（相同逻辑内容在四种表面呈现下的最差情况）下则降至23.5%。我们提出了DeFAb（可废止溯因基准），这是一个数据集和生成流水线，将四十年来公共资助的知识库转化为形式化可验证的评估实例，用于可废止溯因任务：即通过覆盖默认结论同时保留无关预期来构建解释异常的假设。由于每个假设都必须通过多项式时间可验证的有效推导、保守性和最小性检查，DeFAb将逻辑严谨性转化为衡量创造力和理论推理的工具，评判的是对理论修订的规范化构建，而非流畅但破坏理论的文本。该流水线将分类层次结构（OpenCyc、YAGO、Wikidata）与行为属性图（ConceptNet、UMLS）配对，从18个知识源生成372,648+个实例，跨越3375万条物化规则，并按三个难度级别分层，每个级别都有多项式时间可验证的金标准假设。对四个前沿模型的评估显示，当前模型未能可靠地内化可废止推理：渲染鲁棒性下的Level 2准确率介于7.8%至23.5%之间；Kimi-K2.5的80.9%响应完全解码失败；思维链提示的方差（跨越八个模型级细胞σ≈36pp）超过任意两个模型之间的差异；一个合成污染控制实验，通过匹配的事实注入消融加以强化，分离出平均Level 3污染差距为+19.4pp。我们进一步从三个维度对基准进行压力测试：一个DeFAb-Hard变体（由相同流水线生成的235实例Level 3难度试点，最强模型达到53.3%，而符号求解器保持100%）；跨本体和跨环境的泛化研究，覆盖18个知识源，涵盖生物学、法律、材料及一个完全不相交的"交战规则"领域；以及一个视觉接地（M5）模态，视觉语言模型在其中继承了相同的解码器脆弱性。此外，我们发布了CONJURE，一个DeFAb的核验证变换式创造力变体，包含560个Lean 4/Mathlib实例，其金标准答案是指令助手的核之前未曾包含的定义，并配有无评判者的多项式时间验证器；一个诚实的单模型试点在三层新颖性规范下发现零个真正新颖的概念，确立了该轨道校准的证伪目标。该基准的多项式时间验证器还可作为偏好优化（DPO、RLVR/GRPO）的精确奖励函数，从而将基于验证器的训练作为已发布基础设施的下游用途。数据集、流水线和评估工具在MIT许可下发布于：https://huggingface.co/datasets/PatrickAllenCooper/DeFAb。

## 1 引言

一个基于规则的答案集编程求解器，运行与我们生成基准相同的可废止推理算法，在不到50微秒内以100%的准确率解决每个评估实例（Maher, 2001 (https://arxiv.org/html/2606.18557#bib.bib11)）。最先进的前沿语言模型，在最优的思维链提示下，在Level 2规则溯因上达到65%。在渲染鲁棒性指标（相同逻辑内容在四种表面呈现下的最差准确率）下，它达到23.5%。这一差距表明当前基础模型的推理与基准所需的显式信念修订操作之间存在结构性错配。

这一差距反映了当前基础模型在三种能力上的纠缠错配。第一个是**接地**的不足：模型缺乏明确的认知结构来区分严格知识与可修改默认值，无法将预测追溯到其支持证据（Dunker et al., 2001 (https://arxiv.org/html/2606.18557#bib.bib26)）。第二个是**新颖性**的不足：不知道哪些信念是可修改的，模型就无法识别可能适用创造性例外的地方。一个引人注目的生物学例证是 intrinsically disordered proteins (IDPs) 的发现，即缺乏固定三维结构但功能上仍然必需的蛋白质。一个在流行的结构-功能教条上训练的人工智能，不太可能假设IDPs的存在，因为该假设直接与其训练语料中编码的领域知识相矛盾。第三个不足是**信念修订**：即使模型确实更新了知识，它们也缺乏形式化机制来确保更新遵循最小变化原则（Alchourrón et al., 1985 (https://arxiv.org/html/2606.18557#bib.bib45)），即在容纳新证据的同时尽可能少地干扰现有承诺。IDP例子同时说明了所有三个不足，因为发现不仅需要断言无序蛋白质存在，还需要通过有针对性的修订来实现：该修订覆盖了特定子类的结构-函数默认值，同时保留了对常规结构蛋白质的预测。

可废止推理提供了这些不足所需的结构。在可废止理论中，每个结论都通过严格规则和可废止规则的可追溯链推导出来，每个默认值都是显式可修改的，每条证据都参与一个可识别的支持集。这提供了接地、新颖性的机制，以及通过我们的保守性要求（定义A.5 (https://arxiv.org/html/2606.18557#A1.Thmtheorem5)）对理性信念修订的具体操作化，该要求确保解决方案除目标异常外保留所有预期，并直接实现AGM最小变化假设（Gärdenfors, 1988 (https://arxiv.org/html/2606.18557#bib.bib46); Katsuno and Mendelzon, 1991 (https://arxiv.org/html/2606.18557#bib.bib48)）。

这种重新框架带来了方法论上的回报：由于可废止理论使推导、保守性和最小性在多项式时间可判定，逻辑严谨性成为衡量创造力和理论推理的工具，评判的是模型能否构建有效的理论修订（发明或修复一条规则，解决异常而不产生附带损害），而非能否产生流畅但破坏理论的解释。经典逻辑在常识推理中缺乏的严谨性，恰好在此处使创造性和理论能力变得可审计，区分了一个保守例外和一个看似合理但过度泛化的表述。

大规模实现这一框架所需的基础设施已经存在。从20世纪80年代开始，公共资助项目（日本的FGCS (Fuchi, 1981 (https://arxiv.org/html/2606.18557#bib.bib27); Feigenbaum and Shrobe, 1993 (https://arxiv.org/html/2606.18557#bib.bib28))、英国的Alvey (Thomas, 1985 (https://arxiv.org/html/2606.18557#bib.bib29))、欧洲的ESPRIT、DARPA的战略计算资助Cyc (Lenat et al., 1990 (https://arxiv.org/html/2606.18557#bib.bib30); Lenat, 1995 (https://arxiv.org/html/2606.18557#bib.bib31))）追求以可修改逻辑形式编码常识和专家知识。这一势头通过NSF（WordNet (Miller, 1995 (https://arxiv.org/html/2606.18557#bib.bib32))、ConceptNet (Speer et al., 2017 (https://arxiv.org/html/2606.18557#bib.bib33))）、NIH（UMLS (Lindberg et al., 1993 (https://arxiv.org/html/2606.18557#bib.bib38))、Gene Ontology (Ashburner et al., 2000 (https://arxiv.org/html/2606.18557#bib.bib39))）、EU本体（LKIF Core (Hoekstra et al., 2007 (https://arxiv.org/html/2606.18557#bib.bib40))、BabelNet (Navigli and Ponzetto, 2012 (https://arxiv.org/html/2606.18557#bib.bib37))）以及百科项目Wikidata (Vrandečić and Krötzsch, 2014 (https://arxiv.org/html/2606.18557#bib.bib34))、DBpedia (Lehmann et al., 2015 (https://arxiv.org/html/2606.18557#bib.bib35)) 和YAGO (Suchanek et al., 2024 (https://arxiv.org/html/2606.18557#bib.bib36)) 得以延续。这些努力编码了可废止推理所需的两个要素：默认泛化与结构化例外（Wikidata的P2303“约束例外”、ConceptNet的NotCapableOf、Gene Ontology的NOT限定注释）。在深度学习时代，这些基础设施被视为评估背景而非其本应成为的主动形式化脚手架。DeFAb认为这些基础设施并未过时，只是被低估使用，将其激活为基于验证器的评估和训练基底构成了一次新的推进：不是回归符号AI，而是综合，使得几十年形式化的公共知识成为使基于验证器的可废止推理学习成为可能的真实基础。

(1) 默认规则  
教科书教条：每个蛋白质折叠成固定3D结构；功能通过锁-键原则跟随形状。  
protein(X) ⇒ has_3d(X) ⇒ func(X, lock) 符合PDB 1996年前数据  

(2) 异常  
p53_idr有功能但无固定3D结构；默认预测¬func。  
disordered(p53_idr), functional(p53_idr): 两者均被观察到；默认矛盾。  
预测与观察矛盾  

(3) 构建的击败者  
所需修订：仅对无序蛋白质覆盖默认值，保留所有其他预测。  
disordered(X), protein(X) ⇒ func(X, conf), r4 ≻ r2  
保守的、新颖的、机理性的  
观察 → 溯因  

验证器以小于50μs的时间和100%准确率解决任何此类实例。前沿LLM在L3直接上：0.8–37%；渲染鲁棒性：7.8–23.5%。DeFAb使这一差距可测量、受污染控制且可训练。

**图1：** 作为击败者溯因的内在无序蛋白质（IDP）发现，说明了DeFAb测量和训练的任务。(1) 教科书默认：蛋白质折叠成决定功能的3D结构。(2) 异常：p53_idr有功能但无序，与默认预测矛盾。(3) 所需修订：一条新规则，仅对无序蛋白质覆盖默认值，并假设新机制（构象系综）。多项式时间验证器在微秒级解决此类实例；前沿LLM则不能。

构建此领域的任何基准还面临另一个障碍。对于记录良好的默认和例外，如"鸟会飞"和"企鹅不会飞"，我们无法区分真正的可废止推理与检索记忆的预训练解决方案。Zhang et al. (2024 (https://arxiv.org/html/2606.18557#bib.bib91)) 证明了由于污染导致的小学数学准确率下降，LiveCodeBench (Jain et al., 2025 (https://arxiv.org/html/2606.18557#bib.bib92)) 甚至通过时间分段评估暴露了前沿模型中的污染。对于基于众所周知知识库的可废止推理基准，风险尤为严峻，解决它需要评估实例的解决方案可证明超出任何预训练语料。

我们提出DeFAb（可废止溯因基准）以共同解决这些不足。图1 (https://arxiv.org/html/2606.18557#S1.F1) 展示了中心实例类型。我们演示的贡献包括：(i) 一个生成流水线，通过一个参数化划分函数κ和三个级别（事实补全、规则溯因、击败者溯因）的多项式时间实例生成，在形式保守性下将确定逻辑程序转换为可废止理论；(ii) 跨越18个知识源和3375万条物化规则（从Cyc (1984) 到 UMLS 2025AB）的跨本体提取；(iii) 通过infini-gram (Liu et al., 2024 (https://arxiv.org/html/2606.18557#bib.bib93)) 验证谓词在Common Crawl中不存在的合成污染控制；(iv) 四个前沿模型的基线评估，揭示了渲染鲁棒性评估下的脆弱性（7.8–23.5%）、高解码器失败率，以及主导测量能力的提示方差（σ=36pp）；(v) 一个将表面形式敏感性与认知推理分离的渲染鲁棒性评估指标；(vi) 一组鲁棒性消融实验——匹配注入的污染差距为+19.4pp，约束输出消融将格式与推理分离，以及跨基准比较暴露了90+ pp的排名反转；(vii) DeFAb-Hard，一个由相同流水线生成的难度分层变体（三个预注册轴上的235个Level 3实例），将前沿映射到当前能力之上；(viii) 跨领域迁移到完全不相交的"交战规则"领域，包括一个验证器门控指挥官，其形式检查对提示注入越狱具有鲁棒性，以及一个视觉接地（M5）模态，配备开放式VLM试点；(ix) CONJURE，一个DeFAb的核验证变换式创造力变体（560个Lean 4/Mathlib实例，跨越八个Lakatos系列），其每个金标准答案都是证明助理核之前未包含的定义，配有无限判者的多项式时间验证器和一个诚实的单模型试点；(x) 发布的自博弈搜索（AlphaZero风格的在击败者构建MDP上的专家迭代）和对抗性辩论（MCTS与作者-算法证明排列）基础设施，两者都基于同一精确验证器，并配有预注册评估和符号辩论流水线验证试点。该流水线的多项式时间验证器还可用作DPO、RLVR/GRPO和验证器门控重新提示的精确奖励函数；训练模型演示留待后续工作。

## 2 相关工作

非单调推理有着悠久的形式历史。Reiter的默认逻辑 (Reiter, 1980 (https://arxiv.org/html/2606.18557#bib.bib1)) 和McCarthy的限定 (McCarthy, 1980 (https://arxiv.org/html/2606.18557#bib.bib2)) 解决了经典逻辑在常识推理中的不足，Nute的可废止逻辑 (Nute, 1987 (https://arxiv.org/html/2606.18557#bib.bib3), 1994 (https://arxiv.org/html/2606.18557#bib.bib4)) 提供了一种计算上易处理的替代方案。KLM框架 (Kraus et al., 1990 (https://arxiv.org/html/2606.18557#bib.bib6)) 为理性非单调推理提供了公理基础。我们采用的证明理论遵循Antoniou et al. (2001 (https://arxiv.org/html/2606.18557#bib.bib10))，他们与Maher (2001 (https://arxiv.org/html/2606.18557#bib.bib11)) 一起确立了命题可废止推导具有线性时间复杂度，这一结果为我们的生成流水线的易处理性奠定了基础。在信念修订方面，AGM假设 (Alchourrón et al., 1985 (https://arxiv.org/html/2606.18557#bib.bib45); Gärdenfors, 1988 (https://arxiv.org/html/2606.18557#bib.bib46)) 提供了在新证据下更新信念的理性条件，Dalal (1988 (https://arxiv.org/html/2606.18557#bib.bib47)) 引入了基于距离的修订。我们的保守性要求将最小变化操作化于可废止设置中，我们的修订距离提供了Dalal距离度量的一种易处理类比。

现有的推理基准主要评估前向单调推理。