Ring-2 Premise Precision Recall

Premise-retrieval precision and recall replay

It replays copied premise-retrieval records after the fact and reports, problem by problem, how much of the needed support the search actually ranked. ring2_premise_retrieval_precision_recall_harness scores saved premise-retrieval runs after the fact. A proof search first looks for the supporting facts a proof will need, the premises. This component replays copied records of that search and reports, problem by problem, how much of the needed support the search actually ranked.

It keeps two failures apart, a missed premise versus a proof that had everything and still failed, by computing precision and recall and labelling each problem one of four outcomes. The point is to keep two failures apart. A proof can fail because the search never surfaced a premise it needed. A proof can also fail even though every needed premise was ranked. Those call for different fixes. The component computes precision and recall from the copied records, then labels each problem as one of four outcomes so a reader can tell which case they are looking at.

It emits measurement result records, bounded evidence authority, and the labels may never flow back into the ranking or into a provider recipe. It emits result records, bounded evidence authority. The labels are measurement labels. They score a finished run and they are never allowed to flow back into the ranking or into a provider recipe.

Purpose

Blaming the prover hides a missed premise

A failed search invites blaming the prover, but a single reported precision figure cannot say whether the fault was a missed premise or a proof that had everything and still failed. When a proof search fails it is easy to blame the prover and miss the simpler cause: the right facts were never put in front of it. A single reported precision figure hides this. It cannot say whether a low score came from a missed premise or from a proof that had everything it needed and still did not go through.

Recomputed overlap read against proof outcome

It recomputes the numbers by intersecting ranked ids with needed ids and reading the proof outcome, so full recall with a failing proof surfaces as a downstream fault. So the component recomputes the numbers rather than trusting a reported one. For each problem it intersects the ranked premise ids with the labelled needed-premise ids and reads the proof outcome alongside that overlap. Full recall with a passing proof is one outcome; full recall with a failing proof is a different one. That second case is the signal that the fault lies downstream of retrieval, and a loose metric that only averages scores would erase it.

How it works

Two entrypoints over one _build_result

run validates the fixture with five negative cases and run_precision_recall_bundle validates the export without them, both calling _build_result to set one PASS or blocked status. Two entrypoints drive the same core. run validates a fixture directory with the five negative cases included. run_precision_recall_bundle validates an exported bundle with the negative cases turned off. Both call _build_result, which runs the stages below in order and decides a single status of PASS or blocked.

Precision and recall at a top-k cutoff

_evaluate truncates each ranking to top_k, intersects ranked with needed ids for hits, and computes precision and recall against the policy's expected aggregates. The scoring core is _evaluate. It indexes the after-the-fact labels by problem_id, reads default_top_k from the policy (4 if unset) or a per-ranking top_k, and truncates each ranking to that cutoff. It intersects the truncated ranked ids with the labelled needed ids to get the hits, then computes precision = hits / top_k and recall = hits / needed. Aggregate precision and recall come from summed hit, candidate, and needed counts, and are compared against the policy's expected_aggregate_metrics.

The four-way label is mechanical, driven by recall and the recorded proof_outcome: The four-way label is mechanical, driven by recall and the recorded proof_outcome:

• retrieval_hit: recall reached 1.0 and the proof passed.
• proof_failure_despite_hit: recall reached 1.0 but the proof did not pass. Retrieval did its job; the fault is elsewhere.
• partial_retrieval_miss: some needed premises were ranked, not all.
• retrieval_miss: none of the needed premises were ranked.

Enforcing the shape of the evaluation set

_evaluate also requires every expected failure mode, an adversarial decoy problem, and the minimum problem count, turning any gap into a finding. _evaluate also enforces the shape of the evaluation set, not just the happy path. It requires every mode named in the policy's expected_failure_modes to appear, requires an adversarial decoy problem whose needed premise is absent or missed, and requires the policy's minimum problem count. A gap in any of these becomes a finding.

Provenance and digest checks gate the status

