Alphabeta MathHow 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.
Reasoning-training evidence and evaluation targets
Reasoning training and evaluation targets
The finite prompt set, response support, token budget, truncation marker, verifier, reward rule, and sampling policy define the distribution to which an evaluation result applies. An empirical pass@1 is the observed fraction of prompts whose single designated sample is correct; oracle pass@N is the fraction with at least one correct response among N candidates; verifier-selected accuracy is the fraction correct among returned responses the verifier accepts. This last fraction is defined only when at least one returned response is accepted; it is undefined when none is accepted. These statistics need not agree, because the verifier can accept an incorrect response, reject a correct one, or select an incorrect candidate even when another candidate in the group is correct.
The proved group-score identity applies only to unnormalized centering under independent draws from the same finite policy. The finite-budget group update additionally divides by a random group standard deviation, clips a sequence-level policy ratio, and reuses samples from a frozen old policy for several inner steps. The identity alone proves no unbiasedness, monotone policy improvement, or convergence claim for that procedure.
For a general finite-horizon offline MDP with fixed stationary target and behavior policies, the cited trajectory-ratio lemma assumes the Axiom of Choice, a shared fixed initial state and transition/reward law, full-horizon absolute continuity, and integrability of the target return or other function being reweighted. Clipping or self-normalization alters the weights, so that exact change-of-measure identity alone does not establish the corresponding clipped or self-normalized equality or a generic offline-policy safety or performance guarantee. A verifier or benchmark score is an evaluation signal and does not certify a mathematical proof.
Reasoning training and evaluation targets references
The budgeted rejection and best-of-N procedures.
The finite independent and adaptive success bounds and false-acceptance union bound.
The finite sequence-ratio, group-normalized, clipped update procedure.
The exact scope of the unnormalized group-center identity.
The general finite-horizon trajectory ratio under AC and full coverage.
AC asserts that every family of nonempty sets has a choice function.
Absolute continuity means every behavior-null measurable set is also target-null.
A real function is integrable when the integral of its absolute value is finite.
Depends on
- The Axiom of Choice
- Absolute continuity of a signed or complex measure with respect to a positive measure
- Integrable real and complex functions, and their integrals
- Finite-horizon offline reinforcement-learning dataset and coverage
- Budgeted verifier-guided generation and best-of-N sampling
- Independent generation success and verifier false-acceptance bounds
- Finite response likelihood ratios change measure by cancellation
- Finite-budget group-relative policy update
- The group-centered score estimator has factor one minus one over G
- Finite-horizon policy ratios are trajectory Radon-Nikodym derivatives
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
36 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)
- Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, second-edition draft (standard reference, not scraped)
- John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov, Proximal Policy Optimization Algorithms, original arXiv v1 (standard reference, not scraped)