Underwriting Audit

Audit an underwriting ruleset against a catalog of required properties. For each property, the solver either proves it always holds or returns concrete counterexample applicants that break it.

---

Goals

Detect

Reasoning types

Prescriptive

Experience level

Advanced

Download ZIPView on GitHub

Browse files

• Directoryunderwriting_audit/

  • Directorydata/

    • age_buckets.csv
    • coverage_bands.csv
  • pyproject.toml
  • README.md
  • runbook.md
  • underwriting_audit.py

What this template is for

Insurance actuaries, regulatory-technology (RegTech) audit teams, and Model Risk Management (MRM) reviewers periodically check underwriting rulesets against the properties those rules are supposed to guarantee: no high-risk applicant is auto-approved, every frail applicant goes through manual review, no policy exceeds the regulatory ceiling without a second sign-off. Hand-checking even a few dozen rules against a property is impractical, and testing on a sample of applicants only catches the failures that happen to be in the sample. The dependable answer is verification: state the ruleset and the property as a constraint model and ask the solver whether any applicant at all can slip through. If one can, the solver hands back the concrete applicant that breaks the rule.

A real audit is a batch job across many properties at once, and the two sides are owned by different teams: the rule team owns the rule pack, and the compliance or MRM team owns the catalog of properties it must satisfy. This template mirrors that shape. It authors a property catalog separately from the ruleset, then runs one audit per property and produces a single report with a verdict for each — the rule holds (PASS), the rule is broken with example applicants shown (FAIL), or the audit could not decide (INCONCLUSIVE). The bundled ruleset carries a deliberate bug so the report comes back mixed rather than all-clear: the manual-review rule flags only seniors, while the frailty rule counts anyone senior or with a chronic condition, so chronic non-seniors slip past review. The mixed report is the point — a single run separates the properties the ruleset satisfies from the ones it violates. And rather than a single example per failure, the audit returns several distinct counterexamples so the reviewer can see the shape of the failure across ages, conditions, and coverage levels without probing by hand.

Reasoning approach: each property is audited with prescriptive reasoning — a constraint-satisfaction model whose counterexample is the logical negation of the property, solved in multi-solution mode so the solver returns several distinct applicants that break the rule (or proves none exist).

Who this is for

• Insurance actuaries and underwriting governance teams auditing rule libraries
• RegTech / compliance audit harnesses verifying property entailment over rule packs
• Model Risk Management (MRM) reviewers performing rule-level verification before promotion
• Operations researchers learning property-entailment audit as a constraint satisfaction problem (CSP)

What you’ll build

• A batch audit report — one verdict (PASS, FAIL, or INCONCLUSIVE) per property, printed as a verdict matrix, distinguishing the rules the ruleset satisfies from the ones it breaks.
• Witness tables for every failing property: several distinct counterexample applicants that break the rule, spread across ages, conditions, and coverage bands.
• A constraint model of the ruleset itself — the applicant’s attributes as free decisions and each rule as a derived indicator — built with prescriptive reasoning so a property is checked by asking the solver for any applicant that falsifies it.
• A separately-authored property catalog and a per-property audit routine, so adding a new property to check is a one-line change with no other code touched.

Built using prescriptive reasoning (constraint satisfaction with multi-solution enumeration on the MiniZinc solver).

What’s included

• underwriting_audit.py — main script with ontology, decisions, constraints, and solver call
• Runbook: runbook.md — a paste-testable walkthrough that reproduces the template step by step with the RAI skills; as important a reference as the script itself.
• data/age_buckets.csv — 4 representative ages (28, 45, 55, 72) — three under the 70 senior threshold, one above
• data/coverage_bands.csv — 4 coverage levels (250k, 1M)
• pyproject.toml — Python package configuration

Prerequisites

Access

• A Snowflake account that has the RAI Native App installed.
• A Snowflake user with permissions to access the RAI Native App.

Tools

• Python >= 3.10
• RelationalAI Python SDK (relationalai == 1.1.0)

Quickstart

1. Download ZIP:

   curl -O https://docs.relational.ai/templates/zips/v1/underwriting_audit.zip
   unzip underwriting_audit.zip
   cd underwriting_audit

   Tip

   You can also download the template ZIP using the “Download ZIP” button at the top of this page.

