docs/benchmark-evolution-doctrine.md

Benchmark evolution doctrine

A11oy benchmark claims are evidence artifacts, not slogans. A run is publishable only when the corpus, route, judge panel, receipts, and raw results are immutable and replayable.

This doctrine covers competition-math goals in agi-forecast, theorem/runtime routes in lutar-lean and a11oy, and any future Hugging Face test-results mirror.

Corpus immutability

• Every corpus has a stable corpusId, corpusVersion, sourceUri, license, canonicalization, sha256 or externally declared digest, and problem-count manifest.
• A changed prompt, solution, rubric, split, metadata row, or canonicalization rule creates a new corpusVersion.
• Old corpora are never overwritten. They may be deprecated by pointer only.
• competition-math problem text may be stored only when license permits. Otherwise store official/source pointers, metadata, and content digests.

Competition-math raw-score honesty

• Report competition-math benchmark results as raw points: earned_points / possible_points, with year/problem breakdown.
• Do not say “solved the benchmark” unless a sealed, pre-registered corpus reaches a declared threshold with receipts, reproducible tooling, and unanimous headline judge agreement.
• Separate answer correctness, proof validity, Lean/formal verification, runtime formula routing, and provenance compliance.
• Publish failed attempts, retries, time budgets, tool use, and judge disagreements.

Formula routing

Each benchmark item may route to zero or more formulas:

• FalsePosition
• MadhavaBound
• LiuHuiPi
• SummationInvariant
• AdversarialRobustness
• QECLineage
• ReceiptSubstrate

A formula route is advisory unless backed by:

1. a theorem-runtime manifest ID;
2. a runtime file;
3. a test file;
4. a validation command;
5. a current claim status.

Ancient or historical lineage never gives benchmark credit by itself.

Multi-judge panels

Minimum panel:

Judge	Role
raw_grader	Scores final answer against a rubric.
proof_judge	Checks reasoning, theorem use, formalization, or runtime verification.
provenance_judge	Checks receipts, corpus digest, tool budget, and claim wording.

Two-of-three agreement may publish a raw result. Unanimous agreement is required for headline claims.

Receipt requirements

Each run emits JSONL receipts containing:

• runId
• sourceCommit
• benchmarkMapSha256
• corpusSha256 or externalCorpusDigest
• problemId
• promptSha256
• modelId / solverId
• toolPolicy
• attemptNumber
• answerSha256
• judgePanelSha256
• rawScore
• timestamp
• prev_receipt_hash

Receipts must verify as an append-only chain before a result is mirrored.

Hugging Face test-results publication

GitHub remains canonical. Hugging Face can mirror benchmark outputs to a dataset such as SZLHOLDINGS/a11oy-test-results with:

• README.md
• benchmark-map.json
• results/*.jsonl
• receipts/*.jsonl
• MANIFEST.json

The HF dataset must say mirror-not-canonical and point back to GitHub commits, CI runs, receipts, and payload manifests.

CI gates

Block benchmark PRs unless:

• benchmarks/benchmark-map.json validates;
• corpus/result digests match bytes on disk or declared external digests;
• formula routes resolve to docs/theorem-runtime-manifest.json;
• Competition-math benchmark language remains raw-score/staged unless evidence supports more;
• receipt JSONL verifies as append-only;
• HF dry-run includes benchmark/test-results files.

Current state

The current benchmark map is deliberately staged: it defines the operating contract and formula routes, but it does not claim a live benchmark score. The next operational step is a pinned corpus manifest, judge-panel config, and receipt-emitting runner in agi-forecast or a dedicated benchmark package.