recall: fix BM25 length-norm precision + host benchmark vs float BM25 (NDCG parity, faster, deterministic)

[bahadirarda]

Summary

Research-grounded, benchmarked answer to "is Yuva's no-float verified recall actually good, and how does it stand against the people who do this?" — with an honest before/after and a real fix the benchmark surfaced.

Two commits:

1. tb-encode/recall: length-normalization precision fix — a one-line arithmetic reorder in the verified leaf.
2. tools/recall-bench: a host harness that benchmarks the actual Kani-proven leaf against the float BM25 implementations everyone else uses, same-box, on BEIR NFCorpus.

The bug the benchmark found

bm25_tf_norm evaluated the document-length ratio as BM25_B * (dl / avgl) — an integer-floored ratio. For any document shorter than average (dl < avgl, the common case) this floors to 0 and silently disables length normalization; in general it collapses a continuous ratio to a 3–4 step function. Reordering to (BM25_B * dl) / avgl (multiply-before-divide) keeps ~3 fractional digits while staying pure integer / no-float.

Identical for the single-token records the kernel feeds today (dl == avgl == 1), so the M40 boot KAT is unchanged; it only sharpens multi-token ranking (where Cogi's memory is heading).

Result — BEIR NFCorpus test, 323 queries, one WSL box

system	NDCG@10	Recall@10	MAP	QPS	deterministic
bm25s (float, lucene — 2024 SOTA)	0.3052	0.1435	0.1164	~3,250	✗ float
rank-bm25 (float, okapi)	0.3056	0.1446	0.1166	~840	✗ float
Rust-float (ideal, same harness)	0.3052	0.1435	0.1164	~15,900	✗ float
Yuva no-float leaf (integer)	0.3051	0.1433	0.1164	~19,400	✓ bit-exact

Before the fix, the integer leaf scored NDCG@10 0.2887 (−5.4% vs float) with int-vs-float top-10 overlap 0.74 / top-1 52%. After: 0.3051 (float twin 0.3052), overlap 0.9996, top-1 92%.

So the verified integer leaf now matches float BM25 ranking quality, runs ~22–30% faster than the same-harness ideal-float (integer arithmetic, no FP division), and is the only implementation that is both bit-exact deterministic and formally machine-checked.

Why this comparison is fair (and honest)

• All systems consume identical tokens (bm25s standard pipeline, stopwords=english, no stemmer); k1=1.2 b=0.75 everywhere; one canonical evaluator (pytrec_eval). The harness asserts the interchange's params match the leaf's frozen constants.
• bm25s method='lucene' is Yuva's exact IDF twin (ln((N+1)/(df+0.5))), so the comparison isolates float vs integer fixed-point and nothing else. The in-harness ideal-float run reproduces bm25s NDCG@10 to 4 decimals — validating the harness.
• Absolute QPS is hardware-specific; only the same-box figures here are comparable (not compared to any paper's numbers from other hardware).
• The harness links the same tb_encode::recall::bm25_doc_score the kernel scores with — never a second BM25. Index / candidate-gen / top-k are harness plumbing (the kernel keeps those in tb-hal).

Literature grounding

BM25 stays competitive-to-superior out-of-domain and on precise-terminology corpora (BEIR; beats text-embedding-3-large on finance/code term matching). For an agent reading its own memory, exact-match lexical retrieval gives deterministic, interpretable, verifiable-text matches that embedding similarity does not (Beyond Semantic Similarity: Agentic Search via Direct Corpus Interaction, arXiv 2605.05242). Yuva's leaf is the retrieval primitive; QA-memory systems (Mem0, Letta, A-MEM) sit a layer above and could run on it.

Verification

• 13 recall host tests pass; the 5 affected recall Kani harnesses (idf / tf_norm / term_score / absent-is-zero / doc-score-monotone) all VERIFICATION: SUCCESSFUL (the proven properties — denom>0, [0, TF_NORM_CEIL), non-negativity, monotonicity — are scale-agnostic).
• tools/recall-bench is a nested workspace (tb-vmm / prov-signer precedent) — the kernel kbuild / -Zbuild-std lanes are untouched.
• Reproduces from a fresh checkout: prep_bench.py → cargo run --release → eval_all.py (README has the steps + dataset fetch).

[bahadirarda]

Update: added SciFact as a second dataset + honest corrections to the single-dataset framing.

SciFact (5,183 docs, 300 test q): Yuva no-float 0.6634 NDCG@10 vs float twin 0.6625 — parity holds on a second dataset (int-vs-float top-10 overlap 0.997 on both). The in-harness ideal-float again equals bm25s to 4 decimals, revalidating the harness.

Two things the single-dataset table over-implied, now stated plainly in the README:

• Speed: the durable win is vs the same-harness ideal-float (~17–22%, both datasets). It is not universally faster than bm25s — bm25s's numpy vectorisation beats the leaf's scalar scoring on long-document SciFact (~3,290 vs ~2,520 QPS), while the leaf wins on short-document NFCorpus (~19,400 vs ~3,250). Determinism + Kani-verification are the leaf's workload-independent advantages.
• The fix: its principled effect is fidelity to real BM25 (overlap 0.74→0.997 on both). That recovered −5.4% NDCG on NFCorpus; on SciFact NDCG was float-parity either way (floored 0.6667 vs fixed 0.6634 — benign noise, not a gain).

[bahadirarda]

Update 2: a THIRD dataset (ArguAna) surfaced a second precision bug — now fixed.

ArguAna's queries are whole arguments (~hundreds of terms). There the integer leaf's fidelity was only 0.75 and it scored NDCG@10 0.3679 vs float 0.3551 — which looks like beating float but is not: it's the same benign-noise trap (rounding divergence landing favourably), not skill.

Root cause: bm25_doc_score summed bm25_term_score values, each already divided by SCALE — so one rounding error accrued per query term, invisible on short queries but drifting long ones. Fix: accumulate the per-term idf*tf_norm at full scale and divide by SCALE once at the end (saturating throughout).

Final, all three datasets, after both fixes — faithful float-BM25 parity:

dataset	Yuva NDCG@10	float	fidelity
NFCorpus	0.3051	0.3052	0.999
SciFact	0.6634	0.6625	0.997
ArguAna	0.3552	0.3551	0.996

Identical to bm25_term_score for a single-term query, so the kernel's single-token path (which calls bm25_idf, not bm25_doc_score) and the multi-term recall_selftest KAT (relational asserts A>B, A>C, b_plus>=B — robust to the ≤1 per-score shift) are unaffected. kani_recall_doc_score_accumulation_monotone + host tests + clippy all green locally.