Before any score is trusted, _validate_run_material and _validate_source_artifacts check provenance and digests, and status is PASS only when every stage and the secret scan clear. Before any score is trusted, the provenance stages run. _validate_run_material rejects copied material that is missing a source_ref, source_sha256, target_refs, validation_refs, or the expected copied_non_secret_macro_body_with_provenance status. _validate_source_artifacts walks the four files in SOURCE_REFS, hashes each copied artifact under source_artifacts/, and accepts it only if the hash matches the recorded exact digest in SOURCE_DIGESTS or a known path-rewrite digest. A missing file or a hash mismatch is a finding. _build_result also runs a secret-exclusion scan over the inputs. The overall status is PASS only when there are no floor findings, no run-material findings, the source artifacts pass, the evaluation passes, no expected negative case is missing, and the secret scan has no blocking hit. Otherwise it stays blocked.

Result records expose metrics, never proof bodies

_write_receipts emits import ids, target refs, digest status, and metric counts, but writes no proof bodies, model-output data, or non-public paths. _write_receipts then emits the records. It exposes import ids, target refs, digest status, aggregate metrics, and failure-mode counts. It does not write proof bodies, model-output data, or non-public paths.

flowchart TD Inputs["four input files runs, labels, rankings, policy"] --> Build["_build_result orchestrates stages, sets status"] Build --> Evaluate["_evaluate precision/recall + four-way label"] Build --> RunMat["_validate_run_material copied-material provenance"] Build --> Artifacts["_validate_source_artifacts digest match per file"] Build --> Negatives["_negative_findings five typed refusals"] Evaluate --> Status["status: PASS or blocked"] RunMat --> Status Artifacts --> Status Negatives --> Status Status --> Result records["_write_receipts metrics only, no proof bodies"]

Negative cases

EXPECTED_NEGATIVE_CASES names five adversarial inputs that run must reject, each mapped to one refusal code: EXPECTED_NEGATIVE_CASES names five adversarial inputs that run must reject, each mapped to one refusal code:

• oracle_labels_in_ranking plants the known-correct premise ids inside a ranking. _inspect_forbidden_bodies catches the oracle_needed_premise_ids field and emits RING2_RETRIEVAL_ORACLE_LABELS_IN_RANKING.
• proof_body_leakage carries a proof, provider, or private body field and emits RING2_RETRIEVAL_PROOF_BODY_FORBIDDEN.
• test_split_tuning_attempt marks a run as tuned on the test labels and emits RING2_RETRIEVAL_TEST_SPLIT_TUNING_FORBIDDEN.
• metric_overclaim asserts proof, benchmark, provider, or launch-scope decision and emits RING2_RETRIEVAL_METRIC_OVERCLAIM.
• missing_adversarial_decoy omits the required decoy case and emits RING2_RETRIEVAL_ADVERSARIAL_DECOY_REQUIRED.

Missing negative cases block the run

If any of the five is not observed, _build_result records it as missing and the run is blocked. If any of the five is not observed, _build_result records it as missing and the run is blocked.

Prior Art Grounding

Grounded in IR metrics and premise selection

The design draws on TREC and scikit-learn precision/recall evaluation and on hammer-style premise selection, where finding the right facts is a distinct step from replaying a proof. This component is grounded in information-retrieval evaluation. NIST's TREC evaluation measures give the older precision/recall frame for judging retrieval systems, and scikit-learn's precision/recall metric API is a common machine-learning interface for reporting those labels. On the theorem-proving side, premise selection sits next to hammer workflows such as Isabelle Sledgehammer, where finding the right facts is a distinct step from replaying a proof. This component keeps that distinction explicit and measurable.

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary records:

What a pass over the records means

A pass means the records scored to expectation, the four digests matched, and all five negative cases were rejected, without anything running Lean or a prover. A pass means the copied records scored to their expected metrics, the four source artifacts matched their digests, and all five negative cases were rejected. It does not mean anything ran Lean or a prover.