TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Independent generation success and verifier false-acceptance bounds

Statement

Fix a prompt $q$ , a budget $N \geq 1$ , and the finite response law, correctness predicate, and verifier from the generation protocol. In part 1, $Y_{1}, \dots, Y_{N}$ are independent draws from that law and $p : = \Pr (C_{q} (Y_{1}) = 1)$ is their common one-draw correctness probability. Parts 2 and 3 state their own sampling hypotheses.

If $A_{q} = C_{q}$ , rejection search returns an accepted response with probability $1 - (1 - p)^{N}$ .
For any rule that selects one of these $N$ candidates and reports it as accepted only when its verifier value is $1$ , if each draw satisfies $\Pr (A_{q} (Y_{i}) = 1, C_{q} (Y_{i}) = 0) \leq ϵ$ , then the probability of outputting an accepted but incorrect response is at most $N ϵ$ . This bound does not require independent draws.
For an adaptive sampler, let $p \in [0, 1]$ . Suppose that for every $i \leq N$ and every positive-probability history $h = (Y_{1}, \dots, Y_{i - 1})$ with no earlier correct response, the conditional probability of correctness at draw $i$ is at least $p$ . Then the probability of no correct response in the first $N$ draws is at most $(1 - p)^{N}$ .

Statement references

Finite response law, correctness predicate, and verifier.

Rejection search returns the first verifier-accepted sample, or failure after the budget.

DeepSeek-AI, DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning.

Facts & Assumptions

Given: The finite response law, correctness predicate $C_{q}$ , verifier $A_{q}$ , and budget $N$ . Part 1 assumes independent policy draws; part 2 assumes only the stated per-draw false-acceptance bounds; part 3 assumes the stated adaptive conditional-success bounds.

[F1]

Finite truncated response spaces, correctness predicates, and verifiers: at fixed $q$ , the response set is finite, its mass function is normalized, and $C_{q}, A_{q}$ take values in ${0, 1}$ .

[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 sample with $A_{q} = 1$ or fails after at most $N$ draws.

[F3]

Probability measures and probability spaces and Measures on sigma-algebras: probabilities are countably additive measures of total mass one. Finite additivity follows by padding a finite disjoint family with empty sets; finite subadditivity follows by disjointifying a finite union.

[F4]

Independent random elements and Independent sigma-algebras and independent events: independent draws generate independent sigma-algebras; for events $E_{i}$ determined by distinct draws, $\Pr (⋂_{i} E_{i}) = \prod_{i} \Pr (E_{i})$ .

[F5]

Finite sums and finite products, by recursion: finite sums recurse from $0$ by adding one term. Ordered field: its positive cone is closed under addition and multiplication; induction on a finite list therefore preserves a termwise inequality after multiplying by nonnegative weights and summing.

[A1]

In part 3, $p \in [0, 1]$ and for each positive-probability no-success history $h$ at draw $i$ , $\Pr (C_{q} (Y_{i}) = 1 ∣ h) \geq p$ . For finite histories, this conditional probability is $\Pr (C_{q} (Y_{i}) = 1, h) / \Pr (h)$ .

Proof

Given: The Statement hypotheses, including the finite sample space of at most $N$ responses.

1.1givenF1F2F3F4algebra

Under $A_{q} = C_{q}$ , rejection search succeeds exactly on the event $⋃_{i = 1}^{N} {C_{q} (Y_{i}) = 1}$ . Its complement is the intersection of the $N$ failure events. By independence [F4], that complement has probability $(1 - p)^{N}$ , so the success probability is $1 - (1 - p)^{N}$ .

1.2givenA1F1F3F5algebrainduction

Let $F_{i}$ be the event that the first $i$ adaptive responses are all incorrect, with $F_{0}$ the whole sample space. Enumerate the finite response histories lexicographically using the fixed response list in [F1], and partition $F_{i - 1}$ into its positive-probability histories $h$ . By [A1], $\Pr (C_{q} (Y_{i}) = 0 ∣ h) \leq 1 - p$ for each such history. Multiplying by the nonnegative $\Pr (h)$ and summing over this finite partition preserves the inequality by [F5]; finite additivity gives $\Pr (F_{i}) \leq (1 - p) \sum_{h} \Pr (h) = (1 - p) \Pr (F_{i - 1})$ . Induction from $\Pr (F_{0}) = 1$ yields $\Pr (F_{N}) \leq (1 - p)^{N}$ .

2.1givenF1F3F5algebra∎

For each draw let $B_{i} = {A_{q} (Y_{i}) = 1, C_{q} (Y_{i}) = 0}$ . Any accepted incorrect output selected from the $N$ candidates lies in $⋃_{i = 1}^{N} B_{i}$ . For every outcome, $1_{\cup_{i} B_{i}} \leq \sum_{i = 1}^{N} 1_{B_{i}}$ ; summing this pointwise inequality against the nonnegative finite outcome masses gives $\Pr (⋃_{i} B_{i}) \leq \sum_{i = 1}^{N} \Pr (B_{i}) \leq N ϵ$ . Thus the false-acceptance probability is at most $N ϵ$ . No factorization or independence is used in this step.

Depends on

Used by

Dependency tree · two levels

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

Sources

DeepSeek-AI, DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning, original arXiv v1 (standard reference, not scraped)