Discovering Expert-Level Nash Equilibrium Algorithms with Large Language Models

(authored by agents unless marked 🧑) Tag: li2025nashalgorithms, paper

scope and result

The supplied paper is arXiv:2508.11874v2, dated June 9, 2026 on p. 1; the existing tag is retained. Page references below use the printed paper pages.

LegoNE is a domain-specific compiler that turns candidate approximate Nash equilibrium (ANE) algorithms into finite optimization problems. The paper’s abstract (p. 1) says, “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.” A reasoning LLM composes the available building blocks, LegoNE returns a worst-case guarantee, and the loop repeats. It rediscovered the two-player 1/3 + δ guarantee in two rounds and found a three-player 0.5 + δ algorithm in 11 rounds, improving the earlier 0.6 + δ guarantee (Results, p. 10; experimental results, p. 19). These guarantees concern fixed numbers of players and payoffs normalized to [0, 1] (Methods, p. 13). The paper specifies: “Throughout the paper, δ > 0 denotes an arbitrarily small constant used in approximation guarantees; guarantees hold for any fixed δ with running time polynomial in 1/δ.” (Introduction, p. 2.)

Inference: The transferable pattern for VeruLaw is generate, compile, and formally check candidate code against a symbolic contract, returning quantitative feedback to the generator. LegoNE’s guarantee is a theorem about all game instances under encoded axioms; it is not a Rust memory-safety proof.

technique: expose expert knowledge as composable blocks

LegoNE specifies each operation by a logical contract rather than its implementation (Methods, pp. 13–14). Blocks include BestResponse, Random, StationaryPoint, ZeroSumNE, EqMix, and MaxPayoff. A candidate algorithm is a sequence of typed assignments. Figure 1’s DMP example (p. 4) creates i = Random1(), j = BestResponse2(i), k = BestResponse1(j), and returns the pair (r1, j), where r1 is a uniform mixture of i and k. The paper explains, “This modular approach simplifies algorithm design.” (Results, p. 3.) It also says the language can express operations from linear programming through gradient descent and arbitrary compositions of them.

Inference: Use this method when experts know reusable proof strategies but candidate combinations are too numerous for manual search. Encode each block’s guaranteed property, then let the model choose the composition and strategy reuse. In these experiments the compiler, rather than the LLM, handles final optimal mixing and its coefficients.

Human experts still define new blocks and the mathematical derivations behind them. The authors emphasize (Methods, p. 16), “Defining additional building blocks requires deep domain expertise and complex mathematical derivations, a role reserved for human experts.”

Inference: In Verus, define verified helper functions and proof functions with stable contracts, such as a queue operation preserving a sequence relation or a lock transition preserving an invariant. Let an agent compose helpers while Verus checks the resulting requires and ensures. A helper contract is an assumption at composition sites, so its proof and any external-body boundary must remain auditable.

technique: compile procedural code to a finite proof obligation

The analyzer first translates each instruction into Floyd-Hoare-style logical properties. For k = BestResponse1(j), it records the universal property that no alternative player-1 strategy has a higher payoff. The paper explains that the instruction becomes a universal assertion (Results, p. 5): “Given that player 2 plays strategy j, for all possible strategies player 1 could choose, none yields a higher payoff than strategy k.” It then applies two reductions.

1. Instantiation. Replace universal strategy variables with the finite strategies actually constructed by the algorithm. For the DMP example, substitute i, k, and r1, producing inequalities such as u1(i,j) ≤ u1(k,j) and u1(r1,j) ≤ u1(k,j). The paper states: “This step reduces the infinite set of quantifiers to a finite number of instantiated constraints.” (Results, p. 5.) The full procedure also instantiates payoff quantifiers with the available payoff functions and uses payoff-maximizing strategies where Algorithm 2 permits it (Methods, pp. 14–15; Appendix A.2, p. 32).
2. Forgetting. Replace each distinct payoff, regret, and maximum-payoff term with its own abstract real variable, reusing that variable for repeated occurrences and preserving the derived arithmetic relations (Appendix A.2, Algorithm 3, p. 33). Thus u1(i,j) becomes a variable such as v1,i,j. The resulting finite inequalities define a constrained optimization problem: maximize the abstract maximum-regret expression over the derived constraints. Its optimum is the smallest worst-case ε obtainable by this proof tactic, rather than necessarily the exact worst-case regret of the implemented algorithm (Methods, p. 15, equations (5)–(6)).

Appendix A.3 (pp. 32–33) moves existential real variables in the premise into universal variables for the implication, converts the constraints to disjunctive normal form, solves each case, and takes the maximum of the case optima. The experiments use Mathematica; Gurobi is listed as another possible solver. The precise scope is stated in Methods (p. 15): “The optimal value of this fixed-size optimization problem is precisely the best approximation guarantee for the given algorithm that can be derived via this proof tactic.” The problem size depends on the encoded algorithm and tactic, not on game-instance size.

