Discovering expert-level Nash equilibrium algorithms with large language models.

Area of Science:

• Algorithmic Game Theory
• Artificial Intelligence
• Computational Complexity

Background:

• Designing polynomial-time algorithms for approximate Nash equilibria (ANE) with worst-case guarantees is a key challenge.
• Large language models (LLMs) can propose algorithms, but formal verification of their guarantees is difficult.
• No automated system previously existed for certifying worst-case guarantees of ANE algorithms.

Purpose of the Study:

• To create an automated framework for certifying worst-case guarantees of ANE algorithms.
• To leverage LLMs for discovering novel ANE algorithms with provable guarantees.
• To push the boundaries of multi-player ANE algorithm design.

Main Methods:

• Developed LegoNE, a framework that encodes expert proof strategies into a symbolic language.
• LegoNE compiles candidate algorithms into finite optimization problems for certification.
• Integrated LegoNE with a reasoning LLM to automate algorithm discovery and verification.

Main Results:

• Successfully rediscovered an algorithm matching the best polynomial-time guarantee for two-player games.
• Discovered a novel three-player ANE algorithm with an improved guarantee (0.5 + δ).
• The new three-player algorithm's guarantee is provably beyond the capabilities of the extension technique.

Conclusions:

• Encoding domain-specific proof strategies into machine-tractable languages enables LLM-driven algorithm discovery.
• LegoNE facilitates the creation of ANE algorithms beyond existing human design paradigms.
• This approach advances the field of algorithmic game theory by automating formal verification and discovery.