Source-linked AI summary
Deogen: Automatic Benchmark Generation for Reasoning over Policies
Sam Kouteili, William Liang, Keeran Murray, Adriana Zhou, Ramesh Viswanathan, Scott Shapiro, Ruzica Piskac
TL;DR
Existing deontic-reasoning benchmarks are largely hand-crafted, making new entries difficult to scale and verify. DeoGen autoformalizes policies and turns decision-tree paths into labeled benchmark cases, including cases that test abstention. Across its evaluation sample, models were substantially less accurate when facts did not entail a verdict.
Problem
Existing deontic-reasoning benchmarks are typically hand-crafted or aggregated, limiting scalable generation and making construction and correctness difficult to verify.
Source: §1 · p. 1Method
Results
Across 1,639 sampled entries, models achieved 75.1–92.5% correctness on determined verdicts, compared with 4.0–40.0% on NEI cases.
Source: §1 · p. 2Takeaways & Limitations
DeoGen generated 451,047 entries across four policies, while evaluation exposed a substantial gap in model performance on logically underdetermined cases.
Source: §1 · p. 2, §7 · p. 7The generation uses a closed-world setting and does not prohibit improbable but logically permissible scenarios or add unstated normative assumptions.
Source: §5 · pp. 6–7
Abstract
from arXiv · showhide
Language models are increasingly being deployed in regulated settings, where a model must apply given rules to the facts of a situation to determine a verdict. Benchmarking this capability, known as deontic reasoning, remains a costly and manual process, with existing datasets largely hand-crafted. In this paper, we present DeoGen, a scalable, automatic, and parametrizable benchmark generator for deontic reasoning. By autoformalizing policy rules to first-order logic, we can construct decision trees that capture possible outcome trajectories. Each path down a tree becomes a benchmark entry, with each tree producing combinatorially many entries relative to tree depth. Paths ending at a leaf entail a verdict, while non-leaf paths measure a model's ability to abstain when presented with insufficient information. Evaluations show frontier models return the correct verdict 89-92% of the time. Notably, performance degrades (22-40% correct) on entries without sufficient information to claim a verdict, even with explicit instructions to abstain in such cases. In all, DeoGen presents an automatic, scalable, and parametric method for generating deontic reasoning benchmarks.
1 Introduction
Deontic reasoning asks models to apply rules to facts, but existing benchmarks are largely hand-crafted and difficult to scale or verify. DeoGen uses autoformalized policies and decision-tree paths to generate labeled scenarios, including cases where models should abstain.
1 Introduction
- LLM errors in regulated settings such as financial compliance, insurance, and pharmaceuticals can have high-stakes consequences.The introduction cites fabricated clinical details in hospital transcription as an example of hallucination-related harm.Source: §1 · p. 1
- Deontic reasoning applies rules to factual situations to determine whether an action or outcome complies with governing norms.It concerns normative concepts including obligations, permissions, and prohibitions.Source: §1 · p. 1
- Existing hand-crafted or case-aggregated benchmarks can saturate and are difficult to construct and verify accurately.Human annotation is costly and error-prone, while generated samples can contain incorrect labels or logical inconsistencies.Source: §1 · p. 1
- DeoGen autoformalizes natural-language policies so it can enumerate fact scenarios and formally deduce their verdict labels.The formalized rules are used to construct decision trees.Source: §1 · p. 1
- Leaf-reaching paths entail verdicts, while shorter paths can leave authorization undetermined and test whether a model abstains.DeoGen generates new entries by selecting paths; path counts grow combinatorially with tree depth, and depth and path diversity can be controlled.Source: §1 · p. 2
- 75.1–92.5% correctness on determined verdicts fell to 4.0–40.0% on abstention cases across 1,639 sampled entries from 451,047 generated across four policies.The finding isolates logical underdetermination: the policy is fully in context, but the facts do not entail a verdict.Source: §1 · p. 2
2 Preliminaries
The preliminaries formalize policies and facts with logic, then define verdicts through entailment. Policy decision trees connect paths through policy conditions to determined verdicts or insufficient-information cases.
2.1 Boolean Satisfiability
- Boolean satisfiability asks whether some assignment makes a formula true; SMT extends this to theory constraints such as integer arithmetic.The paper writes formulas in SMT-LIB and checks them with Z3.Source: §2.1 · p. 2
2.2 Deontic Reasoning as Entailment
- A policy is a finite set of formulas, and a fact pattern is a consistent set of facts over the policy atoms; entailment determines Yes, No, or NEI.NEI occurs when relevant clauses remain undetermined, and such entries test a model’s ability to abstain.Source: §2.2 · p. 2
2.3 Policy Decision Trees
- A policy decision tree branches on policy conditions, with each leaf labeled Yes or No.Soundness requires each root-to-leaf path to entail its label; reducedness requires each non-leaf path to yield NEI.Source: §2.3 · pp. 2–3
3 Methodology
DeoGen formalizes policies as SMT formulas, compiles them into decision trees, and certifies and renders tree paths as benchmark entries. It also supports parameterized selection of entries by their structural properties.
3 Methodology
- The pipeline formalizes a policy as SMT formulas, compiles them into a policy decision tree, then certifies and renders each path as a benchmark entry.In the experiments, a proprietary translator produced the SMT specifications, which were reviewed by hand; downstream processing was automatic after confirmation.Source: §3 · p. 3, §3.1 · p. 3
3.1 Autoformalizing Policies
- The input formalization must link each clause to its source-text fragment and section label, preserving provenance for generated entries.The autoformalizer creates the SMT representation, with hand review in the experiments.Source: §3.1 · p. 3
3.2 Compiling Policy Decision Trees
- Z3 enumerates assignments consistent with the policy, and a top-down tree branches on variables chosen to reduce estimated depth while pruning variables that cannot change the verdict.Numeric domains are partitioned by policy thresholds; related numeric variables are enumerated jointly, and derived conditions expand into subtrees.Source: §3.2 · p. 3
3.3 Generating Benchmark Entries
- Before release, each path is checked for consistent facts and an entailed label; NEI entries require at least two distinct verdict values to remain satisfiable.Certification addresses inconsistent combinations from independently compiled subtrees and paths whose facts allow multiple outcomes.Source: §3.3 · p. 3
3.4 Parametric Selection
- Entries are annotated by fact count, cut depth, and signature, allowing selection by information withheld and by the structural uniqueness of question sets.Keeping at most k entries per signature class yields structurally distinct benchmark sets.Source: §3.4 · p. 4
4 Experimental Setup
DeoGen was evaluated on four policy sources, with benchmark entries drawn from certified definite and underdetermined populations. The setup samples across fact-count buckets, limits repeated question signatures on large trees, and grades verdict accuracy and provision citations where labels are available.
4 Experimental Setup
- The four sources cover IRS cafeteria-benefit provisions, an American Fidelity cafeteria plan and coverage certificate, and Yale’s hiring policy.The IRS provisions chain across sections, and the AFL plan incorporates IRS sections by reference; Yale verdicts can be appointment types rather than yes/no answers.Source: §4 · p. 4
- 263,795 definite and 187,252 underdetermined entries remained after certification, with inconsistent plan-document classes and ambiguous Fellows paths pruned.The plan-document medical-expense tree lost 31,460 question-set/verdict classes; three Fellows leaf paths entailing multiple appointment types were also removed.Source: §4 · p. 4
- Evaluation samples up to 100 entries per population across four shown-fact-count buckets, using the full certified population when smaller.For large trees, at most one entry per question-signature class is retained; on the health-FSA tree, this removes 66% of certified paths.Source: §4 · pp. 4–5
- Models select among admissible verdicts, including “Not enough information”; accuracy is reported for definite and underdetermined scenarios by policy and overall.The two-proportion tests found every definite–NEI gap significant at p<0.001; the Gemma 4 31B–Claude definite-accuracy gap was not.Source: §4 · p. 5, Table 2 · p. 5
- Provision-citation recall is graded against touched-section labels for IRS and plan-document entries, with ancestor citations receiving half credit and precision also reported.The certificate and hiring policies lack internal section labels, so citation grading covers only the first two policies.Source: §4 · p. 5
- Autoformalizations received 33 manually added bridge assertions linking IRS and AFL variables that policy clauses assumed to be connected.These bridges address clauses that were individually logical but marginally disjoint, such as provisions concerning an individual’s abode.Source: §4 · p. 5
5 Evaluation
Across five models evaluated on 1,639 entries, definite-verdict accuracy was substantially higher than accuracy on underdetermined cases requiring abstention. Accuracy also fell on longer paths and atypical-age scenarios, while few-shot examples improved abstention only partially.
Evaluation results
- Definite-case accuracy ranged from 75.1% to 92.5%, while underdetermined-case accuracy ranged from 4.0% to 40.0%.GPT-5.5 was the strongest abstainer at 40.0%; open-weight Gemma 4 31B led definite cases at 92.5%.Source: §5 · p. 5
Accuracy by fact count
- Performance generally declined as fact chains lengthened, with a more pronounced decrease for NEI verdicts.In sampled traces, models sometimes identified unaddressed conditions but treated them as satisfied by default.Source: §5 · p. 5, Figure 3 · p. 5
Citation grounding
- Models’ citations were usually relevant (precision 0.82–0.94), but the best model cited fewer than a third of the provisions its verdict depended on (recall 0.293).Claude Sonnet 5 had the highest reported recall; Gemma 4 E4B had recall 0.162.Source: §5 · p. 6, Table 3 · p. 6
Few-shot prompting
- Few-shot examples raised NEI accuracy by 10–13 points for three models, with no significant change in definite-verdict accuracy.The best few-shot abstainer still missed about half of its NEI entries.Source: Table 4 · p. 6, §5 · p. 6
Human evaluation
- Two non-expert human annotators achieved 32% accuracy, with 52% inter-annotator agreement.They cited unfamiliarity with legal code and source policy as the main accuracy bottlenecks.Source: §5 · p. 6, Table 5 · p. 7
Atypical-age scenarios
- Across all models, atypical-age scenarios reduced accuracy by 2.3–17.1 percentage points relative to typical-age scenarios.Atypical cases made up 15% of age-related IRS and AFL entries; the authors posit that normative world assumptions contribute to the decrease.Source: §5 · p. 7, Figure 5 · p. 7
6 Related Work
Prior work applies logic to legal texts and benchmarks rule-based reasoning, while autoformalization has expanded beyond translation to roles in LLM checking and training. DeoGen differs from fixed, manually drawn benchmarks by automatically formalizing policies.
Law and logic
- Legal logic systems hand-write rules, making correctness provable but coverage limited to manually encoded content; DeoGen autoformalizes policies to reduce that labor.Source: §6 · p. 7
Deontic Reasoning Benchmarks
- Existing deontic reasoning benchmarks span varied domains, but each remains fixed and manually drawn.Source: §6 · p. 7
Autoformalization
- Autoformalization translates natural language into formal representations and also serves as a checker at test time and a reward oracle during training.Source: §6 · p. 7
7 Conclusion
DeoGen compiles autoformalized policies into decision trees and certifies paths to generate determined and abstention-testing entries. Across four rule sets, models performed substantially worse on NEI verdicts than on determined verdicts.
7 Conclusion
- 75.1–92.5% average correctness on determined verdicts fell to 4.0–40.0% on NEI verdicts across 1,639 sampled entries.Source: §7 · p. 7
- DeoGen compiles autoformalized policies into decision trees, certifies paths for consistency and entailment, and turns them into benchmark entries.Paths to leaves derive determined entries, while paths to internal nodes test abstention because they do not explicitly entail a verdict.Source: §7 · p. 7
- Across four rule sets, DeoGen generated 263,795 definite entries and 187,252 NEI entries, with support for integer datatypes and intra-policy dependence.Source: §7 · p. 7