14 · Random forest verification¶

On this side, a stall concludes nothing: not that the property holds, and not that it fails. A deployed model is retrained rather than patched, so there is no artefact a repair could be folded into, and an undecided question stays undecided until it is asked over a narrower region. Every forest response carries that sentence, as the caveat forest_stall_is_not_a_verdict, whatever its result.

Random Forest Verification checks a trained random forest against properties you state: robustness, monotonicity, fairness and reachability. Each comes back decided, as a counterexample checked on the model itself or as a proof that none exists in the region, or honestly undecided. This chapter is the two questions it answers, the region each answer is about, how to tell a counterexample that matters from one that does not, and a worked example on a public credit model.

The model¶

The model is read as it is deployed: ONNX-ML (TreeEnsembleClassifier, TreeEnsembleRegressor and opset 5's TreeEnsemble), or a Treelite 4.x JSON dump, told apart by their content. A scikit-learn model comes through an ONNX export. A construct neither reader accepts, such as an equality split, preprocessing inside the graph or a transform that is not monotone, is refused by name rather than approximated.

Two questions, two modes¶

forest: your own properties, however hard they are. A table states each property and the region it is asked over, and each comes back decided. A hard region is cut in two on the feature with the most open thresholds, again and again, and each piece is solved with its own time limit: a counterexample in any piece is a counterexample, and the property holds only where every piece is refuted.

result = client.verify_forest("credit_rf.onnx", "credit.properties.json", anchors="credit.csv")
for record in result.records:
    print(record["id"], record["status"])          # SAT, UNSAT, or STALL, which concludes nothing
for caveat in result.caveats:
    print(caveat["code"])                          # on every forest response, whatever its result

found = client.enumerate_counterexamples("credit_rf.onnx", "search.json", anchors="credit.csv")
for finding in found.findings:
    print(finding["anchor_class"], "->", finding["class"], finding["plausibility"]["label"])

Property	It holds when
`robustness`	the decision is the same everywhere in the region around an anchor record
`monotonicity`	moving one feature one way never loses the class, or never lowers its score
`fairness`	changing only the protected features never changes the decision
`reachability`	some input in the region reaches a class, or, for a regressor, a bound

forest_enumeration: the fast search, around real records. Many narrow questions: every feature of a real record pinned but one to three, and those allowed to move only in the direction you name, up, down or any. With almost everything pinned, each question is decided in milliseconds, and decided both ways: a finding is a verified counterexample, and a question that held is a proof that no such move flips that record. Only minimal findings are listed: once a set of moves flips a record, no larger set containing it is asked about. A single ordered move reports the smallest change that flips, found exactly on the model's own thresholds. The enumeration returns verdicts only, and no certificates.

{
  "enumeration": {
    "anchors": {
      "rows": [
        18
      ]
    },
    "moves": {
      "PAY_1": "down",
      "PAY_AMT6": "up"
    },
    "k": 2,
    "label_column": "Default"
  }
}

anchors is explicit rows, or the records the model gives one class, in file order or closest to the decision first. k is the most moves combined, one to three. A finding is a proposal: its property is written as a row you could paste into a table, with no expect and no gate, because promoting it is a reviewer's decision.

The region is the proposition¶

A forest property is asked over a region: a default of fixed (the anchor's own value) or free (the feature's whole domain), and, per feature, a ball, a range or a set of values. The region is as much the question as the property is, so nothing chooses it for you, and the region the engine used travels with every verdict as region_effective. Every forest response carries the caveat forest_region_is_the_proposition: a verdict is about its region and about nothing wider.

Each moving feature needs a domain, and domains inferred from data are refused until a person confirms them. Bounds read off a sample are facts about the sample. A table whose domains_status is anything but confirmed is refused before it is queued, as forest_domains_not_confirmed. A table that names another model's digest in model_sha256 is refused too: a table reviewed against one model is no evidence about another.

Plausibility and the neighbourhood¶

A region is a box, so a counterexample can sit in a corner no customer occupies. That counterexample is true of the model and useless to its owner. Every SAT carries a plausibility judgement against the records you supplied as anchors:

the nearest real record, and its distance in standard deviations;
the features outside the reference's own range;
the pairs of features whose joint cell holds the counterexample and no real record;

and a label, supported or off_support. Nothing there changes the verdict: an UNSAT over a loose box holds over every realistic part of it, so only a SAT can mislead, and the label says how much weight it carries.

The enumeration adds the neighbourhood: how often the 25 real records nearest a counterexample had the class the model gives it. That is the line between a pattern the model learned and a misclassification. A finding whose neighbours mostly have the class the model gives it is the model reflecting its data; one whose neighbours mostly do not is the model being wrong about the people it would be used on.

A worked example¶

The model is a public credit-default recipe, retrained and pinned: 100 trees over the UCI default of credit card clients data, verified around its 29,601 records. Row 18 is a customer who repaid, and the forest agrees, with a probability of default of 0.464. Its latest month is one month late.

The search asks whether safer histories can tip that customer into default: the latest month's status moving down (PAY_1, a smaller delay is safer), and the payment six months back moving up (PAY_AMT6, a larger payment is safer), at most two moves together. Three questions: each move alone, then the pair. Each move alone leaves the record no_default. Together they flip it:

{
  "property": {
    "id": "row18-PAY_1-down-PAY_AMT6-up",
    "kind": "robustness",
    "anchor": {
      "row": 18
    },
    "region": {
      "default": "fixed",
      "PAY_1": {
        "values": [
          -2,
          -1,
          0,
          1
        ]
      },
      "PAY_AMT6": {
        "range": [
          0,
          528666
        ]
      }
    }
  },
  "anchor_class": "no_default",
  "class": "default",
  "change": {
    "PAY_1": [
      1,
      -2
    ],
    "PAY_AMT6": [
      0,
      7
    ]
  },
  "scores": {
    "no_default": 0.4928,
    "default": 0.5072
  },
  "model_verified": true,
  "plausibility": {
    "label": "supported",
    "reference_rows": 29601,
    "nearest": {
      "row": 8062,
      "distance_std": 0.109
    },
    "outside_range": [],
    "empty_pairs": 0,
    "empty_pairs_named": []
  },
  "neighbourhood": {
    "label_column": "Default",
    "k": 25,
    "share_with_predicted_class": 0.24,
    "furthest_std": 1.084
  }
}

What changed: the latest month recorded as no spending (PAY_1 from 1 to −2) rather than one month late, and a payment of 7 six months back (PAY_AMT6 from 0 to 7). Each is a safer history.
What the model does: it moves the customer to default, at 0.5072, a shift of 4.3 points. The counterexample is re-checked on the model in exact arithmetic (model_verified), and onnxruntime gives the same score to four decimal places.
Whether it matters: the point is supported, near real customers, and of the 25 real customers nearest it, 24% defaulted. Most repaid.

What it is: a verified violation of domain logic around a real customer. The forest is not monotone in either feature, and nothing in its training asked it to be. A team that needs it to be has a property to add to its table, and a model to retrain.

What it is not: an account of why the trees learned it. The finding shows what the model does; why it does it is a question about the training, which verification does not answer.

The limits¶

A stall concludes nothing, on this side: not that the property holds, and not that it fails. Narrow the region, or split the question.
An UNSAT is the SAT solver's refutation, admitted: sound, and not self-contained. The forest profile does not build a certificate unless you set certificate_detail: core, and the enumeration builds none at all.
Two-copy properties over wide regions are hard. Fairness and monotonicity compile two copies of the forest into one circuit and ask whether two nearly equal sums land either side of the threshold, the shape a SAT solver finds hardest. Narrow regions decide; a wide one is cut and may stall.
The search covers what it names. A counterexample that needs more than k moves, or a move in a direction the search did not name, is outside the enumeration, and its output says so in enumeration.covers.
A verdict is about its region, and the domains it rests on are the ones a person confirmed.