Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
This work addresses foundational issues in proof complexity and automated theorem proving, offering incremental advances in understanding the metamathematics of resolution lower bounds.
The paper tackles the problem of verifying short proofs in resolution proof systems by studying refuter problems, which aim to find invalid steps in purported proofs of hard tautologies. It introduces a new complexity class and shows that many resolution size lower bounds can be proven efficiently in low-width random resolution.
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. To capture the complexity of refuter problems for resolution *size* lower bounds, we introduce a new class $\mathrm{rwPHP}(\mathsf{PLS})$ in decision-tree $\mathsf{TFNP}$, which can be seen as a randomized version of $\mathsf{PLS}$. Interpreted in bounded arithmetic, our results show that the theory $\mathsf{T}^1_2(α) + \mathrm{dwPHP}(\mathsf{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].