Why Scenario-Based Reasoning Beats Predicate Abstraction for LLMs

Modern LLM-assisted development demands verification techniques that scale with complexity and align with how LLMs actually reason.
This page explains why a scenario-based, reachability-aware approach is fundamentally better suited than classical predicate abstraction, especially for large, complex systems.

1. Predicate abstraction fights the LLM's inductive bias

Predicate abstraction assumes the hardest step is:

Inventing the right predicates.

That assumption breaks down precisely where LLMs struggle most.

Predicates are:

  • Low-level
  • Non-local
  • Brittle under refactoring
  • Semantically opaque in isolation

Choosing the right predicate set is a combinatorial problem with little semantic guidance.
Errors often surface only indirectly as spurious counterexamples, far removed from intent.

LLMs do not reason natively in Boolean lattices.
They reason in:

  • Intent
  • Constraints
  • Causal structure
  • Narrative explanations

A scenario-based approach matches that inductive bias.

2. Scenarios are semantic units; predicates are encoding units

This distinction is fundamental.

Predicate abstraction

  • Unit of reasoning: Boolean predicates
  • Meaning emerges only from global interaction
  • One missing predicate can invalidate the entire abstraction
  • Refinement signal is negative:

    This abstraction was insufficient.

Scenario-based reasoning

  • Unit of reasoning: Structured scenarios
  • Each scenario encodes:
    • Intent
    • Preconditions
    • Postconditions
    • Scope
  • Refinement signal is positive:

    This concrete behavior is missing or inconsistent.

LLMs thrive on positive, structured refinement signals.

3. Complexity amplifies the difference

Predicate abstraction complexity grows roughly exponentially in the number of predicates, i.e. O(2^|Predicates|).

But predicate selection complexity grows even faster:

  • Predicates interact non-locally
  • Hidden state aliases invalidate assumptions
  • Predicates go stale as systems evolve

In complex systems (concurrency, partial observability, layered invariants, long causal chains), LLMs are forced to hallucinate global Boolean structure from local text.

Scenario-based reasoning avoids this failure mode.

4. Scenario complements give LLMs actionable feedback

Predicate abstraction provides feedback like:

This counterexample is spurious; refine the abstraction.

That is nearly unusable for LLMs.

Scenario-based reasoning instead produces:

  • Reachable region complements
  • Stable fingerprints
  • Semantic gaps tied to intent

Example:

There exist reachable executions where:

  • order size exceeds maximum
  • market is open
  • risk flag is unset but no scenario covers this behavior.

This is feedback an LLM can act on.

5. Reachability makes the difference decisive

Reachability analysis strengthens both approaches, but unevenly.

Predicate abstraction

  • Reachability filters false positives
  • Still offers no guidance on which predicate to add

Scenario-based reasoning

  • Reachability filters the scenario complement
  • Leaves only real, unexplained behaviors
  • Gaps are already expressed in scenario form

The LLM receives:

  • Reachable
  • Meaningful
  • Minimal
  • Explainable targets

This is what enables scale.

6. LLMs reason in behaviors, not partitions

Predicate abstraction:

  • Partitions the state space
  • Meaning is implicit and emergent

Scenario-based reasoning:

  • Partitions behavioral intent
  • Meaning is explicit and inspectable

For LLMs:

  • Behaviors > states
  • Narratives > lattices
  • Examples > encodings

7. Compositional repair is the killer advantage

Predicate abstraction:

  • Refinement is global
  • Adding one predicate reshapes the entire abstraction

Scenario-based reasoning:

  • Scenarios compose
  • Adding one scenario does not invalidate others
  • Refinement is local and incremental

This mirrors how LLMs actually work:

  • Patch-based
  • Context-sensitive
  • Iterative

8. Why this matters for very complex systems

In large systems:

  • The right predicates are unknown upfront
  • Correctness is multi-dimensional
  • Human intent matters more than minimal encodings

Scenario-based reasoning:

  • Keeps LLMs at the intent level
  • Delegates combinatorics to the solver
  • Turns verification into a dialogue, not a guessing game

Predicate abstraction asks:

Guess the correct Boolean basis.

Scenario-based reasoning asks:

Explain every reachable behavior.

That difference determines scalability.

Summary

Predicate abstraction asks LLMs to invent low-level Boolean structure for global correctness, while scenario-based, reachability-aware reasoning lets LLMs operate on semantic behaviors and intent using automated reasoning to manage the combinatorial state space. This makes it dramatically more scalable for complex systems. Predicate abstraction compresses the problem for solvers; regions compress the problem for LLMs.

Positioning

This approach can be viewed as:

  • LLM-native CEGAR
  • Behavior-first formal verification
  • Intent-preserving abstraction refinement

It is not a replacement for predicate abstraction; it is a better interface between modern AI systems and formal reasoning engines.

Previous← Recommendations
NextGuides →