Equation (9) — Gradient growth around a common objective minimizer
ProvedSCAFFOLD.GradientGrowthFor convex client functions and any minimizer of their average, every satisfies
Formalization note: direct source inequality, multiplied by ; individual client minimizers need not coincide. No stochastic run is required.
Source: Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020; arXiv:1910.06378v4, https://arxiv.org/abs/1910.06378v4; Appendix B.1, PDF p. 14, equation (9), setup used in Section 5.
Notation and probability model
There are clients, a model space (including ), differentiable client losses with -Lipschitz gradients, , and . The starting point is deterministic and bounds within-client stochastic-gradient standard deviation. A run has rounds, local steps, clients per round, local step , global step , and . All random variables live on a standard Borel probability space with a filtration containing the full history. States and gradient samples are square integrable; gradient samples are conditionally unbiased, have conditional squared error at most , and are independent across clients conditional on each step's history. These are explicit fresh-oracle and finite-moment conventions.
Every round first defines virtual paths for all clients, starting at :
Then an -element subset is sampled uniformly, conditionally independently of these paths given the past. Equivalently, its conditional distribution given the entire completed virtual-path history is uniform. Only selected clients update their controls to ; other controls persist. The server update is . This is option II of Algorithm 1, with the average-gradient form of Appendix E. The model contains the algorithm and oracle laws, not any convergence inequality.
For convex targets, minimizes , and the client losses obey
The initial client controls are arbitrary deterministic vectors and the server control is their average. Define
For nonconvex targets, for all ; a minimizer need not exist. Each is instead initialized by averaging fresh stochastic gradients at , with the same conditional oracle assumptions. These full-client initialization queries are additional to the optimization rounds.
The output is a sampled pre-round server iterate among , represented by its expected loss or squared-gradient statistic. No last-iterate or pathwise guarantee is asserted. Sources: Section 2, PDF p. 2; Algorithm 1, PDF p. 4; Appendix B.1, PDF p. 14, assumptions A3–A5; Appendix E, PDF pp. 25–26, equations (18)–(22), Remark 10; Appendix E.2, PDF pp. 31 and 35, equations (26)–(27) and final warm-start paragraph. Primary reference: Karimireddy et al., SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, https://arxiv.org/abs/1910.06378v4.
import Definitions.Def_SCAFFOLD_Model open MeasureTheory universe u
namespace SCAFFOLD
theorem GradientGrowth :
∀ (d N : ℕ) (P : Problem d N) (xstar : Space d),
Convexity P 0 → IsMinimizer P xstar → ∀ x,
(N : ℝ)⁻¹ * ∑ i, ‖gradient (P.f i) x - gradient (P.f i) xstar‖ ^ 2 ≤
2 * P.β * (objective P.f x - objective P.f xstar) := by sorry
end SCAFFOLDRead-back
What the Lean code literally says, in plain math · gpt-6
For every pair of natural numbers , consider the Euclidean space with its usual real inner product and norm, and data consisting of real-valued functions indexed by , real numbers , and a point . The data are required to satisfy , , and ; each has a gradient at every point of , and for every index and every its gradients satisfy . Define . For every , assume that the convexity condition at parameter zero holds: and, for every and , (the additional quadratic term in that condition has coefficient ). Also assume that is a global minimizer of the average objective, meaning for every . Then, for every , . The minimizer is assumed, rather than asserted to exist or to be unique; it need not minimize each individual . The parameters and are part of the universally quantified data, but beyond they impose no further hypothesis here and do not occur in the conclusion. The case is excluded by the data requirements, while , , and are included. In dimension zero, consists of a single point and the conclusion is ; the conclusion also reduces to whenever . There is no assumption of a strictly positive convexity parameter.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.