DeFAb：一种可验证的基准，用于基础模型中的可废止溯因推理
DeFAb是一个将四十年公共资助知识库转化为可废止溯因推理基准的数据集和生成管道。基于规则的逻辑求解器在50微秒内100%准确解决所有实例，而最佳前沿语言模型达到65%，在鲁棒渲染评估下降至23.5%。该基准通过多项式时间可验证的推导、保守性和最小性检查，将逻辑严谨性作为衡量创造力和理论推理的工具。发布了包含372,648+实例的DeFAb以及更难变体和Lean 4/Mathlib中创造性变体。
研究人员发布了一项名为DeFAb（Defeasible Abduction Benchmark）的新型基准测试，旨在评估基础模型在可废止溯因推理方面的能力。可废止溯因推理是一种高级推理形式，要求模型通过构建假设来解释异常现象，同时覆盖默认规则但保留无关的预期。DeFAb将四十年来的公共资助知识库转化为一个严格的形式化基准，确保每个假设都必须通过多项式时间可验证的推导、保守性和最小性检查。这使得逻辑严谨性成为衡量创造力和理论推理的尺度，鼓励理论修订的纪律性构建，而非流利但破坏理论的文本。
DeFAb的生成管道将分类层次结构（如OpenCyc、YAGO、Wikidata）与行为属性图（如ConceptNet、UMLS）相结合，从18个来源生成了超过33.75万条物化规则，最终产生372,648个实例，分为三个难度级别。每个实例都配有经多项式时间可验证的金标准，确保评估的可靠性。这一设计使得DeFAb不仅是一个基准，更是一个可验证的测试平台，能够精确衡量模型的逻辑推理能力。
实验结果显示，基于规则的逻辑求解器能够在50微秒内以100%的准确率解决所有实例，而最佳的前沿语言模型在标准评估下仅达到65%，在鲁棒渲染评估（考虑四种表面渲染的最坏情况）下更是降至23.5%。有四款前沿模型未能可靠地内化可废止推理：在鲁棒渲染下，它们的二级准确率仅在7.8%至23.5%之间；链式思维方差（约36个百分点）甚至超过了任何模型间的差距；而对污染控制的匹配实验显示，三级差距高达19.4个百分点。这些结果凸显了当前语言模型在严谨逻辑推理上的根本缺陷。
除了DeFAb本身，研究团队还发布了DeFAb-Hard，这是一个包含235个实例的三级难度变体，最佳模型仅达到53.3%的准确率，而符号求解器则保持100%。同时推出的还有CONJURE，一个基于Lean 4/Mathlib的核验证创造性推理变体，包含560个实例，其金标准是证明核此前未包含的定义，并通过无评判验证器进行验证。初步实验并未发现新颖概念，这进一步表明当前模型在创造性推理上的局限。
值得注意的是，DeFAb的验证器还可直接用作偏好优化（如DPO、RLVR/GRPO）的精确奖励，为模型训练提供了新的工具。DeFAb已在MIT许可下发布，可通过Hugging Face获取，这为AI研究社区提供了一个评估和改进模型推理能力的宝贵资源。