2. Create venv:

   python -m venv .venv
   source .venv/bin/activate
   python -m pip install --upgrade pip

3. Install:

   python -m pip install .

4. Configure:

   rai init

5. Run:

   python underwriting_audit.py

6. Expected output. The audit processes the three bundled properties in turn, printing each verdict with its witness table (for FAILs), then a verdict matrix at the end. A few representative lines confirm a successful run:

   ===== Auditing property: frail_implies_review =====
   Verdict: FAIL  (12 witness(es), status=OPTIMAL)
   ...
   Audit report (3 properties: 1 PASS, 2 FAIL, 0 INCONCLUSIVE)

   FAIL is the audit’s finding about the ruleset, not a template error; a PASS means the solver proved no counterexample exists. The full printout and a step-by-step walkthrough are in runbook.md.

Template structure

underwriting_audit/
├── README.md            # this file
├── runbook.md           # analyst paste-test walkthrough
├── pyproject.toml       # dependencies
├── underwriting_audit.py # main script (ontology, decisions, rule pack, property catalog, audit loop)
└── data/
    ├── age_buckets.csv    # representative applicant ages
    └── coverage_bands.csv # representative coverage levels

Start here: run python underwriting_audit.py for the full batch audit end to end, or follow runbook.md to reproduce it step by step with the RAI skills.

Sample data

The two small reference files describe the applicant space the audit searches over. They are the dimensions of an applicant, not a population of applicants — the solver picks values from them on every solution.

• data/age_buckets.csv — 4 representative ages (28, 45, 55, 72), three below the 70-year senior threshold and one above, with the columns id and age_years.
• data/coverage_bands.csv — 4 coverage levels (250k, 1M), with the columns id and coverage_dollars.

Both files need dense, contiguous id values (the audit checks this before solving), because the decision-variable bounds run from the minimum to the maximum id and the rules iterate over the reference rows in between.

Model overview

Rather than a table of applicants, the model has one applicant slot described by free decisions the solver fills in, plus derived indicators that encode each rule. Two reference concepts, AgeBucket and CoverageBand, supply the values the decisions can take.

• Key entities: AgeBucket and CoverageBand (reference rows loaded from CSV); the applicant is represented by scalar decisions rather than a concept.
• Primary identifiers: AgeBucket and CoverageBand are each identified by an integer id.
• Important invariants: reference ids are dense and contiguous; the free decisions age_bucket_id, has_chronic, and coverage_band_id select one reference row (or a binary flag); the rule indicators is_senior, is_frail, and is_manual_review are binaries pinned to those decisions by the rule pack.

For the full concept and property definitions, see underwriting_audit.py; runbook.md builds them step by step with the RAI skills.

How it works

The template factors the audit into three artifacts. A session factory constructs a fresh model for each audit — the concepts, the scalar decisions that describe an applicant, and the rule pack bundled together. A property catalog pairs each property’s name and description with a builder for its counterexample constraints. And a per-property audit routine owns one property’s full lifecycle: build the session, create the problem, attach the constraints, solve, classify the verdict, and read back the witnesses. The main script simply runs the routine over every property in the catalog and prints a verdict matrix at the end.

An applicant is described entirely by free decisions the solver fills in — which age bucket they fall into, whether they have a chronic condition, which coverage band they sit in — rather than by a row in an applicant table. On top of those, three rule indicators (is_senior, is_frail, is_manual_review) are also modeled as decisions, so the property check can compare them directly. The rule pack pins each indicator to a function of the free decisions: the senior indicator turns on when the chosen age bucket is at or above the senior threshold; the frailty indicator is the logical OR of senior-or-chronic, encoded as the standard three-constraint arithmetic for OR over binaries; and the manual-review indicator is pinned by the bundled — deliberately buggy — rule to the senior indicator alone, omitting the chronic arm that the audit is designed to expose.

Each property in the catalog is checked by asserting its logical negation and asking the solver for any applicant that satisfies it. If the solver finds one, the property is violated (FAIL) and the assignment is a concrete counterexample; if it proves none exists, the property holds (PASS); if it cannot decide within the time budget, the verdict is INCONCLUSIVE. Scoped properties add a data-filtered constraint to restrict the sub-population searched. Solving in multi-solution mode returns several distinct counterexamples per failure, each read back through the solver’s per-solution values so the reviewer sees the shape of the failure across ages, conditions, and coverage bands. A fresh model per audit keeps the per-model rule count bounded, which matters as the rule pack grows.

