Metadata-Version: 2.4
Name: provable
Version: 0.9.0
Summary: Exact audit, surgery, and certified discovery for tree ensembles
License-Expression: MIT
Project-URL: Homepage, https://provable.ml
Project-URL: Documentation, https://provable.ml
Project-URL: Repository, https://github.com/provable-ml/provable
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Operating System :: OS Independent
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: numpy
Requires-Dist: pandas
Requires-Dist: scipy
Requires-Dist: scikit-learn
Requires-Dist: statsmodels
Requires-Dist: xgboost>=2.0
Requires-Dist: tabulate
Requires-Dist: plotly
Requires-Dist: qrcode
Dynamic: license-file

# provable

Exact audit, surgery, and certified discovery for tree ensembles.

`provable` treats a fitted model as an auditable artifact. On xgboost models it reads an
**exact** itemization of every rule the model uses (the transported atom spectrum),
checks it against a declared policy, removes forbidden rule families by **appended-tree
surgery whose output is still a valid native model file**, and emits a tamper-evident
certificate dossier that a third party can re-check with an independent, numpy-only
verifier that shares no code with the engine. On raw data it runs the certified-discovery
sieve: an FDR-controlled claims ledger, a dark-mass ledger, and the right to refuse
(k = 0 is a verdict, not an error).

- **Tests that ship with the code:** 35 pytest tests, the 17-item acceptance ledger (`tests/selftest.py`, T1-T7), and a verifier mutation battery.
- **Independent verification:** every certificate is re-checked by `provable-verify` - numpy + stdlib only, zero shared code with the engine, machine-enforced in CI.
- **Reproducibility:** the archived DOI version of this package (10.5281/zenodo.21819947) reproduces every number in the papers.
- **Version 0.9.0.** It becomes **1.0.0 when the evidence-bundle schema and the `enforce` API freeze.**

```
            ┌─ WORKFLOW A: audit a model ────────────────────────────────────────┐
model.json ─► load ────► transported atom spectrum (exact, leaf-readable)        │
Policy ─────► audit ───► verdict + findings: masses, shares, threshold locations │
            │ enforce ─► appended-tree surgery ─► model_v2.json (still native)   │
            │            + dossier: evidence.json · certificate.md · MANIFEST   │
            │ verify ──► independent re-check (own parser, own predictor,        │
            │            own transport; zero shared code; numpy + stdlib only)   │
            └────────────────────────────────────────────────────────────────────┘
            ┌─ WORKFLOW B: interrogate data ─────────────────────────────────────┐
X, y ───────► discover (certified sieve) ─► FDR claims ledger · two-tier         │
            │ predictor · toll/penumbra diagnostics · dark-mass ledger ·         │
            │ phase verdict (I / II-a / II-b / III) · or refusal at k = 0        │
            └────────────────────────────────────────────────────────────────────┘
```

The two workflows share one substrate — the **atom schema** (threshold predicates and
their conjunctions) — so a violation found in a model (A) can be interrogated in the
data (B): *is this pattern a property of your model, or of your world?*

---

## One repo, two distributions

| Path | Distribution | What it is | Depends on |
|---|---|---|---|
| `src/provable/` | `provable` | the instrument: load / spectrum / audit / enforce / discover | numpy, pandas, scipy, scikit-learn, statsmodels, xgboost ≥ 2.0, tabulate, plotly |
| `verify/src/provable_verify/` | `provable-verify` | the independent checker examiners run | **numpy only** |

The verifier re-implements from the xgboost JSON spec its own parser, its own
vectorized tree-walk predictor, and its own transport expansion. Independence is
machine-checked: `tests/test_firewall.py` fails CI on any verifier import outside
{stdlib, numpy} or any import of the engine.

The checker also ships standalone at `github.com/provable-ml/provable-verify`, a byte-identical mirror of `verify/`; changes land in this repository first and are mirrored there.

---

## Install

From PyPI:

```
pip install provable
pip install provable-verify
```

Working from a clone (editable installs of both distributions):

```
pip install -e .            # provable (engine): pulls numpy, pandas, scipy, scikit-learn,
pip install -e ./verify     # provable-verify (checker): numpy only     statsmodels, xgboost, tabulate, plotly, qrcode
```

After this, `import provable` works anywhere in the venv and the verifier runs as
`python -m provable_verify <evidence.json> <model.json>` from any directory (file
arguments are relative to your cwd -- the demo dossier lives in `dossier_demo/`).

Tested with Python 3.12, xgboost 3.3.0 (adapter write-back exercised on 3.3.0 only so
far; needs xgboost ≥ 2.0). The verifier needs numpy only.

---

## Quickstart A — audit, enforce, verify