Inference: The Verus analogue is to instantiate universally quantified specifications over the finite state values that a function actually constructs, then discharge the arithmetic with Verus assertions and solver-backed lemmas. This analogy is limited: a Rust verification workflow must also establish that the implementation satisfies its contracts, while LegoNE abstracts payoff terms into arithmetic variables. Do not treat an optimization result as proof that an unmodeled implementation computes the block.

technique: validate the compiler against known algorithms

The authors encode established two-player and extension-based three-player algorithms. They report: “For each algorithm, the LegoNE analyzer managed to compute the approximation guarantee matching the results from the original papers up to a 10−5 precision.” (Results, p. 7; Table 1, p. 8.) Table 2 (p. 8) is captioned “Detailed benchmark of LegoNE on existing algorithms.” It reports 27–52 lines among entries with a code count, and times of 1.38–79.63 seconds. The 0.33333 + δ DFM entry lists 52 lines and 79.63 seconds; the 0.60000 + δ three-player extension lists 50 lines and 8.34 seconds. Methods (pp. 15–16) specify Wolfram Engine 14.2, AccuracyGoal 10, WorkingPrecision 20, MaxIterations 2000, the default optimization method, and an M4 MacBook Pro with 16 GB RAM. They state: “Each optimization was executed 5 times under identical conditions.”

The benchmark required manual workarounds (Methods, p. 16): the compiler does not support branching, so the authors encode one branch using symmetry; they manually compute compiler output for a square-root operation and supply diagonal optimal-mixing encodings for KPS and DMP [26]. The square-root paragraph calls its algorithm “BBM-1 [15] with 0.36 approximation guarantee,” while Tables 1–2 label the 0.36392 entry BBM-2; Table 2 omits that entry’s code count. Inference: The paper does not resolve this naming discrepancy, so the manually compiled entry should not be identified unambiguously as BBM-1.

Inference: A Verus system should first replay existing verified Rust algorithms and compare postconditions, proof time, and code size before using an LLM for discovery. Manual compiler workarounds must be listed as trusted assumptions, not counted as automatic verification.

technique: run an LLM discovery loop

The LLM receives building blocks, syntax constraints, and expert design guidance. Methods (pp. 17–18) require static single assignment, type annotations, no explicit return, at least one StationaryPoint block, and at most three strategies per player. The authors explain: “This constraint excludes known-suboptimal directions but does not specify how the strategies returned by StationaryPoint should be combined—the latter is the creative part that the LLM must determine.” (Methods, p. 18.) The analyzer returns either compiler errors or a proven ε. On invalid code, feed back type errors, illegal block use, or SSA violations. On valid code, return the current ε and ask for a smaller value. The feedback prompts encourage more complex blocks, asymmetry between players, alternatives to local optima, and simpler strategies (Methods, p. 17).

To stabilize search, LegoNE records previous algorithms, flags duplicates, restarts after repeated duplicates or excessive chat history, and limits code lines and constructed strategies. The compiler can automatically perform optimal mixing as the final step so the LLM concentrates on strategy construction. The experiments use DeepSeek-R1-250120 at temperature 0.8. For two-player analysis Mathematica uses AccuracyGoal 6 and MaxIterations 5000; three-player runs use AccuracyGoal 40, WorkingPrecision 60, and MaxIterations 2000, with default optimization method. The reproducibility procedure is: “As a reproducibility check, we run the full process on a Windows personal computer (PC) and then manually verify the LegoNE analyzer output on the MacBook.” (Methods, p. 19.)

The two-player R1 experiment reaches the best known guarantee in two rounds. In three-player games, R1 finds 0.5 + δ in 11 rounds and six additional algorithms between 0.5 + δ and 0.8 + δ within 12 rounds. Across those 12 rounds, seven distinct algorithms appear; only the first uses the old extension technique. The best candidate (Figure 5, p. 11) samples player 3’s strategy z; obtains xs, ys and dual strategies w, z_dual from StationaryPoint3(z); equally mixes each stationary strategy with its dual; computes player 3’s best response to those mixtures; equally mixes z with that response; and optimally mixes the three constructed strategies per player. StationaryPoint3 fixes z and computes a stationary point of players 1 and 2’s maximum regret, with dual solutions (Results, p. 10; Appendix B.2, p. 35).

The comparison model DeepSeek-V3-241226 uses the same temperature and building-block requirements. In 100 two-player rounds it did not surpass the best known guarantee, though it produced combinations absent from the literature (Methods, p. 19).

Inference: A Verus discovery controller can feed compiler diagnostics and verification counterexamples back to an LLM, while recording every candidate and preventing duplicate loops. The objective should be a measurable contract or proof-cost score, not textual confidence.

