ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

The convex constant-step stability bound is linear in the step count

Example

Let $n, T, d \geq 1$ , $L, β > 0$ , and let $(X, Σ_{X})$ , $(Y, Σ_{Y})$ , and $(A, Σ_{A})$ be measurable spaces. Let $P$ be a probability measure on $X \times Y$ , let $ℓ : A \times Y \to [0, + \infty)$ be measurable, and let $f_{w} : X \to A$ be measurable for every $w \in R^{d}$ . For $z = (x, y)$ put $g (w, z) = ℓ (f_{w} (x), y)$ and assume $g$ and $\nabla_{w} g$ are jointly measurable. For every $z$ , assume $g (\cdot, z)$ is totally differentiable and convex, its gradient is $β$ -Lipschitz, and its values satisfy $∣ g (w, z) - g (v, z) ∣ \leq L ∥ w - v ∥_{2}$ . Let $S = (Z_{1}, \dots, Z_{n})$ be IID with law $P$ , and define $R_{P} (f_{w}) = \int g (w, z) P (d z)$ and ${\hat{R}}_{S} (f_{w}) = n^{- 1} \sum_{i = 1}^{n} g (w, Z_{i})$ . Let $I_{1}, \dots, I_{T}$ be independent of $S$ with $P (I_{t} = i) = 1 / n$ for each $t, i$ ; dependence across times is allowed. From fixed $w_{0} \in R^{d}$ , run $w_{t} = w_{t - 1} - α_{t} \nabla_{w} g (w_{t - 1}, Z_{I_{t}})$ and assume the resulting loss and risk maps are measurable and integrable. For the constant schedule $α_{t} = 1 / β$ , the stability and absolute expected-generalization upper bound is $2 L^{2} T / (β n)$ , which is linear in $T$ as a bound. This is an upper-bound calculation, not a lower bound on the actual stability or generalization gap.

Example references

Expected generalization of convex stochastic gradient training supplies the convex SGD stability and expected-gap bound.

Hardt, Recht, and Singer, arXiv-version Theorem 3.8 (conference Theorem 3.7): full arXiv paper.

Facts & Assumptions

Given: $n, T \geq 1$ , $L, β > 0$ , the convex theorem hypotheses, and the constant schedule $α_{t} = 1 / β$ .

[F1]

Expected generalization of convex stochastic gradient training: for admissible deterministic steps, stability and the absolute expected-generalization gap are at most $\frac{2 L^{2}}{n} \sum_{t = 1}^{T} α_{t}$ .

Verification

1.1givenF1algebra

Since $α_{t} = 1 / β \leq 2 / β$ , every step meets the convex theorem's step-size condition. The sum of the $T$ equal steps is $T / β$ .

2.1F1step 1.1algebra

Substituting this sum into [F1] gives $ε_{s t a b} \leq \frac{2 L^{2}}{n} \frac{T}{β} = \frac{2 L^{2} T}{β n}$ .

3.1givenstep 2.1algebra∎

For fixed positive $L, β, n$ , the displayed right-hand side is a constant multiple of $T$ . It bounds the stability and expected gap from above and yields no corresponding lower bound.

Depends on

Expected generalization of convex stochastic gradient training

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Moritz Hardt, Benjamin Recht, and Yoram Singer, Train faster, generalize better: Stability of stochastic gradient descent, arXiv-version Theorem 3.8 (conference Theorem 3.7) (standard reference, not scraped)