```python
import xgboost as xgb
from provable import audit, enforce, Policy, between

policy = Policy([between('age', 'group_A')], name='fair_lending_demo')

# Audit an EXTERNAL artifact you did not train
a = audit('model.json', policy, X_val, out_dir='dossier_audit')
a['verdict']['state']            # 'PASS' | 'FINDINGS' | 'DECLINED'
a['findings']                    # per clause: n_atoms, exact data mass, share of
                                 # model variance, threshold locations

# Remove the family; output is a still-valid native model
b = enforce('model.json', policy, X_train, X_holdout, 'model_v2.json',
            y_holdout=y_holdout, out_dir='dossier_enforce')

m2 = xgb.Booster(); m2.load_model('model_v2.json')   # loads in STOCK xgboost
```

```
$ python -m provable_verify dossier_enforce/evidence.json model_v2.json
  [PASS] 1 bundle hash = certificate id
  [PASS] 2 model file hash matches bundle
  [PASS] 3 policy hash matches bundle
  [PASS] 4 structural probe (own transport)
  [PASS] 5 behavioral probe (own predictor)
  [PASS] 6 verdict supported by own probes
  [PASS] 7 limits panel present
VERIFICATION: PASS
```

**Data contract (A).** `X` is numeric (ndarray or DataFrame values); feature names come
from the model artifact. Predicates are evaluated in float32 with xgboost's own routing
semantics (`x < c` → left), so threshold-boundary rows route identically in the spectrum
and the stock engine. `NaN` anywhere in `X` is a coded refusal (R-07): `audit` returns
DECLINED, `enforce` raises — the transported audit is not defined for missing-value
routing, and the tool says so rather than guessing.

## Quickstart B — certified discovery

```python
from provable import CertifiedDiscovery

cd = CertifiedDiscovery(stability_reps=8, seed=0)
report = cd.run(X_df, y)                    # X_df: DataFrame (mixed dtypes), y: 1-D numeric
cd.plot()                                   # 4-panel plotly figure
cd.claims_                                  # certified claims ledger (DataFrame)
p = cd.predict(X_new, model='two_tier')     # 'two_tier' | 'certified' | 'xgb'
```

**Data contract (B).** Numeric columns get threshold atoms, non-numeric columns get
one-hot atoms; `NaN` makes every predicate evaluate to `False` (the engine receives NaN
natively). If `y ⊆ {0, 1}` the run is a linear probability model: MSE/Brier primary,
AUC also reported; predictions are not clipped to [0, 1].

---

## The dossier

Every `audit`/`enforce` run with `out_dir` emits:

```
dossier/
├── evidence.json     canonical bundle -- the source of truth; certificate id =
│                     'PV-' + sha256(canonical bundle)[:16]
├── certificate.md   human rendering (GitHub-renderable markdown) bound to the same bundle
└── (enforce)         model_v2.json, MANIFEST.sha256, HOW_TO_VERIFY.txt in the demo
```

Marks used everywhere: `#exact` — an arithmetic fact of the artifact (structural zeros,
masses, prices; no error bar exists). `#est` — a statistical estimate, always with its
interval. The limits panel ("what this does not establish": proxies, causal claims,
off-distribution behavior, NaN routing) is furniture, not fine print: every bundle
carries it and verifier check 7 fails if it is stripped.

## Verdict grammar

| Verdict | Meaning |
|---|---|
| `PASS` | certified absence of every forbidden pattern, within stated (float32 write-back) tolerance |
| `FINDINGS` | violations exist — quantified, localized, priced |
| `DECLINED` | the instrument refuses, with a coded reason — never a crash, never a shrug |

| Code | Refusal |
|---|---|
| R-01 | nothing certifiable at the agreed FDR budget (k = 0) |
| R-02 | reserved certification split too small |
| R-03 | expansion above exact-enumeration cap |
| R-04 | pattern off the representable lattice |
| R-05 | feature not present in the model |
| R-06 | probe budget exceeded |
| R-07 | missing values present; transported audit not defined |
| R-08 | unsupported clause kind |

---

## What "exact" means here (workflow A)

A fitted ensemble on continuous inputs is already a Boolean object on its own split
thresholds. Each leaf box expands exactly:

```
1[lo <= x < hi] = 1[x >= lo] - 1[x >= hi]        (per feature; telescoped over the box)
```

so the whole artifact equals `base_score + Σ coef · AND_f 1[x_f >= t_f]` — a finite,
leaf-readable, signed rule spectrum with no sampling and no approximation. Audit
families, prices, surgery, and both certification probes operate on this identity.

