Mathematical Proof for ML
This skill turns you into a rigorous ML theorist. It covers strategy selection, proof
construction, verification, and the bridge from theory to design decisions.
Follow NeurIPS/ICML/ICLR standards throughout.
Proof Strategy Selection
Choose based on the claim structure — don't default to direct proof:
| Claim Pattern |
Strategy |
Why |
| "Algorithm converges in $T$ steps" |
Induction on iteration count |
Base case = initialization, inductive step = per-iteration progress |
| "No algorithm can achieve error $< \varepsilon$" |
Contradiction — assume one does, derive impossible bound |
Lower bounds almost always need contradiction or information theory |
| "This estimator generalizes" |
Probabilistic — concentration + union bound or PAC-Bayes |
Generalization is inherently statistical |
| "Architecture $X$ is equivariant to group $G$" |
Direct — verify $f(g \cdot x) = g \cdot f(x)$ for generators of $G$ |
Algebraic — just check the group action commutes |
| "Gradient flow doesn't vanish" |
Constructive — exhibit a Jacobian bound bounded away from 0 |
Need concrete bounds, not existence |
| "Method A is strictly better than B" |
Separation — construct an instance where A succeeds and B fails |
Needs a concrete counterexample for B |
| "Network can approximate any continuous function" |
Density argument — Stone-Weierstrass or constructive approximation |
Show the function class is dense in $C(K)$ under sup-norm |
| "Loss landscape has no spurious local minima" |
Landscape analysis — characterize critical points via Hessian |
Show every local min is global, or every saddle has a negative eigenvalue |
| "Generative model learns the target distribution" |
Coupling / OT argument — bound Wasserstein or KL between model and target |
Transport inequalities connect optimization to distribution distance |
| "Adaptive method matches lower bound over $T$ steps" |
Amortized analysis — potential function argument |
Per-step costs vary but total is controlled by potential |
| "Score estimator converges to true score" |
Denoising score matching equivalence — show $\mathbb{E}[|s_\theta - \nabla \log p_\sigma|^2]$ equals DSM objective up to constant |
Avoids intractable $\nabla \log p$; reduces to regression |
Proof Construction Workflow
Step 1: Formalize
Convert intuition into a formal statement with explicit quantifiers.
- Bad: "Attention helps with long-range dependencies"
- Good: "For input $x \in \mathbb{R}^{L \times d}$, self-attention computes pairwise interactions in $O(L^2 d_k)$ time, and $\partial \text{attn}(x)_i / \partial x_j \neq 0$ for all $i, j$"
Every symbol must be defined. Every quantifier (for all, there exists) must be explicit.
Step 2: List assumptions
Every assumption you omit is a gap reviewers will find. Common categories:
- Smoothness: L-smooth? mu-strongly convex? Both? Polyak-Lojasiewicz?
- Boundedness: Bounded gradients? Bounded domain? Bounded variance sigma^2?
- Statistical: i.i.d.? Sub-Gaussian noise? Bounded moments? Log-Sobolev constant?
- Structural: Full rank? Positive definite? Connected graph? Finite covering number?
- Generative: Forward process well-defined? Score function in L^2? Lipschitz drift?
Step 3: Execute with citations
Each step cites the lemma or assumption it uses. No "it is easy to see" — either cite or prove inline.
Read the appropriate reference file for templates and tools:
| Reference |
When to Read |
| references/proof-templates.md |
Convergence proofs, generalization bounds, optimization — has skeletons, worked examples, and the core lemma catalog |
| references/generative-models.md |
Diffusion models, score matching, flow matching, SDE/ODE analysis — has exact formulas for VP-SDE, VE-SDE, DSM loss, CFM loss |
| references/advanced-tools.md |
Rademacher complexity, optimal transport, functional inequalities, NTK, landscape analysis — the advanced toolkit |
Step 4: Verify tightness
This is not optional — a bound without tightness analysis is incomplete.
Tightness verification protocol:
Construct a matching instance. If the bound says $O(1/\sqrt{T})$, exhibit a concrete problem where the actual rate is $\Omega(1/\sqrt{T})$. For GD on strongly convex functions, a quadratic $f(w) = \frac{L}{2}w_1^2 + \frac{\mu}{2}w_2^2$ achieves the exact rate.
Check known lower bounds. Does an information-theoretic or oracle-complexity lower bound exist? If your upper bound matches it, state so. If there's a gap, quantify it.
Vacuousness check. Plug in realistic numbers (e.g., $n = 50\text{K}$ samples, $d = 100\text{M}$ parameters). If the generalization bound exceeds 1 (or the convergence time exceeds $10^{20}$), the bound is vacuous for practice — say so honestly.
State the gap. If the bound is not tight, write: "Gap: upper bound is O(X), best known lower bound is Omega(Y). Closing this gap requires [specific technique or open problem]."
Step 5: Proof-to-Design Bridge
Every theorem should connect back to design decisions. Answer:
- What hyperparameter choices does this bound recommend? (e.g., $\eta = 1/L$, temperature $= \sqrt{d}$)
- What architecture properties does this justify? (e.g., Lipschitz bound justifies QK-normalization)
- When do the assumptions break down? (e.g., strong convexity fails for deep nets, bounded gradients fail with gradient clipping off)
- Is there a practical takeaway? (e.g., "the $1/\sqrt{T}$ rate means diminishing returns after ~10K steps for this loss scale")
| Proof Result |
Design Implication |
| Attention Lipschitz constant $\sim |V| / \sqrt{d}$ |
Use QK-normalization; scale temperature with depth |
| PAC-Bayes: tighter when $\text{KL}(Q | P)$ is small |
Match architecture to data structure (convolutions for images, transformers for sequences) |
| Adam convergence degrades with dimension $d$ |
Consider parameter-efficient methods (LoRA) for very large models |
| NTK becomes constant at infinite width |
Wider networks train more like kernel methods — predictable but less expressive |
| Scaling law: $L \sim A/N^{0.34} + B/D^{0.28}$ |
Allocate compute equally between parameters and data (Chinchilla) |
| Score matching error propagates as $O(\varepsilon \cdot T)$ in diffusion |
Use fewer diffusion steps; prefer flow matching (linear error propagation) |
| PL condition gives linear convergence without convexity |
Overparameterized nets may converge fast even though loss is non-convex |
Output Format
**Theorem.** [Formal statement with quantifiers]
*Assumptions:*
1. [Assumption with mathematical notation]
2. ...
*Proof.*
Step 1: [Description]
[Math] — by [Assumption N / Lemma / named theorem]
Step 2: ...
QED
*Tightness:* [Matching lower bound or explicit gap statement]
*Practical implication:* [Design decision this informs]
Common Pitfalls
- Forgetting quantifiers — "for all epsilon > 0" vs. "there exists epsilon > 0" invalidates the entire proof
- Circular reasoning — especially in inductive proofs where the inductive hypothesis is misapplied
- Dropping constants — O-notation is fine for rates, but exact constants matter for step-size recommendations
- Wrong inequality direction — double-check every <= vs >= after applying an inequality
- Vacuous bounds — many generalization bounds give values > 1 for realistic networks; acknowledge this honestly
- Ignoring the score regularity — in diffusion/score matching proofs, $\nabla \log p_t$ may not exist or be in $L^2$ without explicit assumptions on the data distribution
- Confusing convergence in distribution vs. in parameters — NTK convergence is about function space, not weight space
- Applying concentration to dependent random variables — McDiarmid requires independence; for dependent data, use mixing conditions or other tools
1---2name: math-proof3description: Construct, verify, and communicate mathematical proofs for ML theory — convergence rates, generalization bounds, architecture properties, optimization analysis, generative model theory, and scaling laws. Use when the user asks to prove a theorem about an ML algorithm, verify a convergence bound, analyze Lipschitz properties of a network, derive generalization guarantees, prove properties of diffusion models or flow matching, analyze NTK behavior, construct universal approximation arguments, or build any rigorous mathematical argument in the context of machine learning. Also trigger on: convergence proof, generalization bound, PAC-Bayes, Lipschitz analysis, gradient flow proof, lower bound, concentration inequality, optimization theory, induction on iterations, equivariance proof, score matching, diffusion SDE, flow matching, NTK, neural tangent kernel, Rademacher complexity, Wasserstein distance, optimal transport, scaling law, universal approximation, loss landscape, PL condition.4---56# Mathematical Proof for ML78This skill turns you into a rigorous ML theorist. It covers **strategy selection**, **proof9construction**, **verification**, and the **bridge from theory to design decisions**.1011Follow NeurIPS/ICML/ICLR standards throughout.1213---1415## Proof Strategy Selection1617Choose based on the claim structure — don't default to direct proof:1819| Claim Pattern | Strategy | Why |20|--------------|----------|-----|21| "Algorithm converges in $T$ steps" | **Induction** on iteration count | Base case = initialization, inductive step = per-iteration progress |22| "No algorithm can achieve error $< \varepsilon$" | **Contradiction** — assume one does, derive impossible bound | Lower bounds almost always need contradiction or information theory |23| "This estimator generalizes" | **Probabilistic** — concentration + union bound or PAC-Bayes | Generalization is inherently statistical |24| "Architecture $X$ is equivariant to group $G$" | **Direct** — verify $f(g \cdot x) = g \cdot f(x)$ for generators of $G$ | Algebraic — just check the group action commutes |25| "Gradient flow doesn't vanish" | **Constructive** — exhibit a Jacobian bound bounded away from 0 | Need concrete bounds, not existence |26| "Method A is strictly better than B" | **Separation** — construct an instance where A succeeds and B fails | Needs a concrete counterexample for B |27| "Network can approximate any continuous function" | **Density argument** — Stone-Weierstrass or constructive approximation | Show the function class is dense in $C(K)$ under sup-norm |28| "Loss landscape has no spurious local minima" | **Landscape analysis** — characterize critical points via Hessian | Show every local min is global, or every saddle has a negative eigenvalue |29| "Generative model learns the target distribution" | **Coupling / OT argument** — bound Wasserstein or KL between model and target | Transport inequalities connect optimization to distribution distance |30| "Adaptive method matches lower bound over $T$ steps" | **Amortized analysis** — potential function argument | Per-step costs vary but total is controlled by potential |31| "Score estimator converges to true score" | **Denoising score matching equivalence** — show $\mathbb{E}[\|s_\theta - \nabla \log p_\sigma\|^2]$ equals DSM objective up to constant | Avoids intractable $\nabla \log p$; reduces to regression |3233---3435## Proof Construction Workflow3637### Step 1: Formalize3839Convert intuition into a formal statement with explicit quantifiers.4041- Bad: "Attention helps with long-range dependencies"42- Good: "For input $x \in \mathbb{R}^{L \times d}$, self-attention computes pairwise interactions in $O(L^2 d_k)$ time, and $\partial \text{attn}(x)_i / \partial x_j \neq 0$ for all $i, j$"4344Every symbol must be defined. Every quantifier (for all, there exists) must be explicit.4546### Step 2: List assumptions4748Every assumption you omit is a gap reviewers will find. Common categories:4950- **Smoothness**: L-smooth? mu-strongly convex? Both? Polyak-Lojasiewicz?51- **Boundedness**: Bounded gradients? Bounded domain? Bounded variance sigma^2?52- **Statistical**: i.i.d.? Sub-Gaussian noise? Bounded moments? Log-Sobolev constant?53- **Structural**: Full rank? Positive definite? Connected graph? Finite covering number?54- **Generative**: Forward process well-defined? Score function in L^2? Lipschitz drift?5556### Step 3: Execute with citations5758Each step cites the lemma or assumption it uses. No "it is easy to see" — either cite or prove inline.5960Read the appropriate reference file for templates and tools:6162| Reference | When to Read |63|-----------|-------------|64| [references/proof-templates.md](references/proof-templates.md) | Convergence proofs, generalization bounds, optimization — has skeletons, worked examples, and the core lemma catalog |65| [references/generative-models.md](references/generative-models.md) | Diffusion models, score matching, flow matching, SDE/ODE analysis — has exact formulas for VP-SDE, VE-SDE, DSM loss, CFM loss |66| [references/advanced-tools.md](references/advanced-tools.md) | Rademacher complexity, optimal transport, functional inequalities, NTK, landscape analysis — the advanced toolkit |6768### Step 4: Verify tightness6970This is not optional — a bound without tightness analysis is incomplete.7172**Tightness verification protocol:**73741. **Construct a matching instance.** If the bound says $O(1/\sqrt{T})$, exhibit a concrete problem where the actual rate is $\Omega(1/\sqrt{T})$. For GD on strongly convex functions, a quadratic $f(w) = \frac{L}{2}w_1^2 + \frac{\mu}{2}w_2^2$ achieves the exact rate.75762. **Check known lower bounds.** Does an information-theoretic or oracle-complexity lower bound exist? If your upper bound matches it, state so. If there's a gap, quantify it.77783. **Vacuousness check.** Plug in realistic numbers (e.g., $n = 50\text{K}$ samples, $d = 100\text{M}$ parameters). If the generalization bound exceeds 1 (or the convergence time exceeds $10^{20}$), the bound is vacuous for practice — say so honestly.79804. **State the gap.** If the bound is not tight, write: "Gap: upper bound is O(X), best known lower bound is Omega(Y). Closing this gap requires [specific technique or open problem]."8182### Step 5: Proof-to-Design Bridge8384Every theorem should connect back to design decisions. Answer:85861. **What hyperparameter choices does this bound recommend?** (e.g., $\eta = 1/L$, temperature $= \sqrt{d}$)872. **What architecture properties does this justify?** (e.g., Lipschitz bound justifies QK-normalization)883. **When do the assumptions break down?** (e.g., strong convexity fails for deep nets, bounded gradients fail with gradient clipping off)894. **Is there a practical takeaway?** (e.g., "the $1/\sqrt{T}$ rate means diminishing returns after ~10K steps for this loss scale")9091| Proof Result | Design Implication |92|-------------|-------------------|93| Attention Lipschitz constant $\sim \|V\| / \sqrt{d}$ | Use QK-normalization; scale temperature with depth |94| PAC-Bayes: tighter when $\text{KL}(Q \| P)$ is small | Match architecture to data structure (convolutions for images, transformers for sequences) |95| Adam convergence degrades with dimension $d$ | Consider parameter-efficient methods (LoRA) for very large models |96| NTK becomes constant at infinite width | Wider networks train more like kernel methods — predictable but less expressive |97| Scaling law: $L \sim A/N^{0.34} + B/D^{0.28}$ | Allocate compute equally between parameters and data (Chinchilla) |98| Score matching error propagates as $O(\varepsilon \cdot T)$ in diffusion | Use fewer diffusion steps; prefer flow matching (linear error propagation) |99| PL condition gives linear convergence without convexity | Overparameterized nets may converge fast even though loss is non-convex |100101---102103## Output Format104105```106**Theorem.** [Formal statement with quantifiers]107108*Assumptions:*1091. [Assumption with mathematical notation]1102. ...111112*Proof.*113Step 1: [Description]114 [Math] — by [Assumption N / Lemma / named theorem]115116Step 2: ...117118QED119120*Tightness:* [Matching lower bound or explicit gap statement]121*Practical implication:* [Design decision this informs]122```123124---125126## Common Pitfalls1271281. **Forgetting quantifiers** — "for all epsilon > 0" vs. "there exists epsilon > 0" invalidates the entire proof1292. **Circular reasoning** — especially in inductive proofs where the inductive hypothesis is misapplied1303. **Dropping constants** — O-notation is fine for rates, but exact constants matter for step-size recommendations1314. **Wrong inequality direction** — double-check every <= vs >= after applying an inequality1325. **Vacuous bounds** — many generalization bounds give values > 1 for realistic networks; acknowledge this honestly1336. **Ignoring the score regularity** — in diffusion/score matching proofs, $\nabla \log p_t$ may not exist or be in $L^2$ without explicit assumptions on the data distribution1347. **Confusing convergence in distribution vs. in parameters** — NTK convergence is about function space, not weight space1358. **Applying concentration to dependent random variables** — McDiarmid requires independence; for dependent data, use mixing conditions or other tools
guliqianxun