From Proof Complexity to Circuit Complexity via Interactive Protocols
arxiv(2024)
摘要
Folklore in complexity theory suspects that circuit lower bounds against
𝐍𝐂^1 or 𝐏/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
𝐍𝐄𝐗𝐏⊈𝐏/poly, as recently
observed by Pich and Santhanam (2023).
We show such a connection conditionally for the Implicit Extended Frege proof
system (𝗂𝖤𝖥) introduced by Krajíček (The Journal of Symbolic
Logic, 2004), capable of formalizing most of contemporary complexity theory. In
particular, we show that if 𝗂𝖤𝖥 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 𝗂𝖤𝖥 proofs implies #𝐏⊈𝐅𝐏/poly (which would in turn imply, for example,
𝐏𝐒𝐏𝐀𝐂𝐄⊈𝐏/poly). Our proof
exploits the formalization inside 𝗂𝖤𝖥 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 𝗂𝖤𝖥. Interestingly, further improving our result seems to require
progress in constructing interactive proof systems with more efficient provers.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要