Theoretical computer science · Result 104

Quasipolynomial algorithms for mean-payoff, stochastic and parity games

4 papersLean

Gives deterministic algorithms using \(2^{O((\log(L+2))^2)}\) bit operations, for complete binary input length L, for ordinary mean-payoff games and two separate extensions. They compute exact values and optimal positional strategies in ordinary games, the nonnegative expectation-of-liminf value set in turn-based stochastic games, and the winning set for nonnegative liminf mean payoff conjoined with parity. Signed rewards, rational chance probabilities, and parity priorities are unrestricted and binary-encoded.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 4

Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time

OpenAI · October 5, 2026

We give a uniform deterministic quasipolynomial-time algorithm for finite turn-based stochastic mean-payoff games with signed integer rewards and rational chance-transition probabilities encoded in binary. It computes exactly the vertices of nonnegative value, including value zero, for the expectation of the pathwise liminf mean payoff. The algorithm uses exact rational arithmetic and \(2^{O((\log(L+2))^2)}\) bit operations, where L is the complete binary input length.

Read PDF Download Source

Cite

@misc{OAI:Turn-Based-Stochastic-Mean-Payoff-Games-in-Deterministic-Quasipolynomial-Time-October-5-2026,
  author = {{OpenAI}},
  title = {{Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Turn-Based-Stochastic-Mean-Payoff-Games-in-Deterministic-Quasipolynomial-Time-October-5-2026/stochastic-mean-payoff-games.pdf}{OAI:Turn-Based-Stochastic-Mean-Payoff-Games-in-Deterministic-Quasipolynomial-Time-October-5-2026}},
  year = {2026}
}

Mean-payoff parity games in quasipolynomial time

OpenAI · October 5, 2026

We give a uniform deterministic quasipolynomial-time algorithm for mean-payoff parity games. It computes all vertices from which a player can enforce both nonnegative liminf mean payoff and the parity condition, with arbitrary signed binary rewards and unrestricted binary priorities. The running time is \(2^{O((\log(L+2))^2)}\) bit operations, where L is the complete input length.

Read PDF Download Source

Cite

@misc{OAI:Mean-payoff-parity-games-in-quasipolynomial-time-October-5-2026,
  author = {{OpenAI}},
  title = {{Mean-payoff parity games in quasipolynomial time}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Mean-payoff-parity-games-in-quasipolynomial-time-October-5-2026/mean-payoff-parity.pdf}{OAI:Mean-payoff-parity-games-in-quasipolynomial-time-October-5-2026}},
  year = {2026}
}

Deterministic quasipolynomial-time mean-payoff games

OpenAI · September 25, 2026

We give a deterministic algorithm that computes the complete zero-threshold winning set of a finite mean-payoff game with arbitrary signed integer edge weights encoded in binary. For total explicit input length L, it uses \(2^{O((\log(L+2))^2)}\) bit operations. A reduction also computes the exact rational value at every vertex and globally optimal positional strategies for both players within the same quasipolynomial bound.

Read PDF Download Source

Cite

@misc{OAI:Deterministic-quasipolynomial-time-mean-payoff-games-September-25-2026,
  author = {{OpenAI}},
  title = {{Deterministic quasipolynomial-time mean-payoff games}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Deterministic-quasipolynomial-time-mean-payoff-games-September-25-2026/paper.pdf}{OAI:Deterministic-quasipolynomial-time-mean-payoff-games-September-25-2026}},
  year = {2026}
}

Randomized quasipolynomial-time mean-payoff games

OpenAI · September 25, 2026

We give a randomized algorithm that computes the complete zero-threshold winning set of a finite mean-payoff game with arbitrary signed integer edge weights encoded in binary. For total explicit input length L, it uses \(2^{O((\log(L+2))^2)}\) bit operations on every random tape and is correct with probability at least 7/8. A polynomial-time check certifies the winning regions and positional strategies for both players or reports failure. Independent repetition therefore gives an always-correct algorithm with the same expected quasipolynomial bit bound.

Read PDF Download Source

Cite

@misc{OAI:Randomized-quasipolynomial-time-mean-payoff-games-September-25-2026,
  author = {{OpenAI}},
  title = {{Randomized quasipolynomial-time mean-payoff games}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Randomized-quasipolynomial-time-mean-payoff-games-September-25-2026/paper.pdf}{OAI:Randomized-quasipolynomial-time-mean-payoff-games-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization checks that a specified two-step execution of Truffet's elimination procedure terminates with a feasible but nonoptimal output. It is a finite counterexample to that proposed optimization step.

The formalized result gives one randomized algorithm for the complete zero-threshold winning set of every finite mean-payoff game with signed binary weights. It succeeds with probability at least \(7/8\) and runs in quasipolynomial bit time on every random tape. Self-loops, parallel edges, and history-dependent strategies are allowed, and winning means a nonnegative liminf average payoff.

Comparator links

Result	Comparator statement
Finite counterexample to Truffet's optimization procedure	TruffetCounterexample.lean
Randomized quasipolynomial mean-payoff algorithm	RandomizedMeanPayoff.lean

Scope note on GitHub →