ABD: Default Exception Abduction in Finite First Order Worlds

This paper introduces ABD, a benchmark for default-exception abduction in finite first-order worlds that evaluates ten frontier LLMs on their ability to generate sparse, satisfiability-restoring formulas across three observation regimes, revealing that while models achieve high validity, they struggle with parsimony and exhibit distinct generalization failures.

The Gist

Imagine you are a detective trying to solve a mystery, but the rules of the world you are investigating are slightly broken.

The Core Idea: "The Rulebook with Exceptions"

Think of a Default Theory as a rulebook for a game.

• The Rule: "If a player has a red card, they must sit down."
• The Reality: You walk into the room and see a player with a red card who is standing up.

The rulebook is violated. In the world of logic and AI, this is a problem. The AI needs to figure out why the rule didn't work. Was the rule wrong? No, usually the rule is right, but there's a special case. Maybe that player is the referee, or maybe they have a broken leg.

This process of inventing a reason for the exception is called Abduction. The AI's job is to write a new, tiny rule that says: "The 'sit down' rule applies to everyone EXCEPT people who are referees."

The paper introduces a new test called ABD (Default–Exception Abduction) to see how good modern AI (like the smartest chatbots) are at writing these "exception rules."

The Three Levels of the Test

The researchers created three different ways to play this detective game, representing how much information the AI has:

1. ABD-Full (The Clear Window):

   • Scenario: You can see everything in the room perfectly. You know exactly who has red cards, who is standing, and who is sitting.
   • The Challenge: Find the exception rule that explains the standing red-card player.
   • The Trap: The AI might try to say, "The exception is only for this specific person named 'Bob'." That's a bad rule because it doesn't work if a new person named "Alice" shows up later. The AI needs a general rule (like "Referees").

2. ABD-Partial (The Foggy Window):

   • Scenario: You can see most things, but some details are hidden in fog. You see a player with a red card standing, but you can't see if they are holding a whistle (which would make them a referee).
   • The Challenge: The AI must guess a rule that works if the fog clears in a helpful way. "Maybe they are a referee? If so, the rule holds."
   • The Trap: The AI might get too lucky, assuming the fog will clear in the most convenient way possible, rather than preparing for a bad outcome.

3. ABD-Skeptical (The Paranoid Window):

   • Scenario: Same foggy window, but now the AI must be a paranoid detective.
   • The Challenge: The AI must write a rule that works no matter how the fog clears. Even if the hidden fact turns out to be the worst possible scenario, the rule must still make sense.
   • The Trap: This is the hardest level. The AI often fails by writing a rule that works for the "best case" but collapses when the "worst case" happens.

The "Gotcha" Metrics: Validity vs. Parsimony

The paper doesn't just ask, "Did the AI get the answer right?" (Validity). It asks two harder questions:

1. Is the rule too complicated? (Parsimony)

   • Imagine the AI says: "The exception applies to anyone who is a referee, OR has a red card, OR is wearing a blue hat, OR was born on a Tuesday, OR..."
   • This is technically "valid" (it explains the exception), but it's a terrible, bloated rule.
   • The researchers measure how "bloated" the AI's rule is. They want the AI to find the simplest explanation (Occam's Razor).

2. Does the rule break on new cases? (Generalization)

   • The AI is trained on 10 rooms, then tested on 5 new rooms it has never seen.
   • The Big Finding: Many AIs are great at memorizing the 10 training rooms. They write complex, specific rules that work perfectly for the training data. But when they walk into a new room, their rules fall apart. They are "brittle."

The Results: Who Passed the Test?

The researchers tested 11 of the smartest AI models available. Here is the summary in plain English:

• The "Over-Thinkers" (e.g., GPT-5.4): These models are very good at finding the simplest mathematically correct answer (lowest cost). However, they do it by writing massive, complex rules that look like a maze. When they face a new room, their complex rules often break. They are smart but fragile.
• The "Steady Detectives" (e.g., Opus-4.6, Gemini-3.1): These models write slightly more expensive rules (they mark a few extra people as "exceptions" than strictly necessary), but their rules are simple and robust. They work well on the training data and the new test data. They are the most reliable.
• The "Brittle Ones": Many models failed the "Skeptical" test completely. They wrote rules that worked perfectly for the training data but failed immediately when the hidden facts turned out to be "bad."

The Big Takeaway

This paper shows that being "smart" isn't just about getting the right answer.

In the real world, we don't want AI that writes a 100-page rulebook just to explain why one person is standing up. We want AI that writes a simple, one-sentence rule ("Referees stand up") that works even when the situation changes slightly.

The current generation of AI is getting better at logic, but it still struggles to be simple, robust, and generalizable all at the same time. It tends to either be too simple (and wrong) or too complex (and brittle). The "sweet spot" of a simple, perfect rule is still very hard for machines to find.

Technical Summary

Here is a detailed technical summary of the paper "ABD: Default–Exception Abduction in Finite First-Order Worlds."

1. Problem Definition

The paper addresses the challenge of Default–Exception Abduction in the context of Knowledge Representation (KR). In many domains, rules hold "normally" but admit rare exceptions (e.g., "Birds fly, unless they are penguins"). The task is to infer a compact, first-order logical definition of an abnormality predicate ($Ab(x)$) that explains why a fixed background theory ($\Theta$) is violated by observed data.

