Deogen: Automatic Benchmark Generation for Reasoning over Policies

What it claims

DeoGen generated 451,047 deontic-reasoning entries from four real policy documents: 263,795 with a definite verdict and 187,252 "not enough information" (NEI) entries. The policies are IRS Code §§105(b), 125, 129, 152 and 213; an American Fidelity (AFL) cafeteria plan document; an AFL certificate of coverage; and a Yale hiring fellows policy. A 1,639-entry sample (850 definite, 789 NEI) was run on Claude Sonnet 5, GPT-5.5, Qwen3.6 and Gemma 4. Across all four models, definite-verdict accuracy spans 75.1–92.5%, and NEI accuracy spans 4.0–40.0%. The 89–92% and 22–40% figures in the summary are the frontier models only. The authors frame the NEI failure as logical underdetermination: the full policy is in context, but the facts do not entail a verdict. They distinguish this from epistemic gaps.

How it works

1. Each policy clause is formalized as quantifier-free SMT-LIB, tagged with its source text and section label (e.g. §129(c)(1)).
2. For a chosen verdict atom, Z3 enumerates all assignments consistent with the policy. A tree is built top-down, greedily picking the variable that minimizes estimated subtree depth. Variables that cannot change the verdict are pruned.
3. Derived conditions are expanded into subtrees, such as the AFL plan deferring to IRS §213(d)(10) for long-term-care premiums. Numeric variables are split into regions at the policy's thresholds, with one representative value per region. Linked numerics such as ppy = 65 - taxpayerAge are enumerated jointly.
4. Every path is certified with Z3 before release. Paths that fail the check are dropped.

flowchart TD
  P[Tree path facts] --> L{Ends at leaf?}
  L -- yes --> D{Consistent and entails label?}
  L -- no --> N{Two verdict values satisfiable?}
  D -- yes --> R[Release definite entry]
  N -- yes --> R2[Release NEI entry]
  D -- no --> X[Drop]
  N -- no --> X

Certification catches two failure modes the authors observed. The first is inconsistent facts, where §152(c) and §152(d) subtrees call the same person a child and a sibling. The second is unentailed labels, where the Yale policy allows three appointment types but the tree recorded one.

Generation is parametric through three controls. Fact count sets how many facts a model must integrate. Cut depth sets how much an NEI entry withholds, from most of the determination down to a single fact. A path "signature", the set of variables asked, defines a structural class. Keeping at most k entries per class yields structurally distinct sets.

Evidence

Tree depth and entry counts vary widely by determination. AFL §8.04 eligible medical expense has depth 44 and 163,870 definite entries. IRS §213(a) deductibility has depth 40 and 59,922 definite entries. Yale appointment type has depth 5 and only 8 definite plus 5 NEI entries. Formalization sizes range from 11 assertions (Yale, 2,828 words) to 1,190 assertions (AFL certificate, 15,051 words). The evaluation drew up to 100 definite and 100 NEI entries per determination, over twelve determinations. Each entry carries section labels, so model citations can be checked. Per-model scores are not in the fetched text.

Limits

The autoformalizer used is a proprietary policy-to-SMT translator, and each specification was also reviewed by hand. Only the steps after formalization are automatic. A new policy needs its own reviewed SMT. Numeric coverage is one representative value per threshold region, not a sweep of values. The evaluation covers 1,639 of 451,047 entries. The fetched text is cut off before the results section and does not state a code, data or licence release.