Automating approximation analysis for Nash equilibria algorithms in two-player games

Computing polynomial-time approximate Nash equilibria (NE) is a fundamental problem in algorithmic game theory, with deep connections to the complexity class TFNP. Recent advances in approximate NE algorithms have become increasingly sophisticated, making the verification of their approximation guarantees both complex and error-prone. We present the first automated method for analyzing approximation bounds of algorithms for two-player normal-form games. Given any algorithm that computes approximate NE, our approach automatically derives tight approximation bounds using constraint programming techniques. We demonstrate the effectiveness of our method by applying it to all known algorithms in the literature, reproducing their manually-proven approximation bounds within seconds and without human intervention. Our results provide both a powerful verification tool and new insights into the structure of approximate equilibrium computation.