DeFAb: A Verifiable Benchmark for Defeasible Abduction in Foundation Models
作者: Patrick Cooper, Alvaro Velasquez
分类: cs.AI, cs.LG, cs.LO
发布日期: 2026-06-17
备注: 33 pages, 14 figures, 23 tables. Dataset: https://huggingface.co/datasets/PatrickAllenCooper/DeFAb ; code and evaluation harness: https://github.com/PatrickAllenCooper/blanc
🔗 代码/项目: HUGGINGFACE
💡 一句话要点
提出DeFAb基准以解决可否定推理的评估问题
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 可否定推理 逻辑求解 知识图谱 自然语言处理 人工智能评估
📋 核心要点
- 现有的前沿语言模型在可否定推理任务中的表现不尽如人意，准确率低且不稳定。
- 论文提出DeFAb基准，通过将公共知识库转化为可否定推理实例，结合严格的逻辑验证，提升推理的严谨性。
- 实验结果显示，基于规则的逻辑求解器在准确率和速度上远超前沿语言模型，提供了新的评估标准。
📝 摘要（中文）
本论文介绍了DeFAb（可否定推理基准），这是一个数据集和生成管道，旨在将四十年来的公共知识库转化为形式化的可否定推理实例。通过引入严格的逻辑检查，DeFAb使得理论修订的严谨构建成为衡量创造力和理论推理的工具。实验结果显示，现有前沿语言模型在可否定推理任务中的表现远不如基于规则的逻辑求解器，后者在50微秒内以100%的准确率解决所有实例，而前沿模型的准确率最高仅为65%。
🔬 方法详解
问题定义：本论文旨在解决现有语言模型在可否定推理任务中的低准确率和不稳定性问题。现有方法在处理复杂推理时往往无法保持逻辑严谨性。
核心思路：论文提出DeFAb基准，通过将历史知识库转化为可否定推理实例，并引入严格的逻辑验证机制，确保每个假设都经过有效的推导检查。
技术框架：整体架构包括数据集生成管道和逻辑求解器。数据集生成管道结合了分类层次（如OpenCyc、YAGO、Wikidata）与行为属性图（如ConceptNet、UMLS），生成372,648个实例。逻辑求解器则负责验证推理的有效性。
关键创新：DeFAb基准的最大创新在于将可否定推理的逻辑严谨性与创造力评估结合，强调理论修订的严谨构建，而非流畅但破坏理论的表达。
关键设计：在设计中，采用了多层次的实例生成和多项式时间可验证的黄金标准，确保了推理的有效性和可靠性。
🖼️ 关键图片
📊 实验亮点
实验结果表明，基于规则的逻辑求解器在所有实例中以100%的准确率完成任务，而前沿语言模型在可否定推理任务中的表现最高仅为65%，在渲染稳健性评估下更是降至23.5%。这显示出DeFAb基准在推理任务评估中的重要性。
🎯 应用场景
DeFAb基准在人工智能推理、知识图谱构建和自然语言处理等领域具有广泛的应用潜力。通过提供一个严谨的评估标准，研究者可以更好地理解和改进模型在复杂推理任务中的表现，推动相关技术的发展和应用。
📄 摘要（原文）
A rule-based logic solver resolves every instance in our benchmark in under 50 microseconds with 100% accuracy; the best frontier language model reaches 65% at best and drops to 23.5% under rendering-robust evaluation (worst case over four surface renderings). We introduce DeFAb (Defeasible Abduction Benchmark), a dataset and generation pipeline that converts four decades of publicly funded knowledge bases into formally grounded instances for defeasible abduction: constructing hypotheses that explain anomalies by overriding defaults while preserving unrelated expectations. Because every hypothesis must pass polynomial-time checks for valid derivation, conservativity, and minimality, DeFAb makes logical rigor the instrument for measuring creativity and theoretical reasoning, scoring the disciplined construction of theory revisions rather than fluent but theory-destroying prose. The pipeline pairs taxonomic hierarchies (OpenCyc, YAGO, Wikidata) with behavioral property graphs (ConceptNet, UMLS) to produce 372,648+ instances across 33.75M materialized rules from 18 sources, in three levels with polynomial-time verifiable gold standards. Four frontier models do not reliably internalize defeasible reasoning: rendering-robust Level 2 accuracy is 7.8-23.5%; chain-of-thought variance (~36 pp) exceeds any inter-model gap; and a matched contamination control isolates a +19.4 pp Level 3 gap. We further release DeFAb-Hard (a 235-instance Level 3 difficulty variant; best model 53.3% vs 100% symbolic) and CONJURE (a kernel-verified transformative-creativity variant of 560 Lean 4/Mathlib instances whose gold answers are definitions the proof kernel did not previously contain, judge-free verifier; a pilot finds zero novel concepts). The same verifier doubles as an exact reward for preference optimization (DPO, RLVR/GRPO). Released under MIT at https://huggingface.co/datasets/PatrickAllenCooper/DeFAb.