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

基于规则的逻辑求解器以100%准确率在50微秒内解决我们基准的每个实例；最佳前沿语言模型最好达65%——在渲染鲁棒评估下降至23.5%（四种表面渲染的最坏值）。我们介绍DeFAb（可废止溯因基准）——把四十年公共资助知识库转为可废止溯因形式化锚定实例的数据集与生成管线：构造通过推翻默认值解释异常、同时保持无关期望的假设。因为每个假设必须通过有效推导、保守性与最小性的多项式时间检查——DeFAb使逻辑严谨成为度量创造力与理论推理的工具——为有纪律的理论修正构造打分——而非流畅但破坏理论的散文。该管线把分类层级（OpenCyc、YAGO、Wikidata）与行为属性图（ConceptNet、UMLS）配对——从18个来源、33.75M条物化规则产出372,648+实例——分三级、带多项式时间可验证金标准。四个前沿模型不能可靠内化可废止推理：渲染鲁棒的Level 2准确率为7.8-23.5%；思维链方差（约36pp）超过任何模型间差距；匹配的污染控制分离出+19.4pp的Level 3差距。我们进一步发布DeFAb-Hard（235实例Level 3难度变体；最佳模型53.3%对符号100%）与CONJURE（560个Lean 4/Mathlib实例的内核验证变革性创造力变体——其金答案是证明内核此前没有的定义；无裁判验证器；试点发现零个新概念）。同一验证器兼作偏好优化（DPO、RLVR/GRPO）的精确奖励。MIT许可发布于 https://huggingface.co/datasets/PatrickAllenCooper/DeFAb。