AI in Math deals with mathematics in a constructive manner so that reasoning becomes automated, less laborious, and less error-prone. For algorithms, the question becomes how to automate analyses for specific problems. For the first time, this work provides an automatic method for approximation analysis on a well-studied problem in theoretical computer science: computing approximate Nash equilibria in two-player games. We observe that such algorithms can be reformulated into a search-and-mix paradigm, which involves a search phase followed by a mixing phase. By doing so, we are able to fully automate the procedure of designing and analyzing the mixing phase. For example, we illustrate how to perform our method with a program to analyze the approximation bounds of all the algorithms in the literature. Same approximation bounds are computed without any hand-written proof. Our automatic method heavily relies on the LP-relaxation structure in approximate Nash equilibria. Since many approximation algorithms and online algorithms adopt the LP relaxation, our approach may be extended to automate the analysis of other algorithms.

翻译：AI数学以构造性方式处理数学问题，使推理过程自动化、减少劳动量并降低出错概率。对于算法而言，关键问题在于如何针对特定问题实现分析自动化。本研究首次为理论计算机科学中一个经典问题——双人博弈中的近似纳什均衡计算——提供了自动化的近似分析方法。我们观察到此类算法可重构为"搜索-混合"范式：首先执行搜索阶段，随后进行混合阶段。通过这一重构，我们能够完全自动化混合阶段的设计与分析流程。例如，我们演示了如何编写程序对文献中所有算法进行近似界分析，无需任何人工推导即可计算出相同的近似界。该自动化方法高度依赖于近似纳什均衡中的线性规划松弛结构。由于许多近似算法和在线算法都采用线性规划松弛技术，我们的方法有望推广至其他算法的自动化分析。