ABD：有限一阶世界中的默认例外溯因

我们提出ABD，一个面向有限一阶世界默认例外溯因的基准。给定含反常谓词的背景理论与一组关系结构，模型须输出一个定义例外的一阶公式，在保持例外稀疏的前提下恢复可满足性。我们以精确SMT验证形式化了三种观察情形（封闭世界、存在完备化、全称完备化）。在600个实例上评估十个前沿LLM：最佳模型有效性强但简洁性仍有差距，留出评估揭示了各情形间不同的泛化失败模式。