SearcharxivSearch

arXiv subjects

Dimitrios Alexopoulos

Publications and source records attributed to Dimitrios Alexopoulos.

2 recordsLinked to original sources

DisAgg: Distributed Aggregators for Efficient Secure Aggregation in Federated Learning

Federated learning enables collaborative model training across distributed clients, yet vanilla FL exposes client updates to the central server. Secure-aggregation schemes protect privacy against an honest-but-curious server, but existing approaches often suffer from many communication rounds, heavy public-key operations, or difficulty handling client dropouts. Recent methods like One-Shot Private Aggregation (OPA) cut rounds to a single server interaction per FL iteration, yet they impose substantial cryptographic and computational overhead on both server and clients. We propose a new protocol called DisAgg that leverages a small committee of clients called Aggregators to perform the aggregation itself: each client secret-shares its update vector to Aggregators, which locally compute partial sums and return only aggregated shares for server-side reconstruction. This design eliminates local masking and expensive homomorphic encryption, reducing endpoint computation while preserving privacy against a curious server and a limited fraction of colluding clients. By leveraging optimal trade-offs between communication and computation costs, DisAgg processes 100k-dimensional update vectors from 100k 5G clients with a 4.6x speedup compared to OPA, the previous best protocol.

cs.CR

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic

Neither the classical nor intuitionistic logic traditions are perfectly aligned with the purpose of reasoning about computation, as neither can permit unconstrained recursive definitions without inconsistency: recursive definitions must normally be proven terminating before admission and use. Grounded arithmetic or GA is a formal-reasoning foundation allowing direct expression of arbitrary recursive definitions. GA adjusts traditional inference rules so that terms that express nonterminating computations harmlessly denote no semantic value ($\bot$) instead of yielding inconsistency. Recursive functions are proven terminating in GA essentially by "dynamically typing" terms, or equivalently, symbolically reverse-executing the computations they denote via inference rules. Once recursive functions have been proven terminating, logical reasoning about them reduces to familiar classical rules. We summarize the development and lessons learned from two mechanically-checked formulations of GA, finding both syntactically consistent and semantically sound with respect to an underlying computable model. Propositional grounded arithmetic or PGA is a quantifier-free system for inductive grounded reasoning about open formulas. PGA has logical expressiveness comparable to Skolem's PRA, but has general-recursive (Turing-complete) functional expressiveness. PGA builds upon a simpler system of basic grounded arithmetic or BGA, which omits logical operators entirely. BGA and PGA are not only sound but semantically complete, a combination impossible for powerful classical systems with arithmetic, due to G\"odel's incompleteness theorems. These results suggest that powerful and consistent formal reasoning with unconstrained recursive definitions is possible, potentially enabling new computation-centric formal languages, proof assistants, and type systems in the future.

cs.PL