Brief Announcement: Certified Multiplicative Weights Update: Verified Learning Without Regret
Brief Announcement: Certified Multiplicative Weights Update: Verified Learning Without Regret
复制标题
简短公告：认证乘法权重更新：验证学习无悔
DOI：
10.1145/3087801.3087852
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Stewart, Gordon
中科院分区：
文献类型：
--
作者：
Bagnall, Alexander;Merten, Samuel;Stewart, Gordon
乘法权重更新方法（MWU）是一种简单而强大的算法，用于学习线性分类器，集成学习，近似求解线性和半定系统，计算多商品流问题的近似解，以及在线凸优化等应用。在这个简短的声明中，我们应用交互式定理证明的技术来定义并证明MWU的第一个正式验证的实现是正确的（具体来说，我们证明了我们的MWU是没有遗憾的）。我们的主要应用程序-和一个理由，我们的工作相关的PODC社区-是验证多智能体系统，如分布式多智能体网络流和负载平衡游戏，验证MWU提供了一个方便的方法，分布式计算近似粗相关均衡。
The Multiplicative Weights Update method (MWU) is a simple yet powerful algorithm for learning linear classifiers, for ensemble learning a la boosting, for approximately solving linear and semidefinite systems, for computing approximate solutions to multicommodity flow problems, and for online convex optimization, among other applications. In this brief announcement, we apply techniques from interactive theorem proving to define and prove correct the first formally verified implementation of MWU (specifically, we show that our MWU is no regret). Our primary application -- and one justification of the relevance of our work to the PODC community -- is to verified multi-agent systems, such as distributed multi-agent network flow and load balancing games, for which verified MWU provides a convenient method for distributed computation of approximate Coarse Correlated Equilibria.