联邦学习领域终于有了形式化的计算模型——这篇论文用类型化张量语言统一了分散的协议，做联邦学习系统设计和理论研究的团队值得细读，能帮你理清通信与共享状态的数学本质。
本文提出了一种类型化张量语言，用于形式化联邦学习与联邦分析中常见的计算结构。该语言区分了客户端分区的联邦张量和全局可用的共享张量，并通过与虚拟全局张量的对比定义语义。核心成果是共享状态分解理论：证明类型化单轮程序可通过固定维度的共享状态分解，且该状态大小与客户端和记录数量无关。此外，还证明了可表示性的逆定理，并将对应关系扩展到跨轮状态共享的迭代程序。最后，开发了可微分的学习片段，支持服务器端梯度下降和二阶更新，形式化了一类通信仅通过固定维度共享状态的联邦学习计算。
A Typed Tensor Language for Federated Learning
Federated learning and analytics are often described as collections of separate protocols, even when they share the same mathematical form: client-local tensor computation, mergeable aggregation into shared state, and shared-only post-processing. We introduce a typed tensor language that formalizes this structure. The language distinguishes federated tensors, whose records are partitioned across clients along a tracked record axis, from shared tensors, which are available globally. Its semantics are defined by comparison with a virtual global tensor, used only as a reference object. The main result is a shared-state factorization theory. We show that typed one-round programs factor through fixed-dimensional shared state whose size is independent of the number of clients and records, computed from client-local tensor expressions and merged across clients. We also prove a converse representability result; factorizations whose encoders and decoders are expressible in the language are realized by typed one-round programs, and the correspondence extends to iterative programs whose cross-round state is shared. This gives a formal account of the computations in the language that can be expressed as encode, merge, and decode procedures. We then develop a differentiable fragment for learning. If a per-record loss and its per-record gradient are represented by client-local tensor expressions, the global gradient is represented by record-axis summation of the federated gradient tensor. This yields typed iterative programs for server-side gradient descent and shared-linear-algebra second-order updates. The framework characterizes a broad class of federated learning computations whose communication passes through fixed-dimensional shared state.