Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918404680581120 |
|---|---|
| author | Li, Jiawei Li, Yuhao Ren, Hanlin |
| author_facet | Li, Jiawei Li, Yuhao Ren, Hanlin |
| contents | 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]. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_15515 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds Li, Jiawei Li, Yuhao Ren, Hanlin Computational Complexity Logic in Computer Science 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]. |
| title | Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds |
| topic | Computational Complexity Logic in Computer Science |
| url | https://arxiv.org/abs/2411.15515 |