构建可验证的假说推理基准，检验大模型在异常解释中的逻辑严谨性。
DeFAb: A Verifiable Benchmark for Defeasible Abduction in Foundation Models
- 将知识库转化为形式化假说生成任务，要求假设满足多项式时间可验证的逻辑约束。
- 顶尖大模型在鲁棒评估下准确率仅23.5%，远低于符号系统100%准确。
- 适用于评估模型理论推理与创造性修订能力，尤其适合研究逻辑与可信AI的学者。
我们提出DeFAb（可反驳假说基准），一个将四十年公共资助知识库转化为形式化假说生成实例的数据集与生成流程。该任务要求通过覆盖默认规则但保留无关预期的方式，构造解释异常的假设。每个假设必须通过多项式时间可验证的推导、保守性与极小性检查，使逻辑严谨性成为衡量创造力与理论推理的核心指标。管道结合分类层级（OpenCyc, YAGO, Wikidata）与行为属性图（ConceptNet, UMLS），生成超过37万例实例，涵盖3375万条显式规则，来自18个数据源，分三个层级并提供多项式时间可验证的黄金标准。四个前沿语言模型无法可靠内化可反驳推理：鲁棒评估下二级准确率为7.8%-23.5%；思维链方差达约36个百分点，超过任意两模型间差距；匹配污染对照实验揭示三级任务存在+19.4个百分点差距。我们进一步发布DeFAb-Hard（235个三级难度实例；最佳模型53.3%对比符号系统100%）和CONJURE（560个基于Lean 4/Mathlib的核验证转化型实例，其答案为证明核此前未包含的定义，无评判者验证；初步发现零新概念）。同一验证器亦可作为偏好优化的精确奖励（如DPO、RLVR/GRPO）。项目已开源，地址：https://huggingface.co/datasets/PatrickAllenCooper/DeFAb。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。