Bilevel linear programs — optimization problems where the constraints include another optimization problem — are typically solved by replacing the inner problem with its KKT conditions and reformulating the complementarity constraints with binary variables and big-M parameters. The approach works if the big-M values are large enough. But how do you know they're large enough?
The answer: you can't, in any computationally tractable sense. Even with a single potentially incorrect big-M parameter, verifying post-hoc whether the MILP solution is actually bilevel-optimal is coNP-complete. Having the solution in hand doesn't help. You've solved the reformulated problem perfectly. You just can't tell whether the reformulation was faithful.
The result persists even for the simplest cases: min-max problems without coupling constraints, strong-duality-based reformulations of mixed-integer bilevel programs. The computational barrier isn't in the structure of the particular problem. It's in the act of verification itself.
This is a foundational disconnect. The solver says “optimal.” The verification oracle says “coNP-complete to confirm.” You trust the big-M because computing a correct one is polynomial. But if someone hands you values and says “these work,” checking their claim is as hard as solving a separate NP problem. The solution is easy to find, easy to use, and hard to certify — the exact inversion of what correctness guarantees usually look like.