Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds

We study the refuter problems for proof complexity lower bounds. Suppose ϕ is a hard tautology that does not admit any length-s proof in some proof system P. In the corresponding refuter problem, we are given (query access to) a purported length-s proof π in P that claims to have proved ϕ, and our goal is to find an invalid derivation step within π. As suggested by witnessing theorems in bounded arithmetic, the computational complexity of these refuter problems is closely tied to the metamathematics of the underlying lower bounds. We focus on refuter problems corresponding to lower bounds for resolution, which is arguably the single most studied system in proof complexity. As a warm-up, we show that many refuter problems for resolution width lower bounds are PLS-complete. To capture the complexity of refuter problems for resolution size lower bounds, we introduce a new class rwPHP(PLS) in decision-tree TFNP, which can be seen as a randomized version of PLS. First, we show that the refuter problems for many resolution size lower bounds can be solved in rwPHP(PLS), including the classic lower bound of Haken [TCS, 1985] for the pigeonhole principle. More generally, we identify a common proof technique that we call ”random restriction + width lower bound”, and present strong evidence that resolution lower bounds proved by this technique typically have refuter problems in rwPHP(PLS). We then show that the refuter problem for any resolution size lower bound is rwPHP(PLS)-hard, thereby demonstrating that the rwPHP(PLS) upper bound mentioned above is tight. Informally speaking, this means that ”rwPHP(PLS)-reasoning” is necessary for proving all resolution size lower bounds. Interpreted in bounded arithmetic, our results show that the theory T21(α) + dwPHP(PV(α)) characterizes the ”reasoning power” required to prove (the ”easiest”) resolution size lower bounds. As a corollary, we obtain surprisingly efficient proofs of resolution lower bounds. In particular, we show that many resolution size lower bounds can be proved in low-width random resolution [Pudlák–Thapen, CCC’17].