| Stage | Mechanics | Where |
|---|---|---|
| load / parse | native JSON → leaf boxes (interval constraints per feature); base_score parsed to the empty atom | `adapters_xgb` |
| transport | boxes → signed threshold atoms; guarded by `max_atoms` (R-03 above it) | `calculus.Spectrum` |
| audit | family selection (`between`, `involving`) → exact data mass, share of model variance, per-threshold profile | `surface.audit` |
| price | excision price = mean squared removed component on the sample (`#exact`), quoted **before** the edit | `calculus.data_mass` |
| enforce | one appended chain-tree per removed atom (−coef on the conjunction, 0 elsewhere); off-rule rows **bit-identical** by construction | `adapters_xgb.append_rules` |
| structural probe | re-transport the edited file; max residual forbidden coefficient | `surface.enforce` + verifier check 4 |
| behavioral probe | consecutive-cell second differences over the full (i, j) threshold grid at probe contexts; zero everywhere ⇔ no i×j interaction at the artifact's own resolution | `calculus.grid_probe` + verifier check 5 |
| certificate | canonical bundle, hash-as-id, verdict, limits, self-grading panel (predicted price vs realized holdout change) | `evidence` |

Measured on the shipped acceptance ledger (`tests/selftest.py`, 17/17, xgboost 3.3.0,
200-tree depth-4 external artifact, 4,676 atoms):

| Identity | Measured |
|---|---|
| transport spectrum == stock margin | 2.4e-06 max abs |
| transport == reference Möbius calculus (binary model) | 2.2e-16 max abs |
| off-rule rows after surgery, stock reload | 0.0 (bit-identical) |
| on-rule rows vs functional edit | 1.9e-06 max abs |
| structural residual after excising 299 atoms | 6.2e-09 |
| behavioral grid probe on the edited file | 3.2e-06 |
| excision price predicted vs realized (holdout) | 0.1131 vs 0.1196 (within 25% band, printed on the certificate) |

## The sieve (workflow B)

```
raw X, y
  ├─ engine:      XGBoost on raw features (early-stopped on a carve of the training rows)
  └─ instrument:  atom dictionary ─► RS(ν,R) proposal on S1 ─► forward core ─► one OLS
                  pass on S2 + BH(q) ─► certified model ─► claim-free halo ─► two-tier
diagnostics:      penumbra · toll bounds · spotlight margin · completion · phase · ledger
report:           console tables + plotly figure + machine-readable dict + claims DataFrame
```