reference CSVs → free decisions + rule indicators → rule pack → per-property: assert negation → solve → PASS/FAIL/INCONCLUSIVE + witnesses → verdict matrix

See underwriting_audit.py for the implementation, and runbook.md to reproduce it step by step with the RAI skills.

Customize this template

Use your own data

• Replace data/age_buckets.csv and data/coverage_bands.csv with the reference dimensions of your own applicant space, keeping the id plus attribute columns and dense, contiguous ids.
• Adapt to a different regulated domain by editing the rule pack and the property catalog. The same shape carries to bank anti-money-laundering rules, healthcare prior-authorization, manufacturing segregation-of-duties, and SaaS retention — each is a set of binary indicators and a catalog of properties they must satisfy. Real rule packs in these domains often run to hundreds of rules; if a single audit’s rule count exceeds PyRel’s per-model "Rules created in a loop" threshold, decompose it into smaller property-scoped packs.

Tune parameters

• Raise MAX_WITNESSES to surface more counterexamples per failing property. Production audits typically want 50 to 500 witnesses per failure to cover the rule pack’s failure modes. Raising it past the size of the feasible set makes the solver exhaust every distinct case.
• The solve time cap is time_limit_sec (default 60) in the problem.solve("minizinc", ...) call inside run_audit(...).

Extend the model

• Add a property to the catalog by appending a (name, description, counterexample_builder) tuple to PROPERTIES. The builder takes the audit session and returns the property’s counterexample ICs — the logical negation of the property. For example, to audit “no senior is in the cheapest coverage band”, add ("no_senior_cheap_band", "no senior is in the cheapest coverage band", lambda s: [s.model.require(s.is_senior == 1), s.model.require(s.coverage_band_id == 1)]). run_audit picks it up automatically; no other code changes.
• Add a scoped property by adding a s.model.where(<data filter>).require(<decision constraint>) IC alongside the unconditional counterexample ICs. chronic_under_50_implies_review shows the pattern: the where iterates AgeBucket rows outside the scope (a pure data filter), and the require body forbids the applicant decision from picking those rows. PyRel rejects decision-variable expressions inside where, so the decision-variable constraint must live in require.
• Audit a corrected ruleset by changing the buggy rule inside _build_session(): the manual-review rule pins is_manual_review == is_senior; change the right-hand side to is_frail. With the fix in place, the failing verdicts in the bundled run turn to PASS and the verdict matrix reports 3 PASS, 0 FAIL.
• Add more rule indicators by introducing additional decisions and their defining ICs inside _build_session(), then appending them to rule_pack. A logical AND over binaries is encoded with the dual of the OR pattern used for is_frail.
• Switch from “any counterexample” to “worst counterexample” by adding a problem.minimize(...) over a violation-severity score with solution_limit=1, when triage capacity is limited and you want the single most severe failure first.

Extend to many applicants

• Extend to a fleet of applicants by reintroducing an Applicant concept inside _build_session() and lifting each scalar decision to a property on it, then scoping every IC — including each property’s counterexample ICs — to that concept. The scalar shape used here is the right default for the single-applicant search; the per-applicant shape becomes necessary once the audit binds to a real applicant table.

Scale up / productionize

• Real rule packs are large. The template rebuilds a fresh model per audit precisely so the per-model rule count stays bounded across many properties; keep that factory pattern as the pack grows, and split oversized packs into property-scoped subsets.
• Cross-check the encoding against the source rule pack before trusting a PASS: a pass is sound only for the rules and properties as encoded, so a missing rule arm can pass silently. See the Troubleshooting notes on audit soundness.

Troubleshooting

A property reports PASS / INFEASIBLE when you expected FAIL

