Designing polynomial-time algorithms for approximate Nash equilibria (ANE) with provable worst-case guarantees is a fundamental open problem in algorithmic game theory. While large language models (LLMs) can generate candidate algorithms at scale, certifying worst-case guarantees requires formal analysis over all game instances -- a task for which no automated system previously existed. Here, we present LegoNE, a framework encoding expert proof strategies into a symbolic language that automatically compiles any candidate algorithm into a finite optimization problem certifying its worst-case guarantee. Integrating LegoNE with a reasoning LLM, we rediscovered an algorithm matching the best polynomial-time guarantee for two-player games, and discovered a three-player algorithm improving the best guarantee from $0.6+δ$ to $0.5+δ$ -- provably beyond the reach of the extension technique, the only previously known multi-player ANE design paradigm. These results show that encoding domain-specific proof strategies into a machine-tractable language can support LLM-driven discovery of algorithms outside known human design paradigms.

翻译：设计具有可证明最坏情况保证的近似纳什均衡（ANE）多项式时间算法是算法博弈论中的一个基本开放问题。虽然大语言模型（LLMs）能够大规模生成候选算法，但验证最坏情况保证需要对所有博弈实例进行形式化分析——此前不存在任何自动化系统能够完成此任务。在此，我们提出LegoNE框架，该框架将专家证明策略编码为符号语言，能够自动将任何候选算法编译为有限优化问题，以验证其最坏情况保证。通过将LegoNE与推理型大语言模型集成，我们重新发现了一种匹配双人博弈最优多项式时间保证的算法，并发现了一种三人博弈算法，将最佳保证从$0.6+δ$提升至$0.5+δ$——该结果已超越扩展技术（此前唯一已知的多玩家ANE设计范式）的适用范围。这些结果表明，将领域特定的证明策略编码为机器可处理语言，能够支持大语言模型驱动下发现超越已知人类设计范式的算法。