• Input: A set of finite relational structures ("worlds") containing observed facts and a fixed first-order theory $\Theta$ that uses an abnormality predicate $Ab$ to block default rules (e.g., $\forall x (\phi(x) \land \neg Ab(x)) \to \psi(x)$).
• Output: A first-order formula $\alpha(x)$ such that defining $Ab(x) \leftrightarrow \alpha(x)$ restores the satisfiability of the theory across all provided worlds.
• Objective: The solution must be valid (satisfy the theory in all worlds) and parsimonious (minimize the number of elements marked as abnormal).
• Key Challenge: Unlike standard supervised learning, the model must synthesize a generalizable rule that balances consistency with the theory and sparsity of exceptions, without being given a labeled target.

2. Methodology: The ABD Benchmark Suite

The authors introduce ABD, a benchmark suite designed to evaluate Large Language Models (LLMs) on this task using exact, solver-based verification.

A. Three Observation Regimes

The benchmark formalizes three distinct scenarios regarding how missing information is handled:

1. ABD-Full (Closed-World): All facts are observed. Validity requires the repaired theory to be satisfiable in the given world.
2. ABD-Partial (Existential Completion): Some facts are unknown. A hypothesis is valid if there exists at least one completion of the unknown atoms that makes the theory satisfiable. Cost is measured in the best-case scenario.
3. ABD-Skeptical (Universal Completion): Unknown facts are treated conservatively. A hypothesis is valid only if the theory is satisfiable under every possible completion of unknown atoms. Cost is measured in the worst-case scenario.

B. Evaluation Metrics

To move beyond binary "right/wrong" judgments, the paper introduces:

• Validity: Does the formula satisfy the theory?
• Parsimony Gap: The difference between the model's abnormality count and a solver-computed lower bound (where $Ab$ is allowed to vary freely per world, not constrained to a single formula).
• AST Size: The complexity of the generated formula (Abstract Syntax Tree size) to penalize degenerate "case-splitting" solutions.
• Holdout Generalization: Performance on unseen worlds generated from the same distribution but without adversarial filtering.

C. Dataset Generation

• Controlled Difficulty: Instances are generated using a CEGIS-like (Counterexample-Guided Inductive Synthesis) loop. The system iteratively adds "adversarial" worlds to eliminate simple shortcut hypotheses (e.g., trivial formulas that happen to work on a small set) until only the intended relational structure remains.
• Gold Rules: Each instance has a "planted" gold rule, but models are allowed to find alternative valid rules with lower costs.
• Scale: 600 instances across 7 default theories, evaluated on 11 frontier LLMs.

3. Key Contributions

1. Formalization of Abduction Tasks: The first benchmark to formalize default-exception abduction over finite first-order worlds with three distinct completion semantics (Full, Partial, Skeptical).
2. Solver-Checkable Verification: Unlike NLP benchmarks that rely on natural language ambiguity, ABD uses SMT solvers (Z3) for exact verification of validity and cost, enabling precise error analysis.
3. Multi-Objective Evaluation: Introduces a nuanced evaluation framework that separates validity, parsimony (cost gap), and syntactic compactness (AST size), revealing trade-offs often hidden by binary metrics.
4. Comprehensive LLM Analysis: Provides the first large-scale evaluation of frontier models (including GPT-5, Opus, Gemini, Grok, etc.) on symbolic relational reasoning with explicit exception handling.

4. Key Results & Findings

The evaluation of 11 models reveals distinct performance profiles and failure modes:

• Validity vs. Parsimony Trade-off:

  • High-Validity Cluster: Models like Opus-4.6, Gemini-3.1, DSR, and Grok4.1f achieve >90% validity with compact formulas (AST ~11–15). However, they still exhibit a parsimony gap of ~1.0–1.6 extra exceptions per world compared to the solver lower bound.
  • The GPT-5.4 Outlier: GPT-5.4 achieves the lowest cost gaps (best parsimony) but at the expense of validity (lower than high-validity models) and compactness (massive formulas, AST ~66). It often uses brittle, over-fitted case-splits to minimize cost on training data.

• Generalization Failure Modes:

  • ABD-Full / ABD-Partial: The primary failure is Parsimony Inflation. Models find rules that work on training data but require significantly more exceptions (higher cost) on holdout worlds (gaps roughly double).
  • ABD-Skeptical: The primary failure is Validity Brittleness. Rules that satisfy the universal-completion constraint on training worlds often fail completely on holdout worlds. Interestingly, models that do survive holdout in this regime show smaller cost inflation, suggesting the universal constraint acts as a regularizer.

• Formula Complexity:

  • There is a strong correlation between formula size and generalization. Longer-than-gold formulas (AST > gold) achieve lower training cost gaps but suffer from catastrophic holdout validity drops (28% vs. 85% for shorter formulas).
  • Moderate-size formulas (AST in the low teens) offer the best trade-off between cost and robustness.

• Theory Sensitivity: Performance varies significantly based on the complexity of the background theory (e.g., theories with nested quantifiers or universal consequents are harder and show larger generalization gaps).

5. Significance

• Beyond Natural Language: ABD demonstrates that even state-of-the-art LLMs struggle with genuine first-order relational reasoning when forced to balance consistency, sparsity, and generalization without natural language priors.
• Diagnostic Tool: The benchmark serves as a diagnostic for "shortcut learning." It reveals that models often learn training-specific patterns (brittle case-splits) rather than portable exception rules.
• Future Directions: The paper suggests that improving abductive reasoning requires optimizing for a multi-objective profile (validity + parsimony + compactness) and potentially using solver-in-the-loop refinement to guide models toward robust, generalizable rules.

In conclusion, ABD establishes that while frontier models can often produce syntactically valid repairs, they currently lack the ability to consistently synthesize compact, sparse, and generalizable exception rules in finite first-order worlds, particularly under skeptical (worst-case) reasoning regimes.