• The audited property holds: no feasible applicant falsifies it under the bundled ruleset. This is the audit’s pass signal for that property — the verdict line reports Verdict: PASS (0 witness(es), status=INFEASIBLE). For the bundled catalog this is the expected outcome for senior_implies_review because the buggy rule literally encodes “manual review = senior”.
• If you expected a witness and got none for a different property, double-check the counterexample builder: did the thunk return ICs that assert the negation of the property (e.g. is_frail == 1 AND is_manual_review == 0 for “every frail applicant goes through manual review”)? An accidentally-positive IC (is_frail == 0) would not match the property’s negation.
• Empty reference data: confirm data/age_buckets.csv has at least one non-senior bucket (age < SENIOR_THRESHOLD_YEARS). The buggy rule’s gap is chronic + non-senior applicants slipping past manual review; if every bucket is at or above the threshold, all applicants are flagged as senior and frail_implies_review / chronic_under_50_implies_review correctly find no counterexample (PASS for the wrong reason).

ValueError: id column must be dense and contiguous

• The pre-solve check ran on age_buckets.csv or coverage_bands.csv and found gaps in the id column. The solver bounds the corresponding decision by lower=min(id), upper=max(id); without dense IDs it can pick a value with no matching reference row, and the relational-time implies rules gated on the matching row will not fire — leaving the rule indicator unconstrained for that solution.
• Renumber the rows so IDs run consecutively from the minimum to the maximum (e.g., 1, 2, 3, … or 10, 11, 12, …). Trailing or leading gaps are fine to delete; mid-table gaps are the problem.

How many witnesses will the solver return?

• Up to MAX_WITNESSES (16 by default) or however many feasible witnesses exist, whichever is smaller. solve_info().num_points reports the actual count after the solve; solve_info().termination_status reports SOLUTION_LIMIT when the limit was hit and OPTIMAL when the search has been exhausted.
• When status == OPTIMAL, the search exhausted the feasible set: the set of returned witnesses is stable across runs and only the row ordering may vary. When status == SOLUTION_LIMIT, the solver stopped early and the specific K-subset of witnesses returned can vary across runs and solver versions — only the existence of K witnesses is stable.
• Treat the solution column as a label, not a ranking.
• The K returned witnesses are guaranteed to be pairwise distinct on at least one decision (age, chronic flag, coverage, or any indicator) but not maximally diverse, and they are not ranked by severity or any objective. For systematic spread across the failure-mode space, raise MAX_WITNESSES past the size of the feasible set so the solver exhausts every distinct case; for ranking, add problem.minimize(...) over a severity score and post-process.

"Property holds" -- how do I know the audit was sound?

• A pass result (no witness) means the solver could not find a feasible applicant satisfying the counterexample IC under the modelled ruleset. This is sound for the ruleset as encoded — if your encoding misses a rule arm, the audit will silently pass on the unencoded gap. Always cross-check the encoding against the source rule pack: for every rule arm, there should be a corresponding model.require(...) or implies(...).
• A pass result is also sound only for the property as encoded. Cross-check that the property itself matches the regulation — auditing the wrong property PASSes for the wrong reason.
• Bounded model-checking caveat: this template enumerates K witnesses up to a MAX_WITNESSES limit. That is a search-space cap, not a soundness cap — the solver still proves INFEASIBLE (or returns the full feasible set) when the search exhausts within the time limit. Watch for status: SOLUTION_LIMIT: that means more witnesses may exist beyond the K reported.

Import error for relationalai

• Confirm your virtual environment is active: which python should point to .venv.
• Reinstall dependencies: python -m pip install ..

Authentication or configuration errors

• Run rai init to create or update your RelationalAI/Snowflake configuration.
• If you have multiple profiles, set export RAI_PROFILE=<your_profile>.

MiniZinc solver not available

• This template uses the MiniZinc constraint solver. Ensure the RAI Native App version supports MiniZinc.
• HiGHS is not appropriate here — the model is discrete satisfaction with categorical decisions and binary indicator equivalences, not LP/MILP.

Learn more

Core concepts

• Prescriptive reasoning — the Problem API, decision variables, and constraints that model the ruleset.
• Constraint satisfaction and multi-solution search — solving in enumeration mode and reading back several solutions.

Language / modeling reference

• Integrity constraints and require — encoding rule bodies and property negations as ICs.
• PyRel v1 modeling — concepts, relationships, and the standalone scalar-relationship shape used for the applicant decisions.

CLI / SDK guides

• RelationalAI Python SDK — installing and configuring the relationalai package and connecting to Snowflake.

Support

• File issues at the RelationalAI templates repository.