ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Pass-at-one, oracle pass-at-N, and verifier-selected accuracy differ

Example

For one prompt let the finite response law assign mass $1 / 4$ to a correct response $c$ and mass $3 / 8$ to each of two incorrect responses $w_{1}, w_{2}$ . Let the verifier accept $c$ and $w_{1}$ but reject $w_{2}$ . The single-response pass@1 rate is $1 / 4$ ; for any integer $M \geq 1$ , the empirical pass@1 over $M$ independent replicas from this same law has expectation $1 / 4$ . Oracle pass@2, the event that at least one of two independent candidates is correct, has probability $7 / 16$ . For the same two candidates, use rejection search with budget $N = 2$ ; its verifier-selected accuracy, the probability its output is correct conditional on being accepted, is $2 / 5$ .

Example references

The finite law, correctness predicate, and verifier.

Rejection search returns the first accepted response or explicit failure.

The perfect-verifier rejection formula and general false-acceptance bound.

Facts & Assumptions

Given: The response probabilities, $C (c) = 1$ , $C (w_{1}) = C (w_{2}) = 0$ , $A (c) = A (w_{1}) = 1$ , $A (w_{2}) = 0$ , an integer $M \geq 1$ with $M$ independent replicas from this response law when computing empirical pass@1, two independent candidates, and rejection search with budget $N = 2$ on those candidates.

[F1]

Finite truncated response spaces, correctness predicates, and verifiers: correctness and acceptance are separate binary functions on the finite response set.

[F2]

Budgeted verifier-guided generation and best-of-N sampling Budgeted verifier generation terminates with bounded response and selection calls: rejection search returns the first verifier-accepted response, or failure if all $N$ draws are rejected.

[F4]

Finite sums and finite products, by recursion: the empirical pass@1 rate is the finite average of the single-sample correctness indicators, with sums defined recursively. Field supplies distributivity for finite expansions over the response list.

[F5]

Expectation of a real random variable on a finite probability space: expectation on the finite sample space of the $M$ replicas is the probability-weighted sum over its outcomes.

[F6]

Linearity, monotonicity, and the modulus bound for expectation: expectation is linear for integrable random variables on a common probability space.

[F7]

Finite truncated response spaces, correctness predicates, and verifiers: the response law is a normalized mass function on the finite response set.

[F8]

Finite truncated response spaces, correctness predicates, and verifiers: independent responses from that law have the product joint mass.

Verification

Given: The objects and sampling rule in the Example.

1.1givenF1F4F5F6F7F8algebrainduction

A single sample is correct exactly when it is $c$ , so its pass@1 probability is $1 / 4$ . The $M$ replicas have joint mass $\prod_{m = 1}^{M} π (y_{m})$ on the finite product $Y_{q}^{M}$ by [F8]. For one coordinate the total mass is $\sum_{y} π (y) = 1$ by [F7]. When one more coordinate is added, distributivity in [F4] factors its finite sum as another factor $\sum_{y} π (y) = 1$ ; induction therefore shows the total mass on $Y_{q}^{M}$ is $1$ . If one coordinate is fixed at $y$ , summing each of the other $M - 1$ coordinates contributes a factor $1$ , so that coordinate has marginal mass $π (y)$ . Thus this is a finite probability space and each correctness indicator has expectation $1 / 4$ . The indicators and their average are bounded and integrable; by [F5]–[F6] the average's expectation is the average of their expectations, also $1 / 4$ .

1.2givenF1F4F8algebra

Neither candidate is correct exactly when both lie in ${w_{1}, w_{2}}$ . Summing the four pair masses from [F8] and factoring by distributivity in [F4] gives probability $(3 / 8 + 3 / 8)^{2} = 9 / 16$ . The complementary oracle pass@2 event therefore has probability $1 - 9 / 16 = 7 / 16$ .

1.3givenF1F2F8algebra

A response is accepted with probability $1 / 4 + 3 / 8 = 5 / 8$ . By the product law for independent candidates [F8], rejection search fails only if both candidates are $w_{2}$ , which has probability $(3 / 8)^{2} = 9 / 64$ , so the probability it returns an accepted response is $55 / 64$ .

2.1givenF1F2F8step 1.3algebra∎

By [F8], it returns a correct response if the first draw is $c$ , or if the first is rejected $w_{2}$ and the second is $c$ , an event of probability $1 / 4 + (3 / 8) (1 / 4) = 11 / 32 = 22 / 64$ . Conditional on an accepted output, the selected accuracy is therefore $(22 / 64) / (55 / 64) = 2 / 5$ , distinct from the pass@1 and oracle pass@2 values above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.