ABD：有限一阶世界中的默认异常溯因

本文介绍了 ABD，一个针对有限一阶世界进行默认 - 异常溯因的基准测试。给定包含异常谓词的背景理论和一组关系结构，模型需输出定义异常的一阶公式，在保持异常稀疏的同时恢复可满足性。我们形式化了三种观察机制（封闭世界、存在补全、全称补全），并通过精确的 SMT 进行验证。对十个前沿大语言模型在 600 个实例上的评估显示，最佳模型虽实现了高有效性，但在简约性上仍有差距，且留样评估揭示了不同机制下独特的泛化失败模式。