发表机构
IEOR Department, Columbia University; CMOR Department, Rice University（哥伦比亚大学工业工程与运筹学系; 莱斯大学计算机、数学与统计系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该论文证明交替梯度下降-上升（AltGDA）在有限双人零和矩阵博弈中实现全局 $O(1/T)$ 遍历收敛，并指出最后迭代不收敛，平均迭代是必要的，且结果已在 Lean 4 中验证。
AI 中文摘要
交替梯度下降-上升（AltGDA）是求解有限双人零和矩阵博弈的一种简单且实际有效的方法。然而，AltGDA 的理论仍然有限：现有结果要么仅适用于无约束设置，要么在约束设置中对均衡施加了限制性假设。我们证明 AltGDA 在每个有限双人零和矩阵博弈中均以 $O(1/T)$ 的遍历速率全局收敛。与先前结果不同，我们的保证对每个初始化点和每个时间范围 $T$ 均成立：AltGDA 迭代的均匀平均值满足 $O(1/T)$ 的对偶间隙界。我们的证明受到使用一种新颖的性能估计规划（PEP）框架在紧凸集上搜索 Lyapunov 函数所获得的数值结果的启发。此外，我们提供了简单的反例，表明 AltGDA 的最后迭代对偶间隙不会收敛到零。这证明了迭代平均对于实现 $O(1/T)$ 速率确实是必要的。我们已在 Lean 4 中形式化并机器检查了我们的全局遍历收敛结果。
英文摘要
Alternating gradient descent-ascent (AltGDA) is a simple and practically effective method for solving finite two-player zero-sum matrix games. However, the theory of AltGDA remains limited: existing results either apply only to unconstrained settings or require restrictive assumptions on the equilibrium in constrained settings. We show that AltGDA converges globally at an $O(1/T)$ ergodic rate in every finite two-player zero-sum matrix game. Unlike prior results, our guarantee holds for every initialization and every horizon $T$: the uniform averages of the AltGDA iterates satisfy an $O(1/T)$ duality-gap bound. Our proof is inspired by numerical results obtained using a novel performance estimation programming (PEP) framework for Lyapunov function search over compact convex sets. Additionally, we provide simple counterexamples showing that the last-iterate duality gap of AltGDA does not converge to zero. This justifies why averaging of iterates is indeed necessary to achieve an $O(1/T)$ rate. We have formalized and machine-checked our global ergodic convergence result in Lean 4.
