Certifying Global Optimality of Stationary Points in Imperfect-Recall Games

Single-player decision problems with imperfect recall model a player who may forget information she once had. They arise wherever a strategy must stay compact: the absent-minded driver, imperfect-recall abstractions of poker, and team games compressed into a single forgetful player. The ex-ante optimal behavior strategy of such a problem maximizes a polynomial over a product of simplices. Deciding optimality is $\exists \mathbb{R}$-complete, near-optimality is NP-hard, and the degree of the polynomial grows with the number of visits to an information set. Practice therefore relies on first-order methods: regret matching and its predictive-plus variant reach stationary points at scale. Such a point comes with no guarantee about its distance from the global optimum. We add a certificate layer that runs after the solver. A support-pruned sum-of-squares feasibility program at level $\lceil \mathrm{deg}u/2\rceil$ bounds how far any strategy can beat the reported value. A posterior step turns the floating-point solution into a bound re-verified in exact and interval arithmetic, and the same certificate decomposes the residual gap across information sets. On $77$ instances regenerated from the generators of the reference benchmark, the layer certifies the PRM${}^{+}$ stationary point as globally optimal within relative tolerance $10^{-4}$ on $70$, or $90.9\%$. The verdict is invariant across $10$ seed groups and $4$ of $5$ first-order methods. The global solver SCIP corroborates it to the same tolerance on all $77$; on one instance SCIP reaches that tolerance only at its one-hour limit, where the layer needs $68$ seconds. Support pruning is lossless at level one and wherever strict complementarity holds. The one certified loss is an interior cubic whose gap narrows $33\times$ one level up. On these instances, the stationary points of the standard solvers are almost always global optima, and a sum-of-squares certificate makes that fact checkable in seconds and provable in exact arithmetic in minutes.