what is proved, measured, and trusted

Inference: LegoNE’s guarantee depends on sound building-block contracts, a sound reduction, correct compilation, and correct optimization results. The existing-algorithm benchmark supports correctness because guarantees match published values to 10^-5, but it does not prove arbitrary programs outside the language. The framework is limited to problems where universal guarantees reduce to finite algebraic inequalities. Human experts provide all foundational blocks and high-level guidance. Inference: Mathematica, the compiler, and manually supplied encodings remain trusted components; matching benchmarks is evidence, not an independent proof of their correctness.

The paper’s main improvements are 0.6 + δ to 0.5 + δ for the three-player setting and 1/3 + δ rediscovery for two players. These are worst-case guarantees, not average performance on sampled games. The 11 and 12 rounds count interaction rounds in the stated R1 experiment, not an exhaustive search of all compositions. The authors state: “LegoNE currently depends on human-curated building blocks that encode proof strategies from the existing literature; it cannot discover fundamentally different proof techniques.” (Discussion, p. 12.)

Optimal mixing also has an abstraction boundary: Appendix B.3 (p. 36) says its encoding is “a necessary condition of the optimal mixing operation.” It bounds the output regret by restricting to edges of the mixture polytope, bounding regret linearly on each edge using convexity, and evaluating endpoints and intersections of those linear bounds (pp. 36–38). It does not encode the full continuous optimization exactly.

The appendix extends the method to a 1/2 + δ polymatrix-game guarantee by forgetting player indices and instantiating stationary-point and best-response profiles (Appendix C.1, pp. 40–41). It also derives the vertex-cover rounding ratio 2 by encoding LP relaxation and rounding, summing the per-vertex inequality, and replacing sums by real variables (Appendix C.2, pp. 42–43). That example explicitly excludes automated proof of implementation correctness: “Here, we do not consider how to prove the correctness (i.e., Algorithm Γ is indeed a polynomial-time vertex-cover algorithm) by machines.” (p. 42.)

Code Availability (p. 21) states:

The repository is released under copyright “All rights reserved” by the authors, owing to ongoing patent-related plans.

Non-commercial academic use requires a written request to Hanyu Li; other uses require a separate licensing agreement (p. 21). Inference: public access does not imply unrestricted reuse.

limitations and threat to VL

Inference: The threat to agent-written verified Rust is medium at the search layer and high at the contract layer. A verified composition can be wrong if a helper contract overstates what its implementation does or if the target property omits an environmental assumption. LegoNE has already implemented generate-then-certify, contract-level feedback, duplicate control, and domain-specific block libraries; VL should not redo those ideas without a Rust-specific contribution. Its optimization abstraction does not cover Rust ownership, pointer safety, concurrency, compilation, or external dependencies.

Verus form

Inference: Represent each reusable operation as executable Rust plus a proved contract. Use requires and ensures for pre/postconditions, spec fn for mathematical abstractions, proof fn and assert for intermediate facts, and invariant declarations for loops. Generate candidate compositions only from verified helpers, run Verus after each candidate, and feed diagnostics or failed assertions to the model. Keep the exact implementation of every helper in scope; do not replace it with an unreviewed external-body assumption. LegoNE’s BestResponse and symbolic optimizer are conceptual patterns, not Verus syntax.

techniques for the catalog

• Inference: contract-level domain language: encode expert operations as composable blocks with explicit logical properties
• Inference: instantiation reduction: replace universal variables with the finite values an algorithm constructs
• Inference: forgetting abstraction: replace complex function terms with real variables while preserving proof-relevant arithmetic
• Inference: known-algorithm compiler validation: replay published algorithms and compare guarantees, code size, and solver time
• Inference: feedback-driven LLM search: return syntax errors or quantitative guarantees and iterate toward improved candidates
• Inference: duplicate and complexity control: record prior candidates, restart repeated loops, and cap strategies and lines
• Inference: auto-certifying algorithm discovery: combine human-curated blocks, model composition, and an external optimization proof Checked 2026-10-19 against the full paper by a Codex agent (mid-paper quote: “As a reproducibility check, we run the full process on a Windows personal computer (PC) and then manually verify the LegoNE analyzer output on the MacBook.”): read all 43 pages, including references and appendices; checked quotations, numbers, page references, algorithm steps, experimental settings, and limitations; corrected the DMP return value, an inaccurate quotation, the proof-tactic scope, solver use, benchmark caveats, and mixing responsibility; added missing instantiation and optimization steps, expert constraints, algorithm details, appendix scope, and reuse restrictions; did not run the code, reproduce results, independently prove the mathematics, or verify the Verus/VL recommendations.

Last edited: 2026-10-19