What the paper shows in plain terms: a common trick for solving bilevel linear programs (BLPs) is to turn the lower problem into its optimality conditions and add binary switches and big‑M constants to make a single mixed‑integer linear program (MILP). The authors prove that deciding, after the fact, whether the MILP solution is actually optimal for the original bilevel problem is computationally intractable in the worst case. In complexity terms, that decision is coNP‑complete even if only one big‑M parameter might be wrong. They also show related verification tasks remain hard for other reformulations and for min–max special cases without coupling constraints.

What the researchers did and how the reformulation works: the standard route replaces the follower’s linear program by Karush‑Kuhn‑Tucker (KKT) conditions. One resulting condition, complementarity (either a slack is zero or its multiplier is zero), is usually linearized by introducing binary variables and large constants called big‑M values. Those big‑M numbers act as upper bounds that turn logical “either/or” relations into linear inequalities and so yield a MILP that can be fed to standard solvers. The paper studies two questions: (Q1) Given an optimal solution of that MILP, can we efficiently check whether it is bilevel‑optimal? and (Q2) Given an optimal MILP solution, can we efficiently verify that the chosen global big‑M values are correct (that they do not cut off any feasible or optimal follower solutions)?

Main technical findings: the authors prove that Q1 is coNP‑complete — so unless widely believed complexity collapses occur, there is no polynomial‑time algorithm that always verifies bilevel optimality a posteriori. The hardness holds even when the two big‑M constants are equal, and it extends to strong‑duality based reformulations for mixed‑integer bilevel programs and to min–max instances without coupling constraints. For Q2 they show that checking global big‑M correctness remains computationally difficult even when an optimal MILP solution is provided. They also present approximation‑style hardness: even deciding an ε‑approximate optimality is coNP‑hard for any fixed ε in (0,1).