@s_batzoglou
Our paper “ABD: Default–Exception Abduction in Finite First-Order Worlds” was accepted to KR 2026, in the KR Meets Machine Learning and Explanation track. arXiv: https://t.co/HYb5icwsel code/data: https://t.co/ZXXqzouuni A very nice plain-language summary: https://t.co/Zl5lHu4EGH Motivation: many reasoning benchmarks ask whether a model gets an answer right, but give only a weak view of *why* it succeeds or fails. In ABD, the model has to synthesize an explicit first-order formula explaining the exceptions to a default rule. A typical task is not: “classify this object.” It is: given a background first-order theory, and several finite relational worlds, output one formula α(x) that defines when an object is abnormal (i.e., does not satisfy the background theory), while keeping the exception set sparse. That gives us three things that are hard to get from many natural-language benchmarks: 1. exact semantic checking; 2. an explicit hypothesis produced by the model; 3. a cost measure, so we can distinguish “valid but bloated” explanations from compact ones. The benchmark has three observation regimes: • Full / closed-world: the observed facts are complete. • Partial / existential completion: unknowns may be completed favorably. • Skeptical / universal completion: the explanation must work under all completions. So the same high-level task can be tested under increasingly demanding assumptions about incomplete information. A central design choice is that each instance contains multiple prompt worlds. The model must output one shared α(x) that works across all of them jointly. This is meant to test rule synthesis, not per-world labeling. We also evaluate on matched holdout worlds. This lets us separate two failure modes: formulas that stop being valid on fresh worlds, and formulas that remain valid but become too expensive i.e., call too many objects "abnormal". Empirically, evaluating ten frontier LLMs on 600 instances, the best models often achieve high validity, but parsimony remains a real issue. Many hypotheses repair the theory but use unnecessarily broad exception definitions. Holdout evaluation also shows distinct generalization failures across the three observation regimes. ABD aims to test one specific type of reasoning, formulating simple rules (first-order formulas) that explain exceptions to a given background theory. Finite first-order worlds give us a clean testbed for doing so, by being explicitly solvable and feasible for generating problems automatically. I hope it is useful both for evaluating language models and for comparing them with more symbolic or solver-aided synthesis methods.