The gate is one selection-conditional OLS pass on the reserved half S2 with BH(q) over
partial-t p-values; every quoted effect, CI, t, p comes from that single pass. The halo
is claim-free (using the two-tier predictor never touches the ledger's guarantee). The
dark-mass ledger splits Var(y) into legible (certified), dark-to-certification-but-
visible-to-engine, and engine MSE (noise + dark to both). Phases: I (refusal
competitive or k = 0), II-a (engine ahead, frame-blind margin M_C > 0), II-b (engine
ahead, M_C ≤ 0), III-like (certified core ahead on test).

Key parameters (defaults): `fdr_q=0.10`, `rounds=4`, `entry_t=2.0`, `entry_cap=300`,
`core_cap=120`, `core_tmin=1.0`, `n_cuts=8`, `cart_cuts=True`, `n_harvest=40`,
`interactions=True` (shadow rule `conj_shadow=0.9`), `prune_support=0.005`,
`prune_dup_r=0.98`, `halo='auto'`, `refit_scope='train'`, `test_frac=0.25`,
`s2_frac=0.5`, `stability_reps=0`, `xgb_params=None` (600 trees, lr .05, depth 6,
hist, early stop 50), `seed=0`. Full table with meanings in the class docstring.

**v0.2 vocabulary extensions** (all default-off; when off, the run — claims, report
dict, printed report — is byte-identical to v0.1): `le_cuts=False` mirrors every ≥ cut
as a ≤ twin, making low-side cells nameable and claimable (the duplicate prune switches
from |r| to signed r so exact complements survive); `band_conj=False` admits same-column
`(x>=a)&(x<=b)` pairs, making interior bands first-class atoms; `n_path_harvest=0` with
`path_depth=3` harvests top-gain root-subpath conjunctions from the fitted engine's own
trees (Yes branch → ≤; numeric features only; standard leaf grammar), diversified by
`path_per_set=3` so dominant structures cannot monopolize the harvest; `core_dedup_r=None`
applies the dictionary's duplicate principle at core admission — one representative per
near-duplicate family — without which a densified vocabulary floods the core with shadows
whose S2 partial t's split and BH kills the whole family.

---

## Tests

```
python tests/test_firewall.py     # verifier imports ⊆ stdlib+numpy, zero engine imports
python -m pytest tests/           # 35 contract + protocol + verifier-mutation tests
python tests/selftest.py          # T1-T7 acceptance ledger (17/17)
```

| Suite | Locks |
|---|---|
| `test_contracts.py` | the identities certificates stand on: transport == stock margin across model shapes (depth 1–6, incl. single-split and constant models), float32 boundary routing at exact thresholds, base_score paths, append-tree on/off semantics |
| `test_protocol.py` | refusal codes (R-05, coded R-07), policy canonicalization, order-free bundle hashing, any-single-field mutation breaks the certificate id, limits always present and rendered, verdict grammar closed set, sieve determinism per seed; v0.2 vocabulary: flags-off schema stability, deterministic low-side (\u2264) claim recovery with the extended dictionary |
| `test_verifier_mutations.py` | each of the verifier's seven checks individually killed by a targeted tamper, incl. a resurrected-interaction attack with an attacker-re-hashed bundle |
| `selftest.py` | end-to-end: external artifact → audit → enforce → stock reload → independent verify → mutation → discover → refusal |

Deferred by design until the respective layers land: bundle-schema snapshots and
renderer golden files (reporting layer), enforce-signature tests (refit mode), and the
multi-version xgboost/lightgbm adapter matrix (CI env matrix).

## Road to 1.0.0

- A `schema_version` field in the evidence bundle, honored by the verifier.
- `enforce` grows by keyword-only arguments from here; the positional surface is frozen at 0.9.0.
- The deferred snapshot/golden tests above.
- Semantic versioning from 0.9.0: breaking changes to the evidence-bundle schema or the public API happen only at a major version; 1.0.0 marks the freeze of both.

## Guarantees, estimates, and caveats

- **Controlled:** the FDR of the claims ledger, by BH(q) over a single
  selection-conditional S2 pass. **Exact:** every `#exact` quantity is an arithmetic
  fact of the artifact (and sample) — structural zeros, masses, prices, off-rule
  bit-identity.
- **Float32 is the write-back resolution:** appended-tree coefficients are stored as
  float32 by the native format; certification tolerances (structural ≤ 1e-4, behavioral
  ≤ 1e-3) state this rather than hide it. Measured values are orders of magnitude below
  the gates.
- **Estimates are labeled:** holdout deltas carry CIs; the sieve's penumbra, toll
  bounds, spotlight, and M_C are plug-in quantities with disclosed proxies; ridge* is a
  hindsight benchmark for the frame-blind class, not a deployable model.
- **The limits panel is non-removable:** no proxy claim, no causal claim, no
  off-distribution claim, no fairness-of-outcomes claim — certified absence of named
  rule families in the file at the stated hash, and nothing more.
- **`refit_scope='train'`** re-uses S2 in the sieve's refit and carries a residual
  selection-optimism term (measured small); `'s2'` avoids it; both rows print.
- **Verifier independence is a checked property,** not a promise (see Tests).

## Not in 0.9.0

lightgbm adapter; xgboost version matrix beyond 3.3.0; sealed PDF export (the HTML certificate binds to the same bundle); behavioral probe for `involving`
clauses (structural only); refit surgery mode (excise only); `monitor`; vertical report
packs; NaN-aware transported audit (R-07 declared instead).

## Reproducibility

All stochastic steps are seeded (`seed`; house conventions: split rng 4000+seed, engine
9000+seed, stability replicates 31000+b). Given a seed, repeated runs reproduce the
same report and the same certificate id up to timestamps. Runtime reference (single
container CPU): full acceptance ledger ≈ 8 s; independent verification of the demo
dossier ≈ 5 s; sieve on Adult (45,222 rows, P = 235, B = 8) ≈ 10 s.

## Files

```
src/provable/                  adapters_xgb · calculus · policy · evidence · surface · sieve
verify/src/provable_verify/    the independent checker (single module)
tests/                         firewall · contracts · protocol · verifier mutations · selftest
dossier_demo/                  a real enforce dossier: evidence.json, certificate.md,
                               model.json, model_v2.json, MANIFEST.sha256, HOW_TO_VERIFY.txt
```

## Citing

`CITATION.cff` ships in this repository. BibTeX:

```bibtex
@software{provable2026,
  author  = {Souihli, Oussama},
  title   = {provable: Exact audit, surgery, and certified discovery for tree ensembles},
  year    = {2026},
  version = {0.9.0},
  doi     = {10.5281/zenodo.21819947},
  url     = {https://provable.ml}
}

@misc{souihli2026calculus,
  author = {Souihli, Oussama},
  title  = {Every Interaction Has a Price: An Exact Calculus for Tree Ensembles},
  year   = {2026},
  doi    = {10.5281/zenodo.21819690}
}

@misc{souihli2026instrument,
  author = {Souihli, Oussama},
  title  = {Certified Discovery on Real Grams: an Instrument, its Limits, and its Laws},
  year   = {2026},
  doi    = {10.5281/zenodo.21819895}
}

@misc{souihli2026metrology,
  author = {Souihli, Oussama},
  title  = {Dark-Mass Metrology: Pricing What a Certified Model Does Not Know},
  year   = {2026},
  doi    = {10.5281/zenodo.21819925}
}
```

License: MIT.
