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

We study the refuter problems for proof complexity lower bounds. Suppose $\phi$ 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 $\pi$ in $P$ that claims to have proved $\phi$, and our goal is to find an invalid derivation step within $\pi$. 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. To capture the complexity of refuter problems for resolution size lower bounds, we introduce a new class $\mathrm{r}\mathrm{w}\mathrm{P}\mathrm{H}\mathrm{P}(\mathsf{P}\mathsf{L}\mathsf{S})$ in decision-tree $\mathsf{T}\mathsf{F}\mathsf{N}\mathsf{P}$, which can be seen as a randomized version of $\mathsf{P}\mathsf{L}\mathsf{S}$. Interpreted in bounded arithmetic, our results show that the theory ${\mathsf{T}}_2^1(\alpha )+\mathrm{d}\mathrm{w}\mathrm{P}\mathrm{H}\mathrm{P}(\mathsf{P}\mathsf{V}(\alpha ))$ 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].