联邦学习通用算法的正确编排:基于 CSP 的形式化与验证
分布式、并行与集群计算
2023-06-27 v1
摘要
联邦学习(FL)是一种机器学习设置,其中客户端保持训练数据去中心化,并在中央服务器协调下(中心化 FL)或对等网络中(去中心化 FL)协作训练模型。正确编排是主要挑战之一。本文使用 CSP 进程演算与 PAT 模型检测器,形式化验证两种通用 FL 算法(一种中心化、一种去中心化)的正确性。CSP 模型由对应于通用 FL 算法实例的 CSP 进程组成。PAT 通过证明两种通用 FL 算法的无死锁性(安全性性质)与成功终止(活性性质)自动证明其正确性。CSP 模型自底向上手工构建,作为真实 Python 代码的忠实表示,并由 PAT 自顶向下自动检查。
引用
@article{arxiv.2306.14529,
title = {Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP},
author = {Ivan Prokić and Silvia Ghilezan and Simona Kašterović and Miroslav Popovic and Marko Popovic and Ivan Kaštelan},
journal= {arXiv preprint arXiv:2306.14529},
year = {2023}
}
备注
arXiv admin note: text overlap with arXiv:2305.20027