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.

Perfect and false-positive verifiers have different rejection outcomes

Example

Let a prompt have one correct response $c$ with probability $3 / 4$ and one incorrect response $w$ with probability $1 / 4$ . With a perfect verifier $A = C$ , rejection search with budget $N = 2$ returns an accepted response with probability $15 / 16$ . With a false-positive verifier that accepts both $c$ and $w$ , rejection search always returns its first draw, so its false-acceptance probability is $1 / 4$ ; the per-draw union bound gives $2 (1 / 4) = 1 / 2$ .

Example references

Rejection search returns the first accepted response within its draw budget.

The independent success formula and the false-acceptance union bound.

Facts & Assumptions

Given: A finite two-response law with $\Pr (Y = c) = 3 / 4$ , $\Pr (Y = w) = 1 / 4$ , $C (c) = 1$ , $C (w) = 0$ , rejection budget $N = 2$ , and the two stated verifier choices.

[F1]

Finite truncated response spaces, correctness predicates, and verifiers: correctness and verifier outputs are 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 response accepted by $A$ , or failure after $N$ draws.

[F3]

Independent generation success and verifier false-acceptance bounds: with a perfect verifier, independent rejection succeeds with probability $1 - (1 - p)^{N}$ .

[F4]

Independent generation success and verifier false-acceptance bounds: if each draw has false-acceptance probability at most $ϵ$ , an accepted but incorrect selected output has probability at most $N ϵ$ .

Verification

Given: The objects and hypotheses in the Example.

1.1givenF1F2F3algebra

For the perfect verifier, $p = 3 / 4$ and rejection succeeds iff at least one of the two independent draws is $c$ . Its failure probability is $(1 - 3 / 4)^{2} = 1 / 16$ , so its success probability is $15 / 16$ .

2.1givenF1F2F4algebra∎

For the accept-all verifier, the first draw is always accepted. It is incorrect exactly when it is $w$ , an event of probability $1 / 4$ . Each draw has false-acceptance probability $ϵ = 1 / 4$ , so [F4] gives the valid bound $N ϵ = 1 / 2$ ; the exact first-draw probability $1 / 4$ is below it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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.