تقرير
From Proof Complexity to Circuit Complexity via Interactive Protocols
| العنوان: | From Proof Complexity to Circuit Complexity via Interactive Protocols |
|---|---|
| المؤلفون: | Arteche, Noel, Khaniki, Erfan, Pich, Ján, Santhanam, Rahul |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Computational Complexity |
| الوصف: | Folklore in complexity theory suspects that circuit lower bounds against $\mathbf{NC}^1$ or $\mathbf{P}/\operatorname{poly}$, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation $\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$, as recently observed by Pich and Santhanam (2023). We show such a connection conditionally for the Implicit Extended Frege proof system ($\mathsf{iEF}$) introduced by Kraj\'i\v{c}ek (The Journal of Symbolic Logic, 2004), capable of formalizing most of contemporary complexity theory. In particular, we show that if $\mathsf{iEF}$ proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of $\mathsf{iEF}$ proofs implies $\#\mathbf{P} \not\subseteq \mathbf{FP}/\operatorname{poly}$ (which would in turn imply, for example, $\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$). Our proof exploits the formalization inside $\mathsf{iEF}$ of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan (Journal of the ACM, 1992). This has consequences for the self-provability of circuit upper bounds in $\mathsf{iEF}$. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers. Comment: A conference version of this work is accepted to the 51st EATCS International Colloquium on Automata, Languages and Programming (ICALP 2024) |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2405.02232 |
| رقم الأكسشن: | edsarx.2405.02232 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |