Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generated
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

ℓ3k+1(x)=52x,ℓ3k+2(x)=ℓ3k+3(x)=−x(k≥0).

Each finite prefix is a convex loss sequence and every gradient has magnitude at most 5/2.

[F1]

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

[F2]

The principle of mathematical induction: a property true at zero and inherited by each successor holds for every natural index.

[F3]

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.

[F5]

The natural numbers N (von Neumann): time and cycle indices are natural numbers.

[F6]

Integer powers am: beta^t is the integer power of beta at natural time t.

[F7]

Convex and strictly convex functions on Euclidean convex sets: convexity means the segment inequality for function values.

[F8]

Every complete ordered field is Archimedean: for every real M there is a natural r with r>M.

[F9]

Squaring is monotone on the nonnegatives: on nonnegative reals, a2<b2 implies a<b.

Counterexample

1.1F1F2F3F5F6F7givenalgebrainduction

The losses are affine, hence convex by direct substitution in [F7]. With β2=1/2, define hk=v3k+1, uk=v3k+2, and wk=v3k+3. Substituting the three gradients in [F1] gives h0=25/8, uk=hk/2+1/2, wk=hk/4+3/4, and hk+1=hk/8+7/2. The formula hk=4−7/8k+1 holds at k=0 because 4−7/8=25/8; substitution proves the successor formula, so [F2] gives it for every k. It yields hk<4 and uk<5/2, wk<7/4. Also hk+1−hk=(7/8)(4−hk)>0, so for k≥2, hk≥h2=4−7/512>3.98, where 7/512<1/50.

2.1F1F3F4F5F6F9step 1.1givenalgebra

Let ak,bk,ck>0 be the magnitudes of the three Adam updates in cycle k, so the cycle change is −ak+bk+ck. For k≥2, step 1.1 gives v^3k+1≥hk>3.98>(1.99)2, v^3k+2≤(5/2)/(1−2−8)=128/51<(8/5)2, and v^3k+3<(7/4)/(1−2−9)=896/511<(7/5)2. Since all quantities are nonnegative, [F9] gives the corresponding square-root comparisons. Since β1=0, m^t=gt; with ϵ=1/100 the update magnitudes satisfy ak<(5/2)/(1.99+0.01)=5/4, bk>1/(8/5+1/100)=100/161, and ck>1/(7/5+1/100)=100/141. Exact arithmetic gives 100/161+100/141−5/4=7295/90804>0, so every such cycle increases x by at least this amount.

3.1F2F3F5F8step 2.1givenalgebrainduction∎

Put Xk=x3k+1. For every k≥2, step 2.1 gives Xk+1≥Xk+δ, where δ=7295/90804>0. Induction gives X2+r≥X2+rδ for each integer r≥0. Given any real bound M, [F8] supplies an integer r>(M−X2)/δ ; hence X2+r>M. 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

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