feat(nli): opt-in accurate NLI model with consent and a reported fallback

CHANGELOG.md

@@ -6,6 +6,39 @@ All notable changes to this project are documented here. The format follows
 
 ## [Unreleased]
 
+### Added
+- **An opt-in accurate NLI model.** The bake-off's winner,
+  `MoritzLaurer/DeBERTa-v3-large-mnli-fever-anli-ling-wanli`, runs at k=2 with cuts
+  calibrated on SciFact train. Its SciFact dev macro-F1 is 0.697, against 0.580 for
+  the default model. It is not better on news: on AVeriTeC claims with a readable
+  source it scores 0.475, against 0.537 for the default model at k=2. It is
+  recommended for scientific sources, not for news. It is 643 MB, against 244 MB,
+  and the default install does not change.
+- **`proofpath check --accurate`** uses the accurate model for one run.
+  **`[models] nli = "accurate"`** uses it for every run; set it with
+  `proofpath config set models.nli accurate` or in the `/config` panel.
+- **`permissions.install_model`** guards the 643 MB download. It is `ask` by
+  default: the run asks once, naming the model and its size, with the browser
+  question's answers (once, always, no, never), and "always" and "never" are saved.
+  With no terminal, `ask` is treated as `deny` and the denial is reported. A denied
+  or failed download falls back to the default model and says so in three places:
+  a note with the reason and what would change it (dropped by `-q`, and on stderr
+  under `--format json` or `sarif`); in text mode, an
+  `nli        default model chosen; requested accurate (<reason>)` line that `-q` keeps;
+  and `nli_requested: accurate (<reason>)` in the report's `models` block. That
+  block now also names the `k` that ran.
+
+### Changed
+- **A note when a run has no real low tier.** A run whose `medium` cut sits within
+  0.01 of `decide` now says "this model has no real low tier on SciFact, so an
+  asserted verdict is almost always medium or better". Default runs say it too: the
+  default's `medium` (0.457948) sits 0.008 above `decide` (0.45), which the
+  2026-09-12 tier sweep already measured. When the no-high-tier note also applies,
+  the two are joined with "; ".
+- **The no-high-tier note** now reads "this model earns no high tier on SciFact dev,
+  so medium is the strongest confidence shown".
+- **CI runs strict mypy** over the whole of `src/`.
+
 ### Measured
 - **An NLI bake-off** (`scripts/eval_nli_bakeoff.py`, report in
   `docs/eval/2026-10-01-nli-bakeoff.md`). It compares three NLI models, three

README.md

@@ -155,6 +155,13 @@ was near-certain here", not as a guarantee of 85 % precision. And `medium` lands
 almost exactly on `decide`, so `low` is practically empty among asserted verdicts —
 the display is effectively **two tiers**: near-certain, and asserted at all.
 
