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.

The assigned SAGA Lyapunov factor fails under standard initialization

Statement refuted

For the SAGA iterates and table in Finite-sum SAGA, with step size $η > 0$ and a minimizer $x^{*}$ of $F = n^{- 1} \sum_{i} f_{i}$ , write $V_{k} = ∥ x_{k} - x^{*} ∥_{2}^{2}$ , $S_{k} = n^{- 1} \sum_{i = 1}^{n} ∥ α_{i}^{k} - \nabla f_{i} (x^{*}) ∥_{2}^{2}$ , and $L_{k} = V_{k} + 7 η^{2} n S_{k}$ .

The contract-required one-step bound $E [L_{k + 1}] \leq (1 - μ η) E [L_{k}]$ need not hold for the prescribed SAGA initialization, even when $η \leq \min {1 / (3 L), μ / (13 L^{2})}$ . The following finite instance has $n = 100$ , $L = μ = 1$ , $x_{0} = 1$ , and $η = 1 / 13$ , but $L_{1} / L_{0} = 844 / 869 > 12 / 13 = 1 - μ η$ .

Facts & Assumptions

Given: $d = 1$ , $n = 100$ , $f_{i} (x) = x^{2} / 2$ for every $i$ , the standard SAGA initialization $x_{0} = 1$ , $α_{i}^{0} = f_{i}^{'} (x_{0})$ , and $η = 1 / 13$ .

[F1]

Finite-sum SAGA: initialize $α_{i}^{0} = \nabla f_{i} (x_{0})$ ; at each step form $v_{k} = \nabla f_{I_{k}} (x_{k}) - α_{I_{k}}^{k} + {\overset{ˉ}{α}}_{k}$ , set $x_{k + 1} = x_{k} - η v_{k}$ , then replace the selected table entry using the pre-update point.

[F2]

Strong convexity for an extended-real objective: $1$ -strong convexity is the strong-Jensen inequality with decrement $\frac{1}{2} θ (1 - θ) ∣ x - y ∣^{2}$ .

[F3]

Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction: a $1$ -Lipschitz gradient satisfies $∣ f_{i}^{'} (x) - f_{i}^{'} (y) ∣ \leq ∣ x - y ∣$ .

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : in one dimension $∥ x ∥_{2}^{2} = x^{2}$ .

[F5]

Complete ordered field (least-upper-bound property): rational inequalities are preserved by multiplication by positive denominators.

[F6]

Laws of finite sums and finite products: a finite average of identical component functions equals that common function.

Counterexample

1.1F2F3F4F6givenalgebra

Each $f_{i}^{'} (x) = x$ , so [F3] holds with $L = 1$ . For $z = (1 - θ) x + θ y$ , direct expansion gives $(1 - θ) f_{i} (x) + θ f_{i} (y) - f_{i} (z) = \frac{1}{2} θ (1 - θ) (x - y)^{2}$ ; hence [F2] holds with $μ = 1$ . The finite-sum scaling law [F6] gives $F (x) = x^{2} / 2$ , so $x^{*} = 0$ is stationary. The step size satisfies $1 / 13 \leq 1 / 3$ and $1 / 13 = μ / (13 L^{2})$ .

1.2F1givenalgebra

By [F1], every initial table entry and its mean equal $1$ . For any sampled index, $v_{0} = f_{I_{0}}^{'} (1) - 1 + 1 = 1$ , so $x_{1} = 1 - 1 / 13 = 12 / 13$ . The replacement stores $f_{I_{0}}^{'} (x_{0}) = 1$ , leaving the whole table unchanged. Therefore $V_{0} = 1$ , $V_{1} = (12 / 13)^{2} = 144 / 169$ , and $S_{0} = S_{1} = 1$ .

2.1F4F5step 1.2givenalgebra∎

With $L_{k} = V_{k} + 7 η^{2} n S_{k}$ , [F4] gives $L_{0} = 1 + 700 / 169 = 869 / 169$ and $L_{1} = 144 / 169 + 700 / 169 = 844 / 169$ . Thus $L_{1} / L_{0} = 844 / 869$ . Since $13 \cdot 844 = 10972 > 10428 = 12 \cdot 869$ by [F5], this ratio is greater than $12 / 13 = 1 - μ η$ . The sampled update is deterministic because all components are identical, so the same strict failure holds for the expected Lyapunov values.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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

Aaron Defazio, Francis Bach, and Simon Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NeurIPS 2014 (standard reference, not scraped)
Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2) (2018) (standard reference, not scraped)