联邦学习通用算法的正确编排：CSP中的形式化和验证
摘要：联邦学习（FL）是一种机器学习环境，其中客户端保持训练数据的分散，并在中央服务器（集中式FL）或对等网络（分散式FL）的协调下共同训练模型。正确的编排是其中一个主要挑战。在本文中，我们使用CSP进程演算和PAT模型检查器，形式化验证了两个通用FL算法的正确性，一个是集中式的，一个是分散式的。CSP模型由对应于通用FL算法实例的CSP进程组成。PAT通过证明这两个通用FL算法的无死锁性（安全性属性）和成功终止（活性属性），自动证明它们的正确性。CSP模型是从底向上手工构建的，作为真实Python代码的忠实表示，并通过PAT自动进行自顶向下的检查。
作者：Ivan Proki''c, Silvia Ghilezan, Simona Kav{s}terovi''c, Miroslav Popovic, Marko Popovic, Ivan Kav{s}telan
论文ID：2306.14529
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-06-27