+The report says this itself. A run whose `medium` cut sits within 0.01 of `decide` —
+the default model's does, and so does the [accurate model's](#accurate-model-opt-in) —
+prints `this model has no real low tier on SciFact, so an asserted verdict is almost
+always medium or better`. A calibration that leaves `high` out of reach prints `this
+model earns no high tier on SciFact dev, so medium is the strongest confidence shown`.
+When both hold, both are printed.
+
 ## Citations it reads
 
 Numeric markers — `[12]`, `[12,15]`, `[12-15]`, Nature-style superscripts — and, since
@@ -241,13 +248,61 @@ Apple Silicon Mac, models already downloaded:
 | 1-page markdown draft, 7 references | 79.3 s (v0.1 cold) | **1.35 s** ([v0.2](docs/eval/2026-09-15-v0.2-live.md)) — 15.8 s in v0.1 |
 | 19-page arXiv PDF, 68 references | 12 m 57 s | 3 m 42 s ([v0.1](docs/eval/2026-09-12-v0.1-live.md)) |
 
-The **first ever** run also downloads about 250 MB of ONNX models. Since v0.2 a
+The **first ever** run also downloads about 250 MB of ONNX models. The opt-in
+[accurate model](#accurate-model-opt-in) is a further one-time 643 MB download, asked
+before it starts. Since v0.2 a
 cached re-run asks the network for nothing: reference resolution and the retraction
 check are cached (resolutions 30 days; a retraction hit 30 days, a miss 7 days), the
 fetched text for 7 days, and chunks and verdicts for as long as the text is unchanged. The models are still loaded, and any source whose text
 has expired or was never read is fetched again — the PDF re-run above (v0.1) still
 spent 22 s fetching and re-scored 3 of 102 claims.
 
+## Accurate model (opt-in)
+
+The default entailment model is `cross-encoder/nli-deberta-v3-base` (244 MB). The
+**accurate** profile swaps it for `MoritzLaurer/DeBERTa-v3-large-mnli-fever-anli-ling-wanli`
+(643 MB), reads the top **two** passages per claim instead of one, and uses cuts
+calibrated for that pairing on SciFact train. The default install does not change.
+
+```bash
+proofpath check paper.pdf --accurate        # this run only
+proofpath config set models.nli accurate    # every run; or the models.nli row in /config
+```
+
+**What it buys.** On SciFact dev it scores **0.697 macro-F1, against 0.580** for the
+default model calibrated and scored the same way ([the bake-off](docs/eval/2026-10-01-nli-bakeoff.md)).
+Read 0.697 as optimistic: the same dev split chose this model out of 27 combinations and
+reports its score. With the cuts it ships with, its tiers on dev are `high` 15 of 15
+right (too few to judge), `medium` 114 of 151 (0.755) and `low` empty
+([design](docs/superpowers/specs/2026-10-01-accurate-nli-design.md)), so its reports
+carry the low-tier note above.
+
+**What it does not buy.** It is **not better on news and fact-check pages**. On
+AVeriTeC claims with a readable source it scores 0.475, against 0.537 for the default
+model at k=2 (the shipped default, at k=1, scores 0.438), and all of them are below the
+0.708 majority baseline. Use it for scientific sources, not for news.
+
+**What it costs.** A one-time 643 MB download, and 54 ms per claim–passage pair against
+19 ms (batched, in the eval harness) — with twice as many pairs per claim.
+
+**Consent.** The download is never silent. When the model is not cached yet, the run
+asks once, naming the model and its size, with the browser question's answers: once,
+always, no, never. "Always" and "never" are saved to `permissions.install_model`
+(`ask` by default; `allow` and `deny` skip the question). Piped or in CI there is no
+prompt: `ask` is treated as `deny` and reported. When the download is denied or fails,
+the run uses the default model and says so, so a report never names a model it did
+not run:
+
+- a note, `accurate NLI model not used: <reason> — using the default model.`, with what
+  would change it. It is printed with the run's other notes, so `-q` drops it; under
+  `--format json` or `sarif` it goes to stderr;
+- in text mode, a line that `-q` does not drop:
+  `nli        default model chosen; requested accurate (<reason>)`;
+- `nli_requested: accurate (<reason>)` in the report's `models` block, which also names
+  the `k` that ran.
+
+Once the files are cached, nothing is asked.
+
 ## Looking inside the cache
 
 Everything proofpath fetches, embeds and decides lands in one plain SQLite file:
@@ -408,6 +463,7 @@ switch to, the run says so and tells you how to add one, on the same channels.
 | What | Set | Result |
 |---|---|---|
 | Retrieval + entailment | SciFact dev, 340 pairs | 0.609 accuracy, 0.597 macro-F1, against a 0.406 trivial baseline ([details](docs/eval/2026-09-12-scifact-dev.md)) |
+| Retrieval + entailment, [accurate model](#accurate-model-opt-in) (opt-in) | SciFact dev, 340 pairs | 0.697 accuracy, 0.697 macro-F1, against 0.591 / 0.580 for the default model in the same 2026-10-01 run. Cuts were fitted on SciFact train there, so the default's figures differ from the row above. Dev both chose this model and scores it, so 0.697 is optimistic; on AVeriTeC it is no better than the default model at k=2 (0.475 against 0.537) ([details](docs/eval/2026-10-01-nli-bakeoff.md)) |
 | Reference resolution | hand-built ghost set, 274 references | 0.0 % false-ghost, 99.1 % ghost recall ([details](docs/eval/2026-09-12-ghosts.md)) |
 | Source access | 50 DOIs | 72 % full text, 18 % abstract only, 10 % nothing ([details](docs/eval/2026-09-11-coverage.md)) — a real biomedical paper in the live runs reached 33 % full text |
 | Citation pairing, numeric | 61 hand-built passages | 0.99 ([details](docs/eval/2026-09-11-pairing.md)) |

docs/superpowers/OPEN-ITEMS.md

@@ -608,4 +608,5 @@ five packages. The user's decisions:
 | 20.8 | Bibliography parsing that was measured but never shipped | two-column rejoin (9.10/12.1), multi-block headless fallback (11.11), more headings (16.5), `[1]-[3]` ranges (9.4) |
 | 20.9 | The judge's quote is never checked | `judge._collect` does not verify that the quoted span occurs in the passage. Checking it is a cheap way to enforce product rule 1 |
 | 20.10 | Eval honesty | add a `--judge` flag to `scripts/eval_averitec.py`; do one run with the browser allowed; show the 0.404 search score in the README "Measured" table |
-| 20.11 | NLI bake-off result | **Winner: `large-fever` (MoritzLaurer DeBERTa-v3-large mnli-fever-anli-ling-wanli) × k=2 × `max`.** SciFact dev macro-F1 0.697, against 0.580 for the `base` × k=1 × `max` baseline and 0.608 for the best `base` row. Accuracy 0.697. AVeriTeC 3-way 0.438, or 0.475 on the readable subset, against a 0.708 majority baseline. Cost: 643 MB and 54 ms/pair, against 244 MB and 19 ms/pair. Full report: `docs/eval/2026-10-01-nli-bakeoff.md`. Next: a follow-up spec for an opt-in "accurate" NLI model (consent download, spec §7.1). It must settle three open points. (a) Exclude rule-decided rows from the tier walk: the numeric layer fires 4–6 times on train with 0 correct, so it pins `high` at 1.000000. (b) The winner's `medium` cut sits on `decide`, so the report shows only two tiers. (c) On AVeriTeC the winner is below `base` × k=2 (0.475 against 0.537), and `Supported` is still 2/19 |
+| 20.11 | NLI bake-off result | **Winner: `large-fever` (MoritzLaurer DeBERTa-v3-large mnli-fever-anli-ling-wanli) × k=2 × `max`.** SciFact dev macro-F1 0.697, against 0.580 for the `base` × k=1 × `max` baseline and 0.608 for the best `base` row. Accuracy 0.697. AVeriTeC 3-way 0.438, or 0.475 on the readable subset, against a 0.708 majority baseline. Cost: 643 MB and 54 ms/pair, against 244 MB and 19 ms/pair. Full report: `docs/eval/2026-10-01-nli-bakeoff.md`. Next: (a) and (b) are settled by the accurate-NLI design (`docs/superpowers/specs/2026-10-01-accurate-nli-design.md`), which adds the winner as an opt-in "accurate" profile behind a consent download (spec §7.1); (c) stays open. (a) **settled** — rule-decided rows are left out of the tier walk (the numeric layer fired 4–6 times on train with 0 correct and pinned `high` at 1.000000); the accurate cuts are `high` 0.999142. (b) **settled** — the `medium` cut still sits on `decide`, and the report now says so itself (`NO_LOW_TIER`, default runs included). (c) **still open** — on AVeriTeC the winner is below `base` × k=2 (0.475 against 0.537), and `Supported` is still 2/19; the README recommends the profile for scientific sources, not for news |
+| 20.12 | Accurate-NLI follow-ups | (1) A shared `browser.read_terminal_answer` helper: `model_gate.ask_model_terminal` repeats `browser.ask_terminal`'s prompt loop and imports the private `_CHOICE_ANSWERS` to do it. (2) The `-q` `nli` line carries the fallback reason but not the advice. (3) Ctrl-C and `/stop` do not interrupt a running 643 MB download. (4) An "installed" but corrupt accurate model fails the run instead of falling back. (5) A multilingual NLI model is still deferred (out of scope in the accurate-NLI design); non-English claims still need the judge to translate |