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.
Local updates and periodic synchronization give different averages
Example
Let and on , let the two local-SGD workers start at , and use step size with one uniform component draw per worker and step from . Couple two executions by choosing the positive-probability draw sequence in which worker 1 draws twice and worker 2 draws twice. After two steps without intermediate synchronization their mean is . If they instead synchronize after the first step and again after the second, their final mean is .
Example references
Facts & Assumptions
Given: The two differentiable component functions and the common starting point in the Example.
Local SGD with periodic synchronization: each step samples a component uniformly and updates ; a synchronization replaces all worker states by their arithmetic mean.
The two workers' component draws are independent and uniform at each step, as in [F1]. The displayed coupled draw sequence therefore has probability in either schedule.
Proof technique: direct.
Proof
The gradients are and . Without an intermediate synchronization, worker 1 follows and worker 2 follows . Their arithmetic mean is .
With synchronization after the first step, the worker states are first and , so their common synchronized value is . On the second step, the same coupled draws give worker states and . Their mean is .
Since and the draw sequence in [A1] has positive probability under the algorithm, the two schedules can produce different final worker means.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
2 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
- Sebastian U. Stich, Local SGD Converges Fast and Communicates Little, Definition 2.1 (standard reference, not scraped)