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.
Adam diverges on a periodic bounded-gradient loss sequence
Statement refuted
The claim that bounded gradients alone keep every bias-corrected Adam iterate bounded is false, even in one dimension with fixed parameters beta_1=0, beta_2=1/2, eta=1, and epsilon=1/100.
Facts & Assumptions
Given: Adam is initialized at x_1=m_0=v_0=0 and is fed the finite prefixes of the periodic loss sequence
Each finite prefix is a convex loss sequence and every gradient has magnitude at most 5/2.
Bias-corrected Adam update: Adam uses m_t=beta_1m_{t-1}+(1-beta_1)g_t, v_t=beta_2v_{t-1}+(1-beta_2)g_t^2, bias corrections, and x_{t+1}=x_t-eta mhat_t/(sqrt(vhat_t)+epsilon).
The principle of mathematical induction: a property true at zero and inherited by each successor holds for every natural index.
The Cauchy-sequence reals have the least-upper-bound property establishes that the real field is complete in the sense of Complete ordered field (least-upper-bound property). In particular it is an ordered field, so order is preserved by addition and multiplication by nonnegative numbers; the completeness hypotheses of [F4] and [F8] hold.
Square roots exist: a unique with ; the positives are : each nonnegative real has a unique nonnegative square root.
The natural numbers (von Neumann): time and cycle indices are natural numbers.
Integer powers : beta^t is the integer power of beta at natural time t.
Convex and strictly convex functions on Euclidean convex sets: convexity means the segment inequality for function values.
Every complete ordered field is Archimedean: for every real there is a natural with .
Squaring is monotone on the nonnegatives: on nonnegative reals, implies .
Counterexample
The losses are affine, hence convex by direct substitution in [F7]. With , define , , and . Substituting the three gradients in [F1] gives , , , and . The formula holds at because ; substitution proves the successor formula, so [F2] gives it for every . It yields and , . Also , so for , , where .
Let be the magnitudes of the three Adam updates in cycle , so the cycle change is . For , step 1.1 gives , , and . Since all quantities are nonnegative, [F9] gives the corresponding square-root comparisons. Since , ; with the update magnitudes satisfy , , and . Exact arithmetic gives , so every such cycle increases by at least this amount.
Put . For every , step 2.1 gives , where . Induction gives for each integer . Given any real bound , [F8] supplies an integer ; hence . Thus the terminal subsequence is unbounded above, disproving boundedness from bounded gradients alone.
Remarks
The drift calculation concerns the unprojected Adam update defined in Bias-corrected Adam update on R; no lower-bounded fixed objective or bounded feasible set is assumed. It refutes a blanket bounded-iterate guarantee from bounded gradients alone and makes no claim about Adam on a fixed strongly convex objective.
Depends on
- Bias-corrected Adam update
- The principle of mathematical induction
- Complete ordered field (least-upper-bound property)
- The Cauchy-sequence reals have the least-upper-bound property
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- The natural numbers $\mathbb{N}$ (von Neumann)
- Integer powers $a^m$
- Squaring is monotone on the nonnegatives
- Convex and strictly convex functions on Euclidean convex sets
- Every complete ordered field is Archimedean
Used by
Dependency tree · two levels
41 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
- Sashank J. Reddi, Satyen Kale, and Sanjiv Kumar, On the Convergence of Adam and Beyond, ICLR 2018 (standard reference, not scraped)
- Diederik P. Kingma and Jimmy Ba, Adam: A Method for Stochastic Optimization, ICLR 2015 (standard